DeepMind says AI proved key libsignal properties in Lean: about 6.5M proof lines on 26,000 trusted lines
Google DeepMind says AI agents proved key security properties of libsignal, Signal's protocol library, in Lean, about 6.5 million proof lines resting on 26,000 trusted lines (about 250 to 1, derived). The paper limits the claim to one harness build and to specifications humans must trust.
By Parminder Kumar Sharma · LinkedIn · · 26 min read
About 250 proof lines for every trusted line (derived), and what that ratio leaves out
Google DeepMind's paper AlphaProof Code: Verifying Signal's Security at the Machine-Code Level says its agents produced "about 6.5 million lines of machine-checked Lean proof code, resting on about 26,000 lines of trusted specifications and AArch64 semantics". Divide one by the other and the result is about 250 proof lines for each trusted line (derived: 6,500,000 divided by 26,000). The paper and a DeepMind post are both dated 10 November 2026; the post's page data gives 12:00 UTC. This briefing was read from 14:50 UTC on Tuesday 10 November 2026.
The ratio compares things counted differently. The paper builds the 26,000 as about 18,000 lines of code in its repository plus about 8,000 lines of AArch64 semantics, and says the first figure is about 28,000 with documentation. The 6.5 million sits inside a repository count that includes comments and blank lines. With documentation counted the trusted side is about 36,000 lines and the ratio falls to about 181 to 1 (derived). The 26,000 also leaves out items the paper's own trusted base includes: Lean's kernel, the build scripts, and the tool that extracts symbol names from the compiler's output.
What the ratio does not establish. It says how much of the checking is mechanical. It does not say that the 26,000 lines state what Signal's users need. The paper says so itself: "The specification must be trusted", and "a flaw could weaken the guarantee the theorem provides". Nor does it say that the proofs cover Signal's apps. The paper's results concern one AArch64 Linux build of a small command line harness around libsignal v0.105.4, and it reports no vulnerability in that version.
Google DeepMind builds the Gemini models the proof agents ran on, and its post names its CodeMender agent, so a result that shows agents doing verification at scale serves its interest. The paper's authors are listed at Google DeepMind and Google, and the post names Google Messages among the apps that use the Signal protocol. This briefing treats the paper as the primary source and sets the post against it.
What DeepMind published on 10 November, and who else is in the picture
The post says DeepMind researchers "guided AI agents to mathematically prove key security properties of the actual code underlying the Signal protocol". Its headline numbers are "over six million lines of Lean", human review of "just one percent of the codebase", and "just four weeks". It adds that two real, previously fixed bugs were reintroduced into an "isolated version" of the code and that the system proved the buggy version insecure. It quotes Signal's chief technology officer, which is a vendor-selected quote: the quoted words include "even greater confidence in our code's privacy guarantees".
The paper is the longer document: 57 pages by the PDF's own page count, nine authors, with the proofs described in two security models, a trusted base section, a section on the historical bugs and a related work section. Its abstract points to the Lean development at an artifact site. That site is an HTML edition of the paper, which the repository calls a reviewers' site. The repository page states an Apache 2.0 licence for the code, says libsignal code copied into it keeps its own licence (AGPL-3.0-only), and says: "This is not an official Google product." As read, the repository showed 1 commit, 38 stars and 6 forks.
Signal's part. The paper's acknowledgements thank three Signal staff and give the reason as "for their feedback on our specifications"; the post gives it as "for their feedback on our methodology". The paper also calls its result "a significant milestone towards a grand challenge launched in April 2026", which its reference list attributes to the Beneficial AI Foundation, Signal and Lean FRO under the name Signal Shot. The Signal Shot page says "Join us from April 20, 2026, to formally verify the Signal protocol and Signal app with Lean" and lists a Signal research engineer as an organising co-chair. The DeepMind post does not mention Signal Shot.
Signal's own statement. None found. Signal's blog feed as read had its newest item dated 28 September 2026 and was built on 7 November 2026; nothing in it mentions DeepMind, AlphaProof or Lean FRO. Signal's robots.txt answered 404, so no rules applied. Only the quote inside DeepMind's post speaks for Signal.
How the proof is built, and which layers a reader must trust
The paper's Figure 1 gives four parts. A specification-writing agent works with a user to turn models and properties from the literature into a Lean specification; reviewer agents critique each draft; the user approves it. The unmodified Rust is compiled with the standard compiler and the executable is loaded into Lean next to a formal semantics of AArch64. A team of prover agents proves the specification about that executable. The gatekeeper's conditions, in the paper's words, include "that the proof uses only Lean's standard axioms, and that Lean's kernel accepts the proof", and that the comparator tool confirms the statement and every definition it depends on are identical to a held-out copy of the approved specification.
The design principle is that proofs are untrusted and the specification is trusted. The paper says "since the proof is ultimately checked by the Lean kernel, the reliability of the results does not depend on the reliability of these proving agents". That is the genuine strength here: a 6.5 million line proof written by agents can be wrong in any way and still not weaken the result, because Lean rejects it. The cost is that everything a human must read sits in the specification and the assumptions.
The claim hierarchy: protocol, source and machine code
The post says previous verification stopped "at the design level" and that DeepMind went further. The paper is more precise about what is new. At the protocol level it says "Crucially, we do not aim to advance the state of the art in what has been proven about the Signal protocol". Its symbolic theorems restate earlier published ProVerif analyses of the Double Ratchet and of PQXDH in Lean. The new element, in its words, is connecting them to the machine code. There is no separate source level proof: a Lean model of libsignal that follows the Rust source sits in the middle, and the machine code is proved to match it. The paper says this removes the Rust compiler and the Rust semantics from the trusted base.
The claim hierarchy as the paper states it, with Table 1 of the paper as the source for the assumption column. Read 10 November 2026.
| Layer | What the paper proves, of what code | What it rests on, or excludes |
|---|---|---|
| Protocol design (prior work) | Not claimed as new. Symbolic results from earlier ProVerif analyses are replicated in Lean. | Idealised primitives. Prior papers' published queries were corrected where they were wrong (see below). |
| Model of libsignal in Lean | A byte-level model that follows the Rust source closely; the machine code is proved to compute exactly what it computes (Lemma 4). | The model is trusted. SPQR is modelled in Lean (spqr 1.6.0) and that model is trusted. |
| Machine code, symbolic | Ten theorems on every collision-free execution of libsignal-cli: forward secrecy and post-compromise security of message keys, handshake authentication and KCI resistance, handshake secrecy, even if a quantum attacker later breaks DH. No run faults or diverges. | Idealised hashes, KDFs and MACs; the event layer; a narrower scenario than the model. Not covered: computational secrecy, more than two parties, SPQR post-quantum healing. |
| Machine code, computational | Confidentiality and authenticity of messages, with forward secrecy and post-compromise security, for PQXDH with the Triple Ratchet, as a concrete bound on the attacker's advantage (Theorem 2). | Gap-DH and XEdDSA unforgeability, Kyber1024 collision resistance, PRF/PRG security of HKDF and HMAC, one-time CCA security of AES-CBC with HMAC. Classical attackers only. The bound is vacuous at larger scale. |
Which code? The paper verifies "the one-to-one session code of libsignal-protocol (v0.105.4, with spqr v1.6.0)", wrapped in a command line harness called libsignal-cli. Each run does one operation: keygen, init, send or recv. The theorems cover init, send and recv; "keygen is not verified". The paper's list of properties is longer than the post's one example of "keeping messages protected before and after a device is temporarily compromised": it names forward secrecy, post-compromise security, authentication, handshake secrecy, KCI resistance, session independence and harvest-now-decrypt-later resistance.
Two limits inside the proofs deserve plain statement. First, the symbolic theorems hold up to collisions: libsignal truncates its message authentication code to 8 bytes, so a guess succeeds with probability about 2 to the power of minus 64, and the paper's theorem excuses such runs rather than bounding them. Second, the computational bound grows with attacker activity and the paper says it becomes vacuous at larger scale: if nearly every message starts a new epoch, it is vacuous for single sessions of about 25,000 messages.
The trusted base, line by line
The paper defines the trusted computing base as "the code that must be audited in order to have confidence that the theorems provide the security guarantees that we claim". The table sets out what it lists, with the sizes it prints.
The trusted base as the paper prints it (sections 2.2, 4, 5.3 and 7). Sizes are the paper's; status is the paper's wording.
| Item | Size or count printed | Status in the paper |
|---|---|---|
| Lean statements and definitions | About 18,000 lines (about 28,000 with documentation). Specification directories total about 54,000 lines, only part trusted. | Trusted. Must be read by a human. |
| AArch64 semantics | 7,532 lines of Lean; 467 instructions; 31 system calls. | Trusted. Cannot be proved sound; tested against an emulator and Arm's Sail model. |
| Lean representation of the machine code | About 95,000 lines, extracted by a tool. | Checked against the executable's bytes; only the symbol names it assigns are trusted. |
| Hooked routines | 39 routines replaced by contracts, plus 18 panic entry points. | Trusted contracts. Not proved against the real routines. |
| Cryptographic assumptions | Listed in Table 1 and appendix C. | Assumed. |
| Lean kernel, extraction tool, build scripts | Not counted in the 26,000. | Trusted. |
| Rust source and compiler | Not applicable. | Not trusted. A bug in either would make the theorems false. |
The residual risk is the specification, and the paper says so. It states "while proofs are now much cheaper, specifications remain hard" and "The majority of our effort went not into proofs but into specifications". It also says "human review is not expected to detect all bugs in a large codebase", which is why it adds reviewer agents, proofs that hypotheses are satisfiable, mutation tests such as skipping the ciphertext MAC check, and the two historical bugs.
The paper gives evidence that specification work found real faults, in other people's work. It records every departure from its reference papers: "the computational catalog has over 200 entries and the symbolic one about 35". It adds "Some, however, are errors in the published analyses that we had to repair before the proofs could go through." Fifteen are gaps or bugs in a published computational analysis of the Double Ratchet. That is a point in the paper's favour as careful work and a warning that a specification copied from a peer reviewed paper is not automatically right.
The post says specifications were reviewed by "human experts reviewing every one". The paper says the user "reviews, revises, and approves the specification before any proofs are written", that agents of a different model family review drafts, and that the authors reviewed every amendment at the end of each campaign. The paper's authors are the reviewers; it names no outside specification reviewer other than the thanks to Signal staff for feedback. It also says "Complex specifications, such as ours, will take many rounds of open review and refinement to settle." That is a statement that the review is not finished.
What the paper lists as not verified
Most limitations are in the paper's own words and appear in the symbolic limitations, the computational limitations and the discussion. The table collects them. None is hidden; most are not in the post.
Out of scope or restricted, as the paper states it (sections 2.2, 4, 5.1.6, 5.2.5, 9 and appendices B.7, C.6). Read 10 November 2026.
| Not verified or restricted | What the paper says | Where |
|---|---|---|
| Group messaging, sealed sender, server side protocols | Group messaging is left as future work; extending to sealed sender and server side protocols is listed as a direction. | 3, 9 |
| Key generation | keygen is not verified; the theorems take the parties' keys as part of their setup. | 4 |
| Quantum attackers (computational) | The bounds give no guarantee against a quantum adversary. | 5.2.5 |
| Post-quantum healing by SPQR | The ratchet theorems let the attacker choose the SPQR keys, so they show no weaker than the Double Ratchet, not the healing SPQR adds. | 5.1.6, 9 |
| Side channels | Side channels and other secrets in memory are out of scope. | 5.1.6 |
| Replay based loss of forward secrecy | The forward secrecy and post-compromise theorems do not rule it out; the binary runs libsignal's deduplication but the model does not require it. | 5.1.6 |
| Scenario | Two honest parties on one device each, identity keys pinned, so trust on first use is not exercised; one signed prekey, at most one one-time prekey; one time Kyber prekeys not covered. | 5.1.6, B.7 |
| Scale | Bound vacuous for single sessions of about 25,000 messages if nearly every message starts a new epoch. | 5.2.5 |
| Hardware paths | SPQR's CPU feature probe reports no AES or PMULL, so the proofs follow the portable code paths. | C.5 |
| Programs using threads, signals, dynamic linking | The semantics does not model them, so programs that rely on them cannot be verified. | 2.2 |
| The apps' own builds | The results concern the authors' build of libsignal-cli, not Signal's own applications. | 5.2.5 |
On the last row: the paper says "the Signal apps for Android and iOS run the same Rust code for libsignal" and that its theorems "carry over to these other execution environments as long as we trust that they preserve the behavior of the protocol code". That is a conditional claim with the trust assumption stated. The paper does not say any shipped Signal binary was checked against the proofs, and it says the differences lie in compiler flags, linking and the operating system interface.
Where the post and the paper differ
The post is written for a general reader and is looser than the paper in several places. These are differences between two documents from the same publisher; neither is resolved by this site.
The post and the paper compared. Both read 10 November 2026; derived figures are this site's.
| Topic | The post says | The paper says |
|---|---|---|
| Size | Over six million lines of Lean. | About 6.5 million proof lines; nearly 7 million lines in the repository counting comments and blanks; 5.3 million about the binary, about 860,000 computational, about 350,000 symbolic (sum 6.51 million, derived). |
| Effort | Four weeks, a task that historically takes expert teams years. | The proof work was done by a team of five over four weeks (20 person-weeks, derived). seL4 took twenty person-years and CompCert six, cited as examples, not as like for like comparisons. |
| Human review | Human experts review every specification; agents flag just one percent of the codebase for a second look. | The user approves specifications; human review is not expected to detect all bugs. No percentage and no process producing one appears in the paper. |
| Which code | Down to the exact code running on devices. | The authors' build of libsignal-cli, not Signal's own applications; apps run the same Rust code, a trust assumption. |
| Models | A mix of models for specifications; agents powered by Gemini Carbon for proofs. | Specifications by agents powered by Gemini 4 Carbon and Claude Opus 5.5; proofs entirely by Gemini 4 Carbon teams. |
| Where the protocol is used | Apps like Signal and Google Messages. | Variants deployed in WhatsApp, Meta's Messenger app and Google Messages, besides the Signal app. |
| Signal's input | Feedback on our methodology. | Feedback on our specifications. |
The one percent. The post says the agents audited the proof and flagged areas for a human, "just one percent of the codebase". The paper has no such figure. A search for the word percent returns nothing in the paper or its HTML edition, and the paper describes no audit step that produces one. What the paper does describe is a gatekeeper that checks statements mechanically, a critic agent that vets spec amendments, and a human review of every amendment. If the codebase means the 6.5 million proof lines, one percent is 65,000 lines (derived), which is about 2.5 times the 26,000 trusted lines. The post does not say what codebase means, and Lean checks the proofs regardless of whether anyone reads them. The figure is unexplained, not necessarily wrong.
The four weeks. The paper confines the four weeks to the proof work and to a team of five, who each ran agents on their own workstation. Five people for four weeks is 20 person-weeks, or about 0.38 person-years at 52 weeks a year (derived), under 2 percent of the paper's seL4 figure. That compares unlike things: an operating system kernel and a compiler against one protocol library, built on an AArch64 semantics, a program logic and agent skills whose creation dates the paper does not give. It says "much of our early effort went into the skills that define the agent team", without saying when.
The word first, set against the paper's own related work
The post says "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 has three qualifiers: "the first proofs of protocol-level security properties for the unmodified code of a widely deployed implementation of a cryptographic protocol". The paper's related work cites earlier efforts and says why it counts them differently. The table gives what it says, without a verdict.
Earlier work cited in the paper's related work section, with the paper's own description. Read 10 November 2026.
| Cited work | What the paper says it did | Why the paper says it differs |
|---|---|---|
| LibSignal in F star | A verified implementation of the Signal protocol compiled to WebAssembly. | A new implementation written for verification, separate from the production libsignal. |
| s2n TLS with SAW | The deployed TLS library is continuously verified for functional correctness of HMAC, DRBG and the handshake state machine. | Neither it nor the SPQR crate proof gives protocol level security of the code. |
| SPQR crate with hax | The production Rust crate is proved panic free. | Narrower property. |
| WireGuard in Go (a cited academic project) | An end to end symbolically verified implementation, derived from the official Go code. | They modified the code, removing DDoS protection, metrics and load balancing. |
| miTLS and Project Everest; Noise star | TLS in F sharp with computational security; generated verified Noise implementations. | New implementations written for verification. |
| Concurrent AI work (xv6 on RISC-V, glibc start up on x86) | AI verification of compiled machine code. | Targets generic properties such as crash freedom or functional correctness. |
Of the two deployed code efforts it lists (s2n and the SPQR crate), the paper says: "Neither proves protocol-level security of the code." The post adds a second claim, the first use of AI to verify a widely deployed cryptographic protocol at this depth; the paper's AI related work lists concurrent efforts that it says "largely target generic properties, such as crash freedom, or functional correctness". Whether the post's broader wording matches the paper's narrower one is for the reader; the difference is plain from the two quotations.
The two bugs put back: what that test shows
The post says the team "reintroduced two real, previously fixed bugs into an isolated version of Signal's code" and that in both cases "the system produced a machine-checked proof that the buggy version was insecure". The paper's section is titled Finding Historical Bugs. It says both bugs were found earlier by published work on the Double Ratchet, and that each was injected by reverse applying its upstream fix commit to the v0.105.4 source and recompiling. The bugs are a weak state bug, where a failed prekey message was trial decrypted against an older session and left a copy of the signed prekey secret in the stored state, and a small subgroup bug, where a mangled X25519 base key was accepted. Both mechanisms are in Technical details below.
What the test shows. The specification is strong enough that the symbolic security theorem is provably false for each of those two known bugs. That is a check on the specification's strength, which the paper says is its purpose: "To check whether our specifications are strong enough to catch real bugs". What it does not show. It does not show the system would find an unknown bug; both bugs were published and fixed first, and each disproof "exhibits concrete witness inputs", which the paper does not say the agents found independently. It does not cover the computational theorem: "refuting the computational theorem is much harder", amounting to "an open problem".
No new bug is reported. The paper reports no vulnerability in libsignal v0.105.4 and no CVE. It says proof attempts that would require weakening security are "raised to a human as a potential bug" and that the authors "reviewed escalated specification issues and potential bugs". It does not say how many were escalated or what became of them. The paper's own claim is that a proof of this kind "rules out every bug or attack that would violate those properties", which is why the properties and the assumptions matter more than the absence of a finding.
Cost and compute: what is printed and what is not
Printed. A team of five over four weeks, each running agents on their own workstation. A campaign typically had 40 to 80 agents on a single machine for 24 to 72 hours, which is an upper bound of 960 to 5,760 agent hours per campaign if every agent ran throughout (derived; the paper does not say they did). A clean build of the proofs could take several hours, and the repository says a rebuild takes several hours and 15 to 34 GiB of peak memory. Proofs were produced "entirely by agent teams powered by Gemini 4 Carbon", "none of the authors wrote any proof code", and specifications used Gemini 4 Carbon and Claude Opus 5.5 (a model from Anthropic, another vendor).
Not printed. Token counts, accelerator hours, money, the number of campaigns, how many proof attempts failed, and how often agents tried to weaken a goal. The paper says "Agents under pressure to finish a goal will sometimes weaken it" and describes the countermeasures, without a count. No cost per proof line can be derived from what is printed, so the post's four weeks is the only cost figure and it is a duration of the proof work, not a cost.
Friendly labels: verified, unmodified, machine code, first
Verified here means that a Lean kernel accepted proofs of statements a human approved, about a binary whose cryptographic routines are replaced by assumptions. That is a precise and useful claim. It is not a statement about the apps, the server, the people or the keys. A label stands in for a control when a reader assumes it covers more than the specification says.
Unmodified describes the libsignal crates. It does not describe the verified executable. The paper says that executable "has each hooked routine linked as a stub of four zero bytes, which traps if executed". In other words the 39 hooked routines are not code in what was verified; they are contracts. The theorems hold for any implementation of those routines that satisfies the contracts, and the paper trusts that the real routines do. The same paragraph says the build uses "rustc's release profile with one codegen unit and panic=abort"; apps may use other flags.
Machine-code level is a strength of the approach and the paper explains it: the compiler is not trusted. The price is that the proof is about one compiled artifact. A different compiler version or flag set is a different binary (this site's inference), and the paper says "a new build of libsignal-cli needs a new refinement proof" though not a new security proof.
What is established, and what is not
What the post and paper establish, and what they do not, read 10 November 2026. Items marked none found were searched only on the pages named in the sources list.
| Topic | Stated | Not stated |
|---|---|---|
| Independent replication | Artifacts open sourced under Apache 2.0; rebuild takes several hours and 15 to 34 GiB of memory; comparator check supported on Linux only. | Any third party rebuild or review. None found on the pages read. |
| Other Signal components | One to one sessions of libsignal v0.105.4 with spqr v1.6.0, init, send and recv. | Groups, sealed sender, server, key generation, the apps. |
| Vulnerabilities | Two historical bugs reintroduced and disproved symbolically. | Any bug found in current libsignal. None reported. Count of escalated potential bugs. |
| Security of deployed apps | Apps run the same Rust code; results carry over if behaviour is preserved. | Any shipped binary checked against the proofs. |
| Specification fidelity | Author review, reviewer agents, vacuity checks, mutation tests, two historical bugs, Signal staff feedback. | Independent specification review. The paper itself says review is not expected to find all bugs. |
| Cost | Team of five, four weeks, 40 to 80 agents per campaign for 24 to 72 hours. | Tokens, accelerator hours, money, number of campaigns, failed attempts. |
| Signal's own statement | A vendor selected quote in the DeepMind post. | Any statement on Signal's blog feed as read (newest item 28 September 2026). |
| Other software | The post names medical device firmware and power grid software as future systems. | Anything about either in the paper. Its semantics excludes threads, signals and dynamic linking. |
What a security reader should take from it, in order
Take this with you
This site's suggestions, except where marked as the paper's
- Ask any vendor claiming verified code for the specification and the trusted base, not the proof size. A proof count measures agent effort; the trusted lines measure what a person must believe.
- Name the layer: design, source or machine code. Ask which binary was checked, built how, and whether it is the one you run.
- Read the exclusions before the claims. Here the paper's own limitation sections list groups, key generation, side channels, quantum attackers, scale and the apps' builds, and make a good template to ask any vendor for.
- Treat verified as relative to a specification. Ask who reviewed it other than its authors and whether that review is public.
- Check the licence and whether the proof can be rebuilt by you. Here: Apache 2.0 for the code, several hours and 15 to 34 GiB to rebuild, comparator on Linux.
- Budget for specification review. The paper reports that most of its effort went into specifications, and that complex specifications need many rounds of open review (the paper's own statement).
- Keep testing, fuzzing and code review. Formal verification complements them; a proof about one binary under stated assumptions does not replace them.
- For this result, treat it as a vendor claim until a third party rebuilds the proofs and reviews the specifications, and watch for Signal's own statement.
Technical details
This is a verification paper, not an intrusion report. It prints no vulnerability, CVE, exploit, hash or network indicator for current libsignal. What it prints, and what a defender or reviewer can use, is below: versions and build settings, the line counts, the central definitions in words, the scenario script the authors give, the two historical bug descriptions, and the artifact's rebuild commands. Every block is copied from the source named in its caption. The paper's theorem statements are typeset mathematics that do not survive plain text, so they are described above rather than reproduced.
Versions and build settings. This block is what to compare against any binary you hold: the library and crate versions, the compiler, the link, the release profile and the fact that the hooked routines are four byte stubs in the verified executable. A defender asks whether the app build they run matches any of it.
Paper, as printed (sections 4 and C.6):
libsignal-protocol (v0.105.4, with spqr v1.6.0)
stock rustc (1.98.1) and link them statically with musl into one AArch64 Linux executable
rustc's release profile with one codegen unit and panic=abort, linked at a fixed base address
each hooked routine linked as a stub of four zero bytes, which traps if executed
in our process model, which gives each run 1 GiB of memory beyond its loaded segments and an 8 MiB stack
a run exits with code 2 if its standard input exceeds 220 bytes, and send rejects plaintexts longer than 106 bytes
Repository page, as printed:
lean-toolchain pins leanprover/lean4:v4.34.0
Rust 1.98.1
pinned in rust-toolchain.toml
LLVM ld.lld 22.1.8
Zig 0.16.0 on PATH
Line counts, as printed. The derived lines at the end are this site's arithmetic. Use them to see which counts the 250 to 1 ratio mixes.
The repository contains nearly 7 million lines of Lean, counting comments and blank lines.
About 6.5 million of them are proofs: 5.3 million about the binary, which both security proofs share, about 860,000 for the computational proof and about 350,000 for the symbolic proof.
Another 140,000 lines prove the reintroduced bugs (§6), and 70,000 verify the allocator.
The verified libsignal code is about 560 KB, about 140,000 AArch64 instructions.
The semantics covers 467 instructions and 31 system calls in 7,532 lines of Lean.
Reading every definition that our headline theorems depend on means reading about 18,000 lines of code in the repository (about 28,000 with documentation), plus about 8,000 lines of the AArch64 semantics and a Lean representation of the compiled machine code (about 95,000 lines)
The remaining 39 hooked routines are replaced by contracts at the binary boundary, and 18 panic entry points end the run with SIGABRT.
Derived by this site (not from the paper):
6,500,000 / 26,000 = 250 (proof lines per trusted line)
6,500,000 / (28,000 + 8,000) = about 181 (with documentation counted)
5,300,000 + 860,000 + 350,000 = 6,510,000
6,500,000 / 140,000 = about 46 (proof lines per AArch64 instruction)
The central definitions in words. ElfRunsTo is the statement every theorem rests on: all runs of the executable from inputs satisfying a precondition end in an outcome satisfying a postcondition and never fault. The exit code semantics define what the harness does on success and on rejection.
The central definition, ElfRunsTo bin pre post, states that every run of bin from inputs satisfying pre ends in an outcome satisfying post, and that no run faults, for instance by reading unmapped memory.
Exit code 1 means that libsignal rejected it, and then no file is written
(Exit code 2 reports a malformed command line or an unreadable file.)
Our theorems cover init, send and recv; keygen is not verified, and the theorems instead take the parties' keys as part of their setup.
The authors' scenario script. It plays both the environment and the attacker: two parties, a handshake, two messages, and a replay of the first message that Bob rejects. The authors also ran such scenarios on their Lean semantics of the binary, 15.6 million instructions across 10 invocations, with every run matching the real binary. A reviewer can use it to run the harness; it contains no attack.
ALICE=8a6f1c2e-3b4d-4e5f-9a0b-1c2d3e4f5a6b.1 BOB=5d3e2f10-7a8b-4c9d-8e0f-a1b2c3d4e5f6.1
mkdir alice bob
run bob keygen $BOB 1
run alice keygen $ALICE 0
bundle bob bob_public_bundle
run alice init $BOB ../bob_public_bundle
printf "Hi Bob!" | run alice send $BOB > m1
run bob recv $ALICE < m1
printf "Hi Alice!" | run bob send $ALICE > r1
run alice recv $BOB < r1
run bob recv $ALICE < m1; echo $?
# the paper's comments: m1 is a PreKeySignalMessage; r1 is a SignalMessage; the last line replays m1, prints 1 and writes no file
The two historical bugs. These are the two fixed libsignal bugs the paper reintroduced to test its specification. They are published and fixed; the commit identifiers are upstream fix commits, not indicators of compromise.
Weak state [40, §3.2.1], fix cd36118: a prekey message that fails to decrypt on its new session is trial-decrypted with older sessions, and if that succeeds the new session's unconfirmed state, which holds a copy of the signed prekey secret, is stored.
Small subgroup [40, §3.2.2], fix 5293caa: the PQXDH responder does not check that the initiator's X25519 base key is torsion-free and in range, so a replayed handshake with a mangled base key creates a second session with the same shared secret.
Rebuilding the proofs. The repository lists these commands. The page says the full build takes several hours and about 15 to 34 GiB of peak memory, and that the comparator check is supported on Linux only. This is what a third party would run to replicate the result; the hunt here is for whether anyone has.
lake exe cache get
lake build
./scripts/cli-elf-stock --stdbin --build
./scripts/cli-elf-stock --stdbin --verify-pin --lean-mod LibsignalBinary/Specifications/SignalSession/CliElf.lean
lake build CliElfLib
lake script run checkCliElfOwner
comparator/install-tools.sh
comparator/run.sh
# artifact: google-deepmind.github[.]io/code-verification and github[.]com/google-deepmind/code-verification
The question the result leaves open
Lean can show that 6.5 million lines of proof follow from 26,000 lines of statements and assumptions. It cannot show that those statements describe what Signal's users are owed, and the paper says as much about its own specification. So who, outside the authors and a few Signal staff, has read the 18,000 lines of definitions and the 8,000 lines of semantics, and what did they find?
Key facts
Sources
- PrimaryAlphaProof Code: Verifying Signal's Security at the Machine-Code Level, technical paper dated 2026-11-10, 57 pages: claims, trusted base, limitations, bug test, related work. Read in full. Google DeepMind builds Gemini and names its CodeMender agentGoogle DeepMindaccessed 2026-11-10
- PrimaryIntroducing AlphaProof Code: a breakthrough in verifying complex software at depth, 10 November 2026 by page data: the post's claims, set against the paper. Read in fullGoogle DeepMindaccessed 2026-11-10
- PrimaryHTML edition of the paper (a reviewers' site per the repository): used to check superscripts and quotations. Read as savedGoogle DeepMindaccessed 2026-11-10
- Primarygoogle-deepmind/code-verification repository page: licence, toolchain versions, rebuild commands, time and memory, stars and forks as read. Read the page, not the filesGoogle DeepMind (GitHub)accessed 2026-11-10
- PrimarySignal Shot page: the April 2026 initiative the paper cites, its stated aim and organisers by role. Read in fullBeneficial AI Foundationaccessed 2026-11-10
- PrimarySignal blog feed, built 7 November 2026: read to look for a Signal statement on this work; none foundSignal Messengeraccessed 2026-11-10
