Google DeepMind Unveils AlphaProof Code for Formal Software Verification

Google DeepMind researchers Pushmeet Kohli and Swarat Chaudhuri announced AlphaProof Code, a multi-LLM agentic framework designed to formally verify complex software at depth. According to DeepMind, the system was used to mathematically prove key security properties of the actual code running Signal's cryptographic protocol, which secures messaging in Signal and Google Messages. DeepMind stated this represents the first time the implementation of a widely deployed cryptographic protocol has been formally verified at this depth. In the reported workflow, human experts collaborated with models to translate Signal's security goals into formal mathematical specifications. Agents powered by Gemini Carbon then conducted the proofs, generating over six million lines of Lean code. The agents subsequently audited the proof to highlight areas requiring human review, which DeepMind stated accounted for approximately one percent of the codebase, with Lean automatically checking the remaining proof. DeepMind reported the process took four weeks, compared to years historically required by expert teams. To test detection capabilities, researchers reintroduced two known, previously fixed bugs into an isolated version of Signal's code; in both cases, the system generated machine-checked proofs that the flawed versions were insecure. Ehren Kret, CTO of Signal, noted that using AI agents to translate production code into valid Lean theorems enables verification on a larger scale. Google DeepMind stated it is open-sourcing its formal verification artifacts.

Key takeaways

• Google DeepMind introduced AlphaProof Code, using human-agent collaboration and Gemini Carbon to generate over six million lines of Lean code for Signal's protocol.
• The process formally verified the compiled implementation of Signal's cryptographic protocol within four weeks, with human experts reviewing about one percent of the proof flagged by agents.
• When two previously fixed bugs were reintroduced in isolated testing, AlphaProof Code produced machine-checked proofs identifying both versions as insecure.
• Google DeepMind stated that it is open-sourcing its formal verification artifacts for the community.