Google DeepMind announced that its researchers used AI agents to produce machine-checked proofs demonstrating that key security properties hold for the actual implementation of the Signal protocol. Signal’s cryptographic protocol protects private conversations in apps such as Signal and Google Messages.
The tool: AlphaProof Code
The work used AlphaProof Code, an agentic framework that combines human expertise with multiple large language models to perform deep formal verification. Formal verification means mathematically proving that code implements intended properties without flaws.
How the verification was done
- Researchers first translated Signal’s security goals into formal mathematical specifications, with human experts reviewing each specification.
- AI agents, including those powered by Gemini Carbon, generated the proofs. The agents produced more than six million lines of Lean, a language used for computer-checked mathematical proofs.
- The agents audited those proofs and flagged portions needing human reinspection — about one percent of the codebase, according to DeepMind — allowing experts to focus human judgment where it mattered while Lean automatically checked the rest.
Why this matters
Most prior protocol verification work has been limited to design-level models. DeepMind says this is the first time AI agents have been used to formally verify the implementation of a widely deployed cryptographic protocol at this depth — proving that the compiled, device-running code fulfills the specified security properties. That matters because real-world vulnerabilities frequently arise in the gap between design and implementation.
The verification covered properties such as protecting messages before and after a device is temporarily compromised. Bridging design and implementation increases complexity substantially, which is why this result is notable.
Timeframe and validation
DeepMind reports that the verification process took four weeks — a task that historically has taken expert teams years. To validate the system’s ability to detect insecurity, the team reintroduced two previously fixed, real bugs into an isolated copy of Signal’s code; in both cases, the system produced machine-checked proofs showing the buggy versions were insecure.
Implications and next steps
DeepMind suggests the approach could be extended to other critical systems, from medical device firmware to power-grid software, although scaling will require further research. Paired with automated defense agents such as CodeMender, formal verification could help counter fast, agent-driven cyber threats by providing mathematical guarantees that protections work.
Open source and acknowledgements
DeepMind said it will open-source the formal verification artifacts for community use. The research team includes Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, Charles Sutton, and Pushmeet Kohli. The announcement also thanks multiple contributors and acknowledges feedback from Signal representatives Rolfe Schmidt, Michael Rosenberg, and Ehren Kret.
Summary
According to DeepMind, AlphaProof Code enabled AI agents to produce over six million lines of Lean proofs and reduce human review to roughly one percent of the codebase, completing a formal verification of Signal’s core cryptographic implementation in four weeks. If independently confirmed, the result would represent a significant step toward wider deployment of machine-checked security guarantees for critical software.
