DeepMind AlphaProof Formally Verifies Signal Protocol Code

Google DeepMind researchers have introduced AlphaProof Code, an agentic framework that formally verified core security properties of the cryptographic code underlying the Signal protocol, a milestone in software assurance for a system protecting billions of messages in apps such as Signal and Google Messages. The work is described as the first time AI has been used to formally verify a widely deployed cryptographic protocol at this depth, and the first time the implementation of such a protocol has been formally verified by any method. AlphaProof Code combines human expertise with a multi-model AI workflow. Researchers and human experts translated Signal’s security requirements into formal mathematical specifications, after which agents powered by Gemini Carbon generated more than 6 million lines of Lean proof code to mathematically establish that the compiled implementation satisfies key protections, including security before and after temporary device compromise. The agents then audited the proofs and identified only about 1% of the codebase for human review, allowing Lean to verify the remainder automatically. The team said the verification took four weeks rather than years, a task historically requiring large expert teams. To validate the system’s soundness, researchers reintroduced two previously fixed real-world bugs into an isolated version of Signal’s code; AlphaProof Code produced machine-checked proofs that the buggy versions were insecure. The researchers include Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, Charles Sutton and Pushmeet Kohli, with contributions and support from collaborators at Google DeepMind and Signal.