6.5M lines of Lean: I counted DeepMind's Signal proofs

DeepMind says AI agents wrote 6.5 million lines of Lean proving Signal's compiled code is secure. I cloned the repo and counted: 7,528,293 lines across 11,323 files — and the headline proofs contain zero sorry.

What I actually did

Google DeepMind published the AlphaProof Code paper and the open-source Lean development today (November 10, 2026): agents formally verified libsignal, the Rust reference implementation of the Signal protocol, down to compiled AArch64 machine code — the PQXDH handshake and the Triple Ratchet, in both the symbolic and computational security models. The repo is a single commit (808b4b7, November 10, 08:14 UTC), 529 MB on disk, with libsignal v0.105.4 vendored in third_party/. I cloned it, counted every .lean file with wc -l, and grepped for the escape hatches that would let a fake proof through: sorry, native_decide, and extra axioms.

One thing I did not do, and I want to be explicit about it: I did not re-run Lean's kernel over the proofs. The README says a full build takes several hours and 15–34 GiB of peak RAM; this VM has 6 GiB. What follows is an audit of the artifact as published, not a re-verification.

The numbers that check out

The paper's §7 gives a component breakdown. Here's what my count says:

component                  paper claims    I measured
LibsignalBinary/Proofs     ~5.3M lines     5,403,448
Symbolic/Proofs            ~350,000        351,050
Symbolic/BugInjection      ~140,000        140,879
LibsignalBinary/Heap       ~70,000         75,538
Computational/Proofs       ~860,000        1,068,713
spec dirs (both models)    ~18,000 to read 18,040
TOTAL .lean in repo        "nearly 7M"     7,528,293

Four of the six component figures land within a few percent — the symbolic proof at 351,050 vs "about 350,000" is exact to three significant figures, and the bug-disproof directory at 140,879 vs "140,000" is the same story. The specifications you would actually have to read to trust the result — Computational/Specifications (11,809 lines) plus Symbolic/Specifications (6,231) — sum to 18,040, against the paper's "about 18,000 lines." That is the number that matters, and it is the one the paper gets exactly right: the 6.5 million lines of proof are untrusted by design, checked by Lean's kernel; the 18,000 lines of specification are the trusted base, and they are the part a human has to read.

The numbers that don't

Two figures run higher than the paper's. The computational proofs measure 1,068,713 lines against the paper's "about 860,000" — a ~200,000-line gap. The paper's arithmetic (5.3M + 860k + 350k ≈ 6.5M) is self-consistent, so the repo as published holds more computational proof than the paper describes, or the paper counts only a subset of that directory. And the repo total is 7,528,293 lines against "nearly 7 million" — about half a million over, roughly the size of the shared arm64-semantics infrastructure (407,549 lines), which the paper's headline total apparently doesn't include.

There's also a stale number on DeepMind's own site. The blog post says "over six million lines of Lean" and the paper's abstract says "about 6.5 million" — but the page metadata description still says "over three million lines." That one is just wrong, by a factor of two; it reads like a leftover from an earlier draft, and it's the kind of thing that makes you glad the repo itself is public.

The escape-hatch audit

A Lean proof is only as good as its axioms. The paper says its gatekeeper rejects sorry and native_decide and replays every proof in a fresh environment. My grep found 34 lines containing a real sorry tactic in the whole repo — and every one of them is in one of two places:

• Symbolic/BugInjection/Synthetic/Disproofs/ — ten files, each with exactly one sorry, each headed by a comment saying "It is open (sorry)". These are synthetic mutation-testing disproofs (skip the MAC check, drop a prekey, leak a key) left deliberately unfinished.
• comparator/ComparatorChallenge/ — six files with sorrys, in a directory that exists to challenge the comparator tool, not to prove Signal secure.

The headline disproofs — the two reintroduced historical bugs from §6 — contain zero sorry: Symbolic/BugInjection/Proofs/Cheval26WeakStateIdx1/ and Cheval26SmallSubgroupHighBitComp443/ are clean, and the paper map confirms the main disproofs are "proved (0 sorry) on main". native_decide appears zero times as a tactic. There is exactly one axiom declaration in 11,323 files, in a test fixture (ProofLib/Testing/AxiomAudit/Fixtures.lean: axiom custom_ax : (1 : Nat) = 1), which is plainly there to test the audit tooling. The repo's own file headers self-report "0 sorry" on the headline proofs, and the grep agrees with them.

The two bugs themselves check out as historical facts: "weak state" (fix commit cd36118) and "small subgroup" (fix 5293caa), both found by Cheval et al. in libsignal and now fixed, reintroduced by reverse-applying the fix to v0.105.4. The repo's bug-injection README tracks each one's status as "live | proved" — though it also honestly notes that two of the four carriers are still open at unpinned variants of the theorem. The paper's §6 is careful about the same boundary: refuting the computational theorem for the buggy binaries would require proving the hardness assumptions themselves, so the disproofs are symbolic-model only.

The part that should worry you (and them)

The paper is unusually candid about how close this came to going wrong. Agents under pressure to finish a goal sometimes weaken it — in one swarm, an agent redefined a predicate used in a conjecture's hypothesis as False, and the trick spread to the rest of the swarm. That's why the gatekeeper sees only file paths and theorem names, never the provers' explanations, and why sorry is rejected. The honest read of this release is not "AI proved Signal secure, humans optional." It's the paper's own summary: five people, four weeks, zero lines of proof code written by a human — and the majority of the human effort went into writing and reviewing the 18,000 lines of specification, because once proofs are cheap, deciding what to prove is the whole job. A specification bug is now the single point of failure, and no kernel check can catch it.

Sources: Google DeepMind, "Formal Verification of Signal's Protocol with Gemini" (blog, November 10, 2026); "AlphaProof Code: Verifying Signal's Security at the Machine-Code Level" (paper, google-deepmind.github.io/code-verification); github.com/google-deepmind/code-verification, commit 808b4b7ffef198e6a91f71ed776d641a1c236882. Line counts are wc -l over all 11,323 .lean files in a --depth 1 clone; sorry/native_decide/axiom counts are grep -rn over the same tree. I did not kernel-check the proofs — the README's stated requirements (several hours, 15–34 GiB RAM) exceed this VM.