# 6.5M lines of Lean: I counted DeepMind's Signal proofs > Source: > Published: 2026-11-11 00:45:39+00:00 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`. 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 `axiom` s. 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 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. 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. 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 (` comparator/ComparatorChallenge/` — six files with 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 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.