DeepMind's AlphaProof Code formally verifies Signal's cryptographic protocol

Google DeepMind says it has used AI agents to mathematically prove the security properties of Signal's cryptographic protocol, the code that secures conversations in apps including Signal and Google Messages. The company announced the result, achieved with a new framework called AlphaProof Code, in a blog post on November 10, 2026.

According to DeepMind, the work is the first time AI has formally verified a widely deployed cryptographic protocol at this depth. The company also claims it is the first time the implementation of such a protocol, as opposed to its abstract design, has been formally verified by any method, with or without AI.

How the verification worked

Formal verification uses mathematics to prove that code behaves as intended, and is generally regarded as the strongest form of security assurance available. It has traditionally been so slow and labor-intensive that it is rarely applied to large, production software.

DeepMind describes AlphaProof Code as a multi-LLM agentic framework that divides the labor the way a research group would. Human experts worked alongside models to translate Signal's security goals into formal mathematical specifications, and every specification was reviewed by a person. Agents running on a model DeepMind calls Gemini Carbon then carried out the proofs, producing more than six million lines of Lean, a language in which proofs are mechanically checked.

The agents then audited their own work and flagged only about one percent of the generated codebase for human scrutiny. Because Lean verifies the remainder automatically, DeepMind says its experts could concentrate on the small fraction where judgment mattered most.

Proofs extended to deployed code

DeepMind points out that most formal analysis of cryptographic protocols stops at the design level. Its agents went further, showing that the compiled code satisfies key security properties, including that messages stay protected before and after a device is temporarily compromised, for the exact code running on devices. The company argues this step matters because flaws in real systems frequently arise in the translation from design to implementation, and covering that distance is what makes such proofs so difficult.

Even so, the entire effort took four weeks, according to DeepMind, which says comparable verification efforts have historically taken expert teams years.

Planted bugs were caught

To test whether the system could actually distinguish secure code from broken code, the researchers reintroduced two real, previously fixed bugs into an isolated copy of Signal's code. In both cases, DeepMind reports, the system produced a machine-checked proof that the modified version was insecure.

Why it matters

Cryptographic protocols sit underneath nearly all digital communication, from banking to browsing, and DeepMind notes that a single flaw can expose millions of people at once. Until now, mathematical proof of such code has been out of reach for widely deployed software. If DeepMind's results hold up, machine-checked verification could become practical for the systems that need it most, and Signal users gain a stronger guarantee that the protocol's privacy claims hold in the actual shipped code.

DeepMind also frames the result as preparation for a future of AI-driven attacks, arguing that automated theorem proving paired with defensive agents like its CodeMender tool can match the speed and scale of modern threats.

Open artifacts and open questions

The company is open-sourcing its formal verification artifacts and has published a technical paper. It cautions that scaling these techniques further will require continued research, and suggests the approach could eventually secure other critical software, from medical device firmware to power grid systems. Signal researchers Rolfe Schmidt, Michael Rosenberg and Ehren Kret provided feedback on the methodology, according to the post, although the verification work itself was carried out by DeepMind's team.