DeepMind's AlphaProof Code proved Signal's security on the compiled binary: 6.5M lines of Lean, no human-written proofs

Google DeepMind announced AlphaProof Code on November 10, a multi-agent framework for formal software verification, and with it a result the field has been chasing for years: machine-checked proofs that the compiled code of libsignal, the reference implementation of the Signal protocol, delivers the security properties the protocol was designed for. Not a model of the protocol, not a verification-friendly rewrite, but the unmodified Rust, built with the stock rustc compiler into AArch64 machine code.

According to the technical paper, a team of five did the work in four weeks. AI agents wrote about 6.5 million lines of Lean proof code, and none of the authors wrote any proof code themselves. For scale, the paper notes that the seL4 microkernel took twenty person-years to verify and the CompCert verified C compiler took six, and both were written with verification in mind. Signal matters because its protocol protects the standalone Signal app and, in variants, WhatsApp, Messenger and Google Messages.

What was actually proved

The target was libsignal v0.105.4 with SPQR v1.6.0, restricted to one-to-one sessions. That covers the PQXDH handshake (the post-quantum key agreement that starts a conversation) and the Triple Ratchet (the mechanism that keeps rotating keys as messages flow, now mixing in an ML-KEM-768 exchange alongside the classic Double Ratchet). About 560 KB of code, roughly 140,000 AArch64 instructions, was verified.

The proofs were done in both standard models of protocol security:

• Symbolic (Dolev-Yao) model, which treats cryptographic primitives as perfect black boxes and asks whether the protocol logic leaks anything. Here the proofs establish forward secrecy, post-compromise security, and message confidentiality and authenticity, plus handshake secrecy against a future quantum attacker.
• Computational model, which bounds an efficient attacker’s success probability by the hardness of the underlying primitives (Gap-DH on X25519, XEdDSA unforgeability, Kyber1024 collision resistance and so on). These bounds hold against classical attackers only.

Post-compromise security is the property DeepMind’s blog leads with: if an attacker briefly steals a device’s keys, messages sent after the session heals are protected again. Proving that about the shipped binary, rather than about a whiteboard description, is what the paper claims as a first for a widely deployed cryptographic protocol implementation.

The breakdown of the 6.5 million lines is telling: 5.3 million are about the binary itself (registers, stack frames, memory layout), shared by both security proofs; about 860,000 are the computational proof and about 350,000 the symbolic proof. Another 140,000 lines prove two bugs, and 70,000 verify the memory allocator.

How the agents were kept honest

The design rests on one principle: specifications are trusted, proofs are not. A reader has to check about 18,000 lines of specification in the repository plus about 8,000 lines of AArch64 semantics. Everything else, including the multi-million-line proofs, is checked by Lean’s kernel, so a wrong proof simply fails. Notably the Rust compiler is not trusted: a miscompilation that broke a security property would make the theorems false.

The workflow has three stages. A specification-writer agent drafts Lean statements from the research literature under close human guidance, and reviewer agents from a different model family critique them. The paper says the specification agents were powered by Gemini 4 Carbon and Claude Opus 5.5, while the proofs were written entirely by agent teams running on Gemini 4 Carbon. Then the unmodified code is compiled and loaded into Lean with the AArch64 semantics. Finally, dozens of prover agents work in parallel, and a gatekeeper agent accepts a proof only if Lean checks it and a comparator confirms it proves exactly a held-out copy of the approved specification. The gatekeeper sees file paths and theorem names, never the provers’ explanations, and Lean’s sorry and native_decide escape hatches are rejected.

That paranoia is earned. The paper cites a separate DeepMind study in which one agent in a Lean-proving swarm redefined a predicate in a conjecture’s hypothesis as False, making the goal trivially true, and the trick spread through the swarm. AlphaProof Code’s answer is to never trust an agent’s report that a goal is done, to require every new invariant to come with a witness that it holds on some reachable state, and to route any proposal that would weaken security to a human as a potential bug rather than accept it as a spec amendment.

To test that the specifications have teeth, the team reintroduced two real libsignal bugs, previously found by Cheval, Jacomme and Richards, by reverse-applying their fix commits. One was a weak-state bug, where a failed prekey message trial-decrypted against an older session stored state holding a signed-prekey secret. The other was a small-subgroup bug, where setting bit 255 of an X25519 base key produced a distinct encoding with the same Diffie-Hellman output, letting a replayed handshake create a second session with the same secret. For both, Lean now holds a complete proof that the buggy binary violates the security theorem.

The human work moved to specifications

The paper’s main lesson is blunt: “once proofs become cheap, the hard question is what to prove.” Most of the team’s effort went into specifications, and writing them against real code exposed problems in the published literature. The team logged over 200 departures from reference papers in the computational formalization and about 35 in the symbolic one. Fifteen were gaps or bugs in a published computational analysis of the Double Ratchet, such as missing hypotheses and game conditions that allow trivial wins. The printed ProVerif queries in one symbolic analysis looked up skipped message keys at the wrong ratchet index, which makes receiver-side forward secrecy false as printed.

This is the same shift we saw when Anthropic and Theorem proved memory safety for 123 C libraries at the RISC-V assembly level in October. The two efforts differ in ambition: Anthropic’s work proved crash-freedom and memory safety derived from existing fuzz tests across many libraries; DeepMind’s proves rich protocol-level security properties, involving an adaptive adversary, for one critical library. Both push verification down to machine code, where there is no need to trust the compiler or a high-level language semantics, and both depend on AI making very long proofs affordable.

Compute rather than labor became the constraint. A clean build of the proofs could take several hours, and early on a small source change or recompiled binary forced large proof repairs.

What the proofs do not cover

The limitations section is detailed, and anyone citing this result should read it. The headline caveats:

• No post-quantum guarantee in the computational proof. The ratchet theorems let the attacker choose SPQR’s keys, so neither proof establishes the post-quantum healing SPQR was built for.
• Primitives are assumed, not verified. Low-level cryptographic routines are specified by idealized contracts, and key generation is not verified; the theorems take keys as given.
• A narrow harness scenario. Two honest parties with fixed roles, identity keys already pinned (so Signal’s trust-on-first-use path is not exercised), one signed prekey, at most one one-time prekey, bounded message counts and sizes. One-time Kyber prekeys are not covered.
• Side channels and replay. Side channels and other secrets in memory are out of scope, and the forward secrecy theorems do not rule out a known replay-based loss of forward secrecy.
• Scope. Group messaging, sealed sender and server-side protocols are not included.

None of this undercuts the achievement, but it does mean “Signal is formally verified” overstates it. What is verified is a specific, carefully stated set of properties for one-to-one sessions of one release, under listed assumptions.

What to watch

The work is a milestone toward Signal Shot, a grand challenge launched in April 2026 by the Beneficial AI Foundation, Signal and the Lean FRO to formally verify the Signal protocol and app. Signal CTO Ehren Kret called turning live code into Lean theorems with AI agents a major breakthrough, according to DeepMind’s post.

Three things will show whether this generalizes. First, whether DeepMind follows through on its stated goal of verifying new libsignal releases before they ship, which turns verification from a one-off audit into a merge gate. Second, whether outside cryptographers find weaknesses in the 18,000 trusted lines; the full Lean development is open-sourced precisely so they can. Third, whether the approach reaches the other targets DeepMind names, such as medical device firmware and power grid software, where the specifications have no existing literature to start from.