DeepMind generated 6.5 million lines of proof for Signal—but it did not verify the app

The story

Google DeepMind has used teams of AI agents to produce machine-checked proofs for key security properties in compiled code from Signal’s cryptographic library. The AlphaProof Code project generated about 6.5 million lines of Lean proof and connected guarantees such as forward secrecy, authentication and post-compromise security to an AArch64 executable built from libsignal. DeepMind published the paper, proof artifacts and code on November 10.

The result is more specific than saying AI proved Signal secure. Researchers linked the unmodified Rust library into a small command-line harness, compiled it with the stock Rust toolchain and reasoned about roughly 140,000 machine instructions. Their proofs cover the post-quantum PQXDH handshake and Triple Ratchet under defined symbolic and computational models. They do not cover the complete Signal mobile or desktop applications, their user interfaces, servers, group messaging or every deployment environment.

Formal verification begins by expressing a desired property as mathematics and proving that a program satisfies it. Ordinary testing can expose failures in scenarios engineers remember to try; a valid formal proof can exclude every failure covered by its statement and assumptions. The difficulty is cost. DeepMind’s paper notes that verification of the seL4 microkernel took about 20 person-years, while the CompCert compiler took about six. AlphaProof Code’s proof work was completed by a five-person team working for four weeks.

That speed did not remove people from the process. Human researchers selected the reference models, decided what to prove, guided the structure of the specifications and approved changes to trusted assumptions. AI agents drafted specifications, proposed amendments and generated the proof code. A gatekeeper compared each result with a held-out, human-approved specification, and Lean’s small kernel accepted or rejected the derivation. The authors say they wrote no proof code themselves.

This distinction matters because a proof can be perfectly valid and still establish the wrong claim. The agents’ millions of proof lines are treated as untrusted: a logical mistake prevents Lean from accepting them. The specification and execution model remain trusted. DeepMind estimates that a reviewer must examine about 18,000 lines of definitions and theorem statements, plus roughly 8,000 lines describing AArch64 semantics and symbol information tied to the executable.

The campaign added two useful checks against empty or weak specifications. Researchers restored two previously fixed libsignal bugs in isolated builds and showed that the resulting binaries violated the symbolic security theorem. They also checked the compiler’s output rather than trusting Rust or the compiler to preserve source-level properties. That narrows a long-standing gap between proving an abstract protocol design and establishing properties of the bytes a processor runs.

The trust boundary is still substantial. Low-level cryptographic routines are represented by assumed contracts rather than verified instruction by instruction. The model concerns a single-threaded, statically linked process and does not model threads, dynamic linking or arbitrary files. The paper says its computational theorem is classical and does not establish the post-quantum healing property intended by SPQR; it also uses restrictions including fixed message lengths and a one-to-one session setting.

Independent reporting reinforces both the importance and the limits. WIRED described the work as a landmark demonstration but noted that it did not verify the entire app and that earlier Signal formal-methods research provided a head start. The Register reported that the proofs cover PQXDH and Triple Ratchet properties in libsignal. No outside research group has yet published a full reproduction or audit of the newly released artifacts.

INNOVOX analysis: AlphaProof Code changes the economics of proof generation, not the logic of assurance. A machine-checked proof is stronger than an AI-generated code review because the proof assistant does not accept persuasive language or probabilistic confidence. Yet the most consequential choices—scope, threat model, abstractions and trusted contracts—remain human decisions. Faster proofs make specification quality more important, not less.

What to watch next is replication and transfer. Formal-methods researchers can inspect the public Lean repository, audit the trusted base and rerun its deterministic checks. A stronger demonstration would reproduce the result independently, extend it to Signal’s group and application layers, and apply the workflow to unrelated critical code without months of custom preparation. Until then, the project is a technically significant verification campaign, not a universal certificate that Signal—or software generally—cannot be hacked.

INNOVOX analysis

The advance is not an AI declaration that software is safe; it is a division of labor. Humans define the claim and its trust boundary, agents generate enormous proofs, and a small proof kernel rejects invalid derivations. If outside researchers reproduce the artifacts, this could shift formal verification from a rare, multiyear project toward a repeatable security-engineering process. The bottleneck then moves from writing proofs to writing specifications that deserve to be trusted.

What to watch

Watch for independent reproduction of the released Lean artifacts, audits of the trusted specifications and AArch64 semantics, stronger post-quantum theorems, and expansion to group messaging, sealed sender and real application environments. Cost, compute use and performance on unrelated codebases will determine whether the method becomes practical beyond a flagship demonstration.