Google DeepMind says it formally verified the machine code of the Signal protocol with AlphaProof Code

Pushmeet Kohli of Google DeepMind announced that his team has proven key security properties of the machine code underlying the Signal messaging protocol. DeepMind says this is the first time the production code of a widely deployed protocol has been formally verified, by any method, at this depth. These are DeepMind's own claims.

The work used AlphaProof Code, which DeepMind describes as a new agentic framework for formal verification that runs on LLMs including Gemini Carbon. DeepMind says the verification reaches down to the code running on devices, and that it took about a month, where similar efforts could take teams decades of combined effort. It credits the Signal team as a partner.

DeepMind is open-sourcing its formal specifications and verification artifacts so others can build on them. The post had 1,297 likes on X by the morning of November 10.