📅 November 10, 2026 • Google DeepMind
Google DeepMind announced AlphaProof Code, an agentic framework for formal verification of software. Researchers guided AI agents to mathematically prove key security properties of the actual code of the Signal protocol, which protects private conversations in Signal and Google Messages. Per DeepMind, this is the first time AI formally verified a widely deployed cryptographic protocol at this depth, and the first time the implementation of such a widely deployed protocol was formally verified by any method, with or without AI.
The framework works in layers. Human experts worked with models to translate the security goals of Signal into formal mathematical specifications, and per DeepMind every specification was reviewed. Agents powered by Gemini Carbon generated over 6 million lines of Lean, a language for machine-checked mathematical proofs. The agents audited the proofs and flagged just 1 percent of the codebase for human review, while the Lean checker automatically verifies the rest.
Per the DeepMind technical report, the team verified libsignal, the reference implementation of the Signal protocol, at the machine-code level, including the PQXDH post-quantum handshake and the Triple Ratchet design. Proofs cover properties such as keeping messages protected before and after a device is temporarily compromised, down to the exact compiled code running on devices. Per DeepMind, most earlier protocol verification stopped at the design level, and the process took four weeks.
Signal CTO Ehren Kret, quoted by DeepMind, called the use of AI agents to translate live code into valid Lean theorems a major breakthrough, adding that rigorously verifying the Signal protocol implementation gives the team even greater confidence in its code privacy guarantees.
WIRED reported on November 10, 2026 that the analysis did not find new vulnerabilities in the portions of the Signal protocol it examined. When researchers ran AlphaProof Code on older versions of Signal that contain known, long-fixed vulnerabilities, it correctly identified them and showed those versions could not be formally verified.
WIRED also noted the limits of the result. The team did not verify the whole Signal mobile app, researchers describe the work as one milestone among many, and DeepMind ran the project as research without disclosing its cost.
What this changes
For security engineering, the result moves formal verification from design documents to deployed code. Proofs now cover the exact compiled code running on devices, and machine-checked review reduces the manual audit burden to the 1 percent of the code that agents flagged for human review. Per DeepMind, the formal specification and the proofs are being published so that other teams can build on the work.
The DeepMind blog, written by Pushmeet Kohli and Swarat Chaudhuri, describes formal verification as the highest standard of security assurance, one that has historically been difficult and labor-intensive. With agents generating over 6 million lines of Lean proofs and humans reviewing only 1 percent of the codebase, per DeepMind, the practical cost of that standard drops, and the published specifications give other protocol teams a concrete starting point.
Sources:
deepmind.google/blog/introducing-alphaproof-code
wired.com/story/a-new-ai-tool-from-google-deepmind-formally-verified-the-signal-protocol
google-deepmind.github.io/code-verification
Continue the conversation: https://t.me/AIAutomationArchitecture · Bluesky
Top comments (0)