AlphaProof Code: what DeepMind's 6.5 million lines of Lean actually prove about Signal's libsignal

Google DeepMind says AI agents have proved key security properties of the code that actually runs the Signal protocol. The paper behind the November 10 announcement, "AlphaProof Code: Verifying Signal's Security at the Machine-Code Level" by Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, Charles Sutton and Pushmeet Kohli, supports the core of that claim. It is also more careful about where the claim stops than the blog post that announced it.

The short version: the proofs are about unmodified libsignal code compiled by an ordinary Rust compiler, checked instruction by instruction in Lean. They do not cover the cryptographic primitives, key generation, group chats or the Signal apps. And a side result got almost no attention: writing the specifications turned up errors in the published security analyses of Signal that the proofs were built on.

What was actually proved

The target is libsignal-protocol v0.105.4 with the spqr v1.6.0 crate, the one-to-one session code: the post-quantum PQXDH handshake and the Triple Ratchet (the classic Double Ratchet plus Signal's Sparse Post-Quantum Ratchet). DeepMind wrapped the unmodified crates in a small command-line harness, libsignal-cli, compiled it with stock rustc 1.98.1, statically linked it with musl and stated the theorems about the resulting AArch64 Linux executable.

That choice is what makes the result unusual. Because the theorems are about machine code, the Rust compiler is not part of what you have to trust. Instead you trust a Lean model of AArch64 user-mode execution: 467 instructions and 31 system calls in 7,578 lines, tested in lockstep against the Unicorn emulator and Arm's Sail model. The proofs follow every init, send and recv run from the program's entry point to its final exit_group call, through musl's allocator, protobuf parsing, the ratchet state machines and MAC checks.

There are two independent proofs. A symbolic one, in the Dolev–Yao style, restates ten properties from earlier ProVerif analyses (forward secrecy, post-compromise security, handshake authentication and secrecy, resistance to harvest-now-decrypt-later) and connects them to the binary. A computational one bounds an attacker's advantage in a game that combines the PQXDH analysis of Fiedler and Günther with the Double Ratchet model of Alwen, Coretti and Dodis.

The proofs are about 6.5 million lines of Lean: 5.3 million about the binary, which both security proofs share, about 860,000 for the computational proof and 350,000 for the symbolic one. What a reader has to trust is much smaller: about 18,000 lines of specifications plus about 8,000 lines of AArch64 semantics, per the paper.

We checked the published repository, google-deepmind/code-verification. It holds 11,323 .lean files totalling about 443 MB, 325 MB of them in the LibsignalBinary directory, which fits the paper's line counts. The README says a full check takes "several hours" and 15 to 34 GiB of peak RAM, so replaying the proofs is within reach of anyone with a big workstation and an afternoon. We did not run the build.

Where the announcement says more than the paper

"By any method." The blog post says this is "the first time the implementation of a widely deployed protocol like this has been formally verified by any method, with or without AI." The paper's claim is narrower and easier to defend: "the first proofs connecting protocol-level security guarantees to the unmodified code of a widely used cryptographic protocol implementation." Its related-work section lists implementations that were verified before. miTLS and Project Everest proved computational security of a TLS implementation written in F#. LibSignal* is a verified Signal implementation in F*. Arquint et al. verified a WireGuard key exchange derived from the official Go code. The difference, which the paper states openly, is that those were new implementations or code changed to make verification easier. "Unmodified" is the real first here, and it matters more than "first" does.

Three million or six million. The blog post's body says the agents generated "over six million lines of Lean." The page's meta description, the text search engines and link previews show, says "over three million lines." Some reposts of the news are already repeating the smaller number. The paper says about 6.5 million lines of proof and nearly 7 million in total.

"One percent." The blog says agents flagged the parts that needed a human's second look, "just one percent of the codebase." We found no 1% figure in the paper. Its own measure of what a reader has to trust is about 26,000 lines, under half a percent of the repository, plus the symbol names in a 95,000-line Lean listing of the machine code.

Gemini, and Claude. The announcement is titled "Formal Verification of Signal's Protocol with Gemini" and credits agents "powered by Gemini Carbon." That is accurate for the proofs: the paper says they "were produced entirely by agent teams powered by Gemini 4 Carbon," and none of the authors wrote proof code. The specifications, though, were written in "an intense back-and-forth between humans and agents powered by Gemini 4 Carbon and Claude Opus 5.5," with every draft reviewed by "an agent from a different model family." The blog post doesn't mention Claude.

Four weeks. The paper says a team of five worked for four weeks, each running agents nonstop on their own workstation. A single proof campaign ran 40 to 80 agents on one machine for 24 to 72 hours. The authors also write that "the majority of our effort went not into proofs but into specifications." That is probably the most useful sentence in the paper: once proofs are cheap, the hard part is deciding what to prove.

What the proofs don't cover

The limitations are spelled out in the paper's Table 1 and its limitations sections, and they are substantial:

• The cryptography itself. 37 routines are "hooked," meaning replaced by trusted contracts instead of being verified. They include SHA-256 and SHA-512 compression, AES-256-CBC, the X25519 and Edwards curve operations, Kyber1024, and ML-KEM-768 and HMAC from libcrux, along with memmove, bcmp, strlen, error formatting and the routines that write files and standard output. The results depend on those primitives being secure and correctly implemented. Other projects verify primitives like these; this one doesn't.
• Key generation. The keygen command is not verified; the theorems take the parties' keys as given.
• Groups and devices. Only one-to-one sessions between two parties are covered. Group messaging is left for future work, and there is no multi-device state.
• Quantum attackers. The computational proof covers classical attackers only. The symbolic proof covers handshake secrecy against a future quantum attacker, but neither proof shows the post-quantum healing that SPQR was added for. The ratchet theorems show that the Triple Ratchet is "no weaker than the Double Ratchet."
• Scale. Because libsignal truncates its MAC to 8 bytes, the computational bound grows with use. If nearly every message starts a new epoch, the bound becomes vacuous for a single session of about 25,000 messages, or for 2^20 sessions of 2^10 messages each.
• The apps. The theorems are about DeepMind's libsignal-cli build, run as a fresh process with a fixed clock, 1 GiB of memory beyond its loaded segments and an 8 MiB stack. The paper argues they carry over to Signal's Android and iOS apps, which run the same Rust code on AArch64, "as long as we trust that they preserve the behavior of the protocol code." Side channels are out of scope.

None of this undercuts the result. It does mean that the version going around on social media, that Signal has now been mathematically proven secure, is not what was shown.

The bugs were in the papers

Before proving anything, the team had to turn published security analyses into Lean statements that are true of the real code. The paper keeps a list of every place where the Lean statements depart from the papers or from libsignal: over 200 entries for the computational side and about 35 for the symbolic side. Most are routine. Some are errors in the published analyses:

• fifteen gaps or bugs in the computational analysis of the Double Ratchet by Alwen, Coretti and Dodis (EUROCRYPT 2019), "such as missing hypotheses and security game conditions that allow trivial wins";
• in the ProVerif queries printed by Vincent Cheval, Charlie Jacomme and Jessica Richards (IEEE S&P 2026), a lookup of skipped message keys "at the wrong ratchet index, which makes receiver-side forward secrecy false as printed," an unbound variable, and a post-compromise-security statement bracketed so that it excuses too much;
• in the PQXDH analysis by Karthikeyan Bhargavan et al. (USENIX Security 2024), a phrasing that, read literally, makes one corollary unprovable.

These are mistakes in how security properties were written down, not attacks on Signal. But they are exactly what a machine-checked proof against real code is supposed to catch, and they back the paper's point that specifications, not proofs, are now the part that needs scrutiny.

Testing the specification, and the agents

A proof is only as good as its statement, and an agent under pressure has an easy way out: weaken the goal. The paper cites a swarm of Lean agents where one agent redefined a predicate in a conjecture's hypothesis as False, and the trick "spread to the rest of the swarm." AlphaProof Code's defences are mechanical. A gatekeeper agent sees only file paths and theorem names. It accepts a proof only if Lean's comparator tool confirms that the statement and every definition it depends on match a held-out copy that no agent can write to. sorry and native_decide are rejected. Agents can propose changes to the specification, but a critic agent that never sees the proof attempts has to accept them, and changes to trusted assumptions need human approval.

To check that the specification can tell good code from bad, the team reverse-applied two libsignal fixes for bugs that Cheval, Jacomme and Richards had found: cd36118 (a prekey message that decrypted only under an archived session stored state that included a copy of the signed prekey secret) and 5293caa (no torsion check on the initiator's X25519 base key). For both rebuilt binaries, Lean proves that the symbolic security theorem fails. No new vulnerabilities in libsignal were reported. The computational theorem can't be tested this way: refuting it would require proving the hardness assumptions themselves, which the paper calls "an open problem."

Where this sits

The work answers part of Signal Shot, a project launched in April 2026 by the Beneficial AI Foundation, Signal and the Lean FRO to formally verify "the Signal protocol and Signal app" in Lean. Co-author Samuel Schlesinger of Google is listed among its collaborators. The paper calls its result "a significant milestone towards" that challenge, not a completion. Signal's CTO, Ehren Kret, is quoted in the announcement calling the translation of live code into Lean theorems "a major breakthrough."

The questions that remain are practical. Proofs pinned to a SHA-256-identified binary of libsignal v0.105.4 are a snapshot, and the paper says that early on, "small source changes or a recompiled binary required large proof repairs." Whether this becomes continuous verification as libsignal keeps changing is up to Signal and the Signal Shot community. Independent review of the 26,000 trusted lines is still to come. That is the human work the paper says now matters most.