Google DeepMind's AlphaProof Code Proves Signal's Encryption Correct: 6.5 Million Lines of Lean in Four Weeks

Google DeepMind on Monday introduced AlphaProof Code, an agentic formal-verification framework, and used it to clear a milestone that security researchers have chased for decades: a machine-checked mathematical proof that the actual code of the Signal protocol delivers its core security guarantees. The company says it is the first time the implementation of a widely deployed cryptographic protocol has been formally verified by any method, with or without AI. Signal's encryption protects conversations in Signal, Google Messages and other messaging apps used by billions of people.

The distinction that matters is depth. Most formal analysis of a cryptographic protocol stops at the design level, checking a mathematical description of how the protocol should behave. Real vulnerabilities, however, often hide in the gap between that design and the implementation running on a phone. DeepMind's agents proved properties about compiled AArch64 instructions from an unmodified build of libsignal v0.105.4, a binary of roughly 560 KB containing about 140,000 instructions, removing the "trust the compiler" assumption from the equation.

The workflow splits the labor the way a research team would. Human experts worked with models to translate Signal's security goals into formal specifications, reviewing every one. Agents powered by Gemini then generated over six million lines of Lean, a proof language checked mechanically by its kernel, and audited their own output, flagging about one percent of the codebase for a second human look. The whole verification took four weeks, a task DeepMind says has historically taken expert teams years.

The proofs cover the post-quantum PQXDH handshake and the Triple Ratchet, establishing forward secrecy, authentication, handshake secrecy and post-compromise security, meaning messages stay protected before and after a device is temporarily compromised. As a sanity check, the team reintroduced two real, previously fixed bugs into an isolated version of Signal's code. In both cases the system produced a machine-checked proof that the buggy build was insecure. No new vulnerabilities were found in the current code.

Signal's CTO Ehren Kret called the automatic translation of live code into valid Lean theorems a major breakthrough, saying the result gives the team greater confidence in its privacy guarantees. Signal staff reviewed the methodology but did not participate in the proofs.

The caveats are significant. The guarantees apply to one-to-one sessions in a specific compiled binary under documented assumptions; group messaging, sealed sender, side channels and several multi-device scenarios remain outside the verified scope, and DeepMind has not disclosed the compute cost or whether this becomes a product. The specifications, the proofs and the artifacts are being open-sourced, and DeepMind names medical device firmware and power grid software as candidate next targets, paired with its automated CodeMender defense agents.

The result lands in a fast-moving niche. Within the past year, DeepMind's AlphaProof Nexus worked through open Erdos problems, Claude generated 180 million lines of proof for open-source libraries, and startups like &Truth and Axiom Math have raised money around machine-checked verification. What those efforts share is an admission that AI now writes code faster than humans can review it; AlphaProof Code's answer is to stop reviewing and start proving.