AlphaProof Code and Signal: what the machine-code proofs cover

Google DeepMind’s AlphaProof Code did not prove that Signal is secure. It proved something narrower and, by its authors’ account, without precedent: a set of machine-checked security theorems about the compiled AArch64 machine code of one build of libsignal, Signal’s reference Rust implementation. People chose what to prove, approved every trusted statement and adjudicated changes to it. AI agents wrote all of the proofs, about 6.5 million lines of Lean. Lean’s kernel, not a human reader, checked those proofs.

That division is the key to the “one percent” figure in DeepMind’s November 10 announcement. Human review was not a one percent sample of the agents’ proofs. It was concentrated on the part of the project that cannot be checked automatically: the statements themselves, the model of the processor and the assumptions about code that was left out. The technical paper puts that trusted layer at about 26,000 lines.

The guarantee has hard edges. It covers one-to-one sessions in a command-line harness built from libsignal v0.105.4, with cryptographic primitives replaced by contracts, under two standard models of protocol security. It does not cover group messaging, the Signal apps as shipped, side channels, later libsignal releases or a computational guarantee against quantum attackers. The Frontier Wire has not rerun the proofs. This reconstruction is based on the announcement, the paper, the published repository and an account from the Beneficial AI Foundation, which runs a parallel effort to verify Signal.

TL;DR

• Humans approved the trusted statements; agents powered by Gemini 4 Carbon wrote every proof; Lean’s kernel checked them against a held-out copy of the approved specification.
• The paper never says “one percent”; the figure best matches the trusted base, about 18,000 lines of statements and definitions plus about 8,000 lines of AArch64 semantics, against about 6.5 million proof lines.
• The theorems concern a compiled libsignal v0.105.4 harness, not the Signal apps, and rest on idealized cryptography and, in the paper’s version, contracts for 39 routines.
• Two previously fixed libsignal bugs, reinserted, produced binaries that provably violate the symbolic security theorem.

Dates, versions and who reported what

Several dates matter here and they are easy to blur. The announcement and the paper are both dated November 10, 2026. The verified code is libsignal v0.105.4, which GitHub’s release record shows as published on October 22, 2026 (GitHub timestamps here are UTC). The paper pairs it with the SPQR crate at v1.6.0. The paper says the proof work took “a team of five over four weeks”. It does not say which four weeks.

Almost every quantitative claim in this article is reported by DeepMind’s authors about their own work: line counts, agent counts, run times and the outcome of the bug tests. Where a figure is The Frontier Wire’s own arithmetic on those numbers, it is labelled as such.

The table yields one observation the paper does not address. The verified release was published 19 days before the announcement, which is shorter than the four-week effort. The paper notes that early in the project “a recompiled binary required large proof repairs”, which suggests the target was updated during the work. That is an inference from the timeline, not something the authors state.

The verification target is a harness, not an app

DeepMind did not state its theorems about the Signal application or about the Rust source code. It wrapped the unmodified libsignal crates in a small command-line program, libsignal-cli, compiled it with the stock Rust compiler (rustc 1.98.1), statically linked it with the musl C library and stated theorems about whole runs of the resulting AArch64 Linux executable.

Each run performs one operation for one party. init starts a session from a prekey bundle (the set of public keys a user leaves on the server so others can contact them while they are offline), and send and recv encrypt or decrypt one message. A fourth operation, keygen, creates keys but is not verified: the theorems take the parties’ keys as part of their setup. A party’s entire state lives in a directory of files, so in the model, stealing that directory is exactly a full compromise of the party.

The paper puts the verified code at about 560 KB, roughly 140,000 AArch64 instructions. The proofs reason instruction by instruction about the harness, its file-backed stores, musl’s mallocng memory allocator, the PQXDH handshake, the Triple Ratchet and SPQR state machines, key derivation, protobuf serialization and MAC verification.

Some code is not verified. The paper lists 39 “hooked” routines that are replaced by contracts, trusted descriptions of what the routine does, rather than executed. They include the low-level cryptographic primitives (SHA-256 and SHA-512 compression, AES-256-CBC, X25519 and Edwards curve operations, Kyber1024, ML-KEM-768 and HMAC from libcrux), five libc memory and string routines, the two functions that write files and standard output, and a few small Rust library routines. Another 18 panic entry points simply end the run.

That count has already moved. On November 11 the repository’s maintainers merged a pull request that verifies the machine code of 10 more library routines, including memmove, bcmp, strlen, memrchr, UTF-8 checking and the zeroizing destructors, instead of trusting contracts for them. The pull request describes the change as “37 → 27” hooked routines. It does not explain the difference from the paper’s count of 39. According to the pull request, the 27 that remain are the 23 low-level cryptographic primitives, two Rust error-formatting routines and the two output functions. The headline theorem statements are unchanged, the bug disproofs still go through, and the pinned binary has a new SHA-256 hash because the newly verified routines are now linked in as real code.

Verifying machine code rather than source has a specific payoff. The paper states that the Rust compiler is not trusted: a compiler bug that broke a stated security property would make the theorem false, and the proof would fail. Source-level Rust verifiers, the authors note, trust rustc, LLVM and a model of Rust’s semantics. The cost is that a large share of the proofs concerns registers, stack frames and memory layout.

The theorems are tied to a precise environment: a fresh single-threaded process, 1 GiB of memory beyond the loaded segments, an 8 MiB stack, a fixed clock, and all randomness drawn from a file. The paper argues that the results are relevant to the Android and iOS apps, which run the same Rust code on AArch64, but only “as long as we trust” that those environments preserve the protocol code’s behavior as exercised by the harness. That bridge is argued, not proved.

Who did what in the workflow

AlphaProof Code splits the work into roles, each defined by a “skill”, a natural-language document describing an agent’s task, sources and required checks. The table below reconstructs the division of labor from sections 2 and 7 of the paper. It is The Frontier Wire’s synthesis, and the trust column follows the paper’s own shading of trusted and untrusted components.

The paper names the models. Specifications were developed “through an intense back-and-forth between humans and agents powered by Gemini 4 Carbon and Claude Opus 5.5”, with a reviewer from a different model family than the drafter. Proofs were “produced entirely by agent teams powered by Gemini 4 Carbon”, and “none of the authors wrote any proof code”. A typical proof campaign ran 40 to 80 agents on a single machine for 24 to 72 hours.

The authors also describe a role that is easy to miss: building the agent team itself. Much of the early effort went into the skills, which they “developed iteratively by watching campaigns run”. Monitoring took a lot of human time at first and dropped as the skills matured. A clean build of the proofs could take several hours.

What the humans specified

The paper’s central claim about method is that “the majority of human effort in software verification now lies in engineering the specification”. A specification here is the set of theorem statements plus every definition they depend on: the model of the attacker, the model of the processor, the contracts for unverified routines. It has to be trusted, because a flaw in it weakens the guarantee without any proof failing.

For Signal, the humans did not invent new security definitions. They adapted established ones. The symbolic side restates the PQXDH theorems of Bhargavan and colleagues and the Double Ratchet theorems of Cheval, Jacomme and Richards, both originally proved with the ProVerif tool. The computational side combines a PQXDH game from Fiedler and Günther with a secure-messaging game from Alwen, Coretti and Dodis. Those prior analyses treated the handshake and the ratchet separately and predate Signal’s post-quantum ratchet, so the specifications had to compose them and extend them to the protocol as deployed.

That work found problems in the published analyses. The authors kept a log of every place where the Lean statements depart from their reference papers or from libsignal: over 200 entries on the computational side and about 35 on the symbolic side. Most are routine. Fifteen, according to the paper, are gaps or bugs in the computational analysis of the Double Ratchet, such as missing hypotheses and game conditions that allow trivial wins. On the symbolic side, the paper reports that the printed ProVerif queries of Cheval and colleagues look up skipped message keys at the wrong ratchet index, which makes receiver-side forward secrecy false as printed. These are author-reported findings; The Frontier Wire has not seen responses from the original authors.

The humans also had to keep the specification strong. A theorem with overly restrictive assumptions can hold even for buggy code. The paper describes four checks: skeptical reviewer agents; proofs that a theorem’s hypotheses can actually be satisfied, so it is not vacuously true; mutation testing, in which agents insert plausible bugs such as skipping MAC verification and prove the security theorem then fails; and the historical-bug test described below.

What the agents proved

There are two independent proofs, because the two standard models of protocol security give different assurances.

The symbolic proof

In the symbolic (Dolev-Yao) model, cryptographic primitives are perfect black boxes: hashes never collide, ciphertexts cannot be read without the key, signatures cannot be forged. The attacker controls the network and can compromise long-term keys, prekeys or session state, and may later break Diffie-Hellman, as a future quantum computer might, or the KEM.

Using DyLean, a Lean framework for symbolic protocol analysis, the agents proved ten theorems of a composed PQXDH and Triple Ratchet model: forward secrecy and post-compromise security of message keys, initiator and responder secrecy, authentication, and five PQXDH corollaries including resistance to key-compromise impersonation and “harvest now, decrypt later” attacks. They then proved that every run of the binary is explained by a run of the model, up to collisions, so the ten properties carry over to the machine code.

The collision clause matters. Real bytes are finite. libsignal truncates its MAC to 8 bytes, so an attacker who guesses it, with probability 2^-64 per attempt, gets a forged message accepted. The symbolic theorem excuses such collisions and gives guarantees only on the trace before one occurs. Bounding the probability of a collision is, in the paper’s words, “a computational question, outside Lean”. The theorem also assumes fresh randomness; with a cryptographically secure generator that assumption fails with probability about k²/2^251 over k draws.

The computational proof

The computational model treats messages as bit strings and the attacker as any efficient probabilistic algorithm with a bounded number of queries. The goal is a concrete bound: the attacker’s advantage against the compiled executable is at most a sum of advantages of efficient reductions against named assumptions, such as Gap Diffie-Hellman, XEdDSA unforgeability and HKDF and HMAC behaving as pseudorandom functions, plus statistical terms.

The paper took care that “there exists a reduction” cannot be satisfied trivially. Reductions are written in a small embedded language with a cost semantics, so a “reduction” that simply searches for the secret key or hard-codes a table is ruled out. Two assumptions are non-standard because libsignal uses one Curve25519 key for both Diffie-Hellman and signatures; the paper proves in Lean that both reduce to standard Gap-DH when SHA-512 is modeled as a random oracle.

The bound has limits that the paper states directly. It gives no guarantee against a quantum adversary. If nearly every message starts a new ratchet epoch, the statistical terms make it vacuous for a single session of about 25,000 messages, or for 2^20 sessions of 2^10 messages. The adversary cannot inject its own initial handshake message to the responder of a session that is later promoted to messaging, which the paper calls the most significant restriction.

What “one percent” means

The blog says the agents “audited the proof and highlighted areas that needed a second look by a human”, amounting to “just one percent of the codebase”, and that “because Lean automatically checks the rest, our experts could focus their review where human judgment matters most”. The paper does not use the phrase “one percent”. It gives the underlying numbers instead.

By The Frontier Wire’s arithmetic, 26,000 trusted lines is about 0.4 percent of 6.5 million proof lines, and 54,000 specification lines is about 0.8 percent of a 7 million line repository. Either figure is consistent with “one percent” as a rounded description. In The Frontier Wire’s reading, the blog’s framing of agents highlighting areas corresponds most closely to the paper’s statement that every specification file is marked as trusted, trusted in part or checked by Lean. Neither document spells out the link.

Two things follow. First, the human review was not a sample. People were not spot-checking one proof in a hundred and trusting the rest; they were reading the part that defines what the proofs mean, and relying on Lean for everything else. The paper says the untrusted proofs are reliable regardless of how reliable the agents are, because “any logical error in a proof is rejected by Lean’s kernel”.

Second, “one percent” understates the human role. The paper says humans also adjudicated amendments that change trusted assumptions, reviewed escalated specification issues and potential bugs, reviewed all amendments at the end of each campaign, designed the structure of the specifications and the overall proof strategy, and designed the agents’ skills. In the paper’s words, “the majority of our effort went not into proofs but into specifications”. The one percent is the reading load for a reviewer who wants to trust the result, not the share of human effort.

How the agents were kept from cheating

A known failure of goal-driven agents is weakening the goal. The paper cites a case in another Lean-proving swarm where an agent redefined a predicate in a conjecture’s hypothesis as False, making the theorem trivially true, and the trick spread through the swarm. AlphaProof Code’s defenses are structural.

At the start of a campaign, a gatekeeper agent copies the approved specification into a held-out directory that no agent can write to. A proof is accepted only if the Lean project’s comparator tool confirms that the theorem and every definition it depends on are identical to that copy, that the proof uses only Lean’s standard axioms, and that Lean’s kernel accepts it. The sorry placeholder and the native_decide tactic are rejected. Proof agents cannot declare a top-level goal finished. The gatekeeper sees only file paths and theorem names, not the provers’ explanations.

Specifications are not frozen, because first drafts are often wrong about real code in harmless ways. Agents can propose amendments to a critic agent that never sees the proof attempts. An amendment must be shown to be necessary, must not weaken security, and must be small. A proposal that would weaken security to match the code “is never accepted as an amendment; it is raised to a human as a potential bug.” One logged example strengthens a library contract to match reality: “memcpy may copy from read-only memory.”

The design moves the integrity question from “did the agents behave?” to “is the held-out statement the one the humans approved, and does comparator work?”. Both are checkable. The repository’s README gives scripts to rebuild the SHA-256-pinned binary, recheck the proofs and rerun comparator. It notes that building and checking all the proofs takes several hours and about 15 to 34 GiB of peak memory, and that the comparator check runs only on Linux, because comparator sandboxes its builds with Linux’s Landlock security module. The repository pins Lean v4.34.0 and the standalone comparator. Comparator’s own README now says the tool has been merged into Lean core as lake comparator as of Lean v4.35.0, so a future recheck may use the built-in version.

The reintroduced bugs

The blog’s evidence that AlphaProof Code “can tell correct code from buggy code” is a test on two bugs found by Cheval, Jacomme and Richards and since fixed. The paper says the authors injected each one by reverse-applying its upstream fix commit to the v0.105.4 source and recompiling.

• Weak state (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, including a copy of the signed prekey secret, is stored anyway.
• Small subgroup (fix 5293caa): the responder does not check that the initiator’s X25519 base key is torsion-free and in range, so a replayed handshake with a modified base key creates a second session with the same shared secret.

For both, the agents produced complete Lean proofs that the symbolic security theorem does not hold for the buggy binary, with concrete witness inputs. The Lean kernel parses the pinned buggy executable and steps its machine code through each attack trace. Those disproofs take 140,000 lines.

The test establishes that the specification is strong enough to reject these two bugs. It does not measure how many unknown bugs the specification would catch: both bugs were chosen after the fact, from a paper whose models the specification was built to replicate. The test also covers only the symbolic theorem. The paper explains that refuting the computational theorem would require exhibiting an attack that defeats every cost-bounded reduction, which amounts to proving the hardness assumptions themselves, an open problem.

What the guarantee does and does not cover

The table below is The Frontier Wire’s consolidation of the paper’s Table 1, its limitations sections (5.1.6 and 5.2.5), the trusted computing base (5.3), the restrictions in Appendices B.7 and C.6 and the future work listed in its discussion (section 9).

Some exclusions are subtle. The symbolic theorems let the attacker choose SPQR’s keys, so they show the Triple Ratchet is no weaker than the classical Double Ratchet, not that SPQR delivers the post-quantum healing it was designed for. Exact replay of a prekey message is not ruled out as a source of forward-secrecy loss. The computational proof covers prekey messages only in canonical protobuf encoding. The binary is built with one codegen unit, panic=abort and a fixed base address, and SPQR is forced onto its software code paths with AES and PMULL support reported as absent.

The paper says that a new build of libsignal-cli “needs a new refinement proof but no new security proof” on the symbolic side, because the binary enters only through the refinement theorem. Between the verified release and the end of November 10, libsignal shipped v0.106.0, v0.106.1, v0.106.2 and v0.107.0. The Frontier Wire has not checked whether those releases changed the one-to-one session code. The proofs do not cover them until someone reruns the refinement.

How it compares with other AI verification work

The paper places itself among several concurrent efforts that use AI to verify compiled machine code, and says those “largely target generic properties, such as crash freedom, or functional correctness”. One of them, the Anthropic and Theorem workflow, is the subject of our earlier walkthrough. The comparison below uses only that article and the DeepMind paper; it compares stated scope, not quality.

The useful contrast is where the difficulty sits. A crash-freedom property is generic and can be stated once for many programs. A security property for a messaging protocol needs an attacker model, a definition of what counts as a trivial win and a mapping from bytes to protocol events. That is why the DeepMind paper argues that “the specification of a nontrivial software artifact is itself a nontrivial software artifact.” The same tension, between a narrow checked statement and a broad reading of it, ran through our analysis of FlashProve’s cryptographic receipts.

The “years of work” comparison

The blog says the verification took “just four weeks” for a task that “historically takes expert teams years”. The paper’s comparison points are seL4, which it says took twenty person-years to verify, and CompCert, which took six. The paper also notes that in both cases the source code was written with verification in mind, while libsignal was not.

By The Frontier Wire’s arithmetic, five people over four weeks is at most about 20 person-weeks of human time, if all five worked on it throughout. That figure excludes the agent compute, which the paper does not report in tokens, machine hours or cost. It is also unclear whether it includes building the program logic, the agent skills and the AArch64 semantics (467 instructions and 31 system calls in 7,532 lines of Lean). The Beneficial AI Foundation says the AArch64 semantics “were created during the project”. The comparison with seL4 is suggestive, not like for like: different systems, properties, tools and accounting.

Two accounts beyond DeepMind’s

Signal’s chief technology officer, Ehren Kret, is quoted in DeepMind’s announcement: “Using AI agents to translate live code into valid Lean theorems is a major breakthrough.” The paper thanks three Signal staff, Rolfe Schmidt, Michael Rosenberg and Kret, for feedback on its specifications; the blog thanks the same three for feedback on the methodology. Neither source describes a formal review of the theorems by Signal beyond that feedback.

The Beneficial AI Foundation, which leads Signal Shot with Signal and the Lean FRO, published its own account on November 10. It calls DeepMind’s work “a huge step” that is “complementary to our work and partly builds on it”, and says DeepMind assumed correct the Dalek elliptic-curve library BAIF has verified and the SPQR library it is still working on. It also warns against “formal-washing”, a term it credits to a joke by Jonathan Protzenko, and describes as over-hyping what has been proven and downplaying assumptions. BAIF wrote that DeepMind “accurately stated that they ‘prove key security properties of libsignal’”, while some coverage had been less precise.

BAIF’s list of remaining work overlaps with the gaps above: completing security proofs for ML-KEM Braid, SPQR and SCKA messaging; Signal’s anonymous credential system, which DeepMind did not formalize; independent validation of the AArch64 semantics; replication on other architectures and compiler settings; and continuous verification so that Signal stays verified across frequent releases.

What remains unknown

Several questions bear directly on how much weight the result can carry.

• Independent rechecking. The proofs are public and the checking scripts are published. As of November 12, The Frontier Wire found no report of an independent party rebuilding the pinned binary and rerunning comparator. The target has also moved once: after the November 11 change, a recheck of the current repository concerns a different pinned binary from the one the paper describes.
• Documentation of the trust boundary. An issue filed on November 10 by an outside user reports that files the code refers readers to, a trusted-base document and the scripts that compute the trusted closure, are missing from the public tree. It was still open when The Frontier Wire checked. Until those are published, the per-theorem list of trusted definitions is harder for an outsider to reproduce.
• Faithfulness of the semantics. The AArch64 model is trusted and cannot be proved correct against hardware. The paper describes lockstep testing against the Unicorn emulator and the Sail model of Armv9.4-A, plus loader tests against qemu-aarch64 on “a large number of binaries”. It does not give test counts or coverage figures for that testing.
• Cost. The paper gives agent counts and campaign durations but no compute, token or dollar figures, so the economics of repeating this for each release are unknown.
• The bridge to the apps. The claim that the theorems carry over to Signal’s Android and iOS builds rests on a trust argument about compiler flags, linking and the operating system interface.
• Specification review by outsiders. The authors say complex specifications “will take many rounds of open review and refinement to settle.” The specifications were published on November 10, so that review is at an early stage.

The proposed tests below would most change the assessment. They are proposals, not work anyone has reported doing.

1. Proposed: an independent group rebuilds the SHA-256-pinned binary and reruns comparator against the published challenge statements on separate hardware.
2. Proposed: a blind mutation study, in which a third party inserts bugs the authors have not seen, to measure how often the specification rejects them.
3. Proposed: a refinement proof for a later release such as v0.107.0, reporting the human time, agent compute and proof repair needed. This would test the paper’s stated goal of verifying new libsignal releases before they ship.
4. Proposed: cryptographers outside the project reviewing the 26,000 trusted lines and the deviation logs, especially the reported errors in the published Double Ratchet analyses.

What the result establishes

The verified claim is specific and checkable: for a specific compiled build of libsignal, under stated assumptions, machine-checked proofs connect protocol-level security definitions from the research literature to the instructions the processor runs, without trusting the Rust compiler. The paper calls these the first such proofs for the unmodified code of a widely deployed cryptographic protocol implementation. Its related-work section explains the distinction: earlier efforts targeted abstract protocol models, reimplementations written for verification, implementations modified to simplify verification, or narrower properties such as crash freedom.

The less visible result may matter more for the field. Once proof writing was delegated to agents and checked by Lean, the remaining hard and human work was deciding what the theorem should say, and the process surfaced errors in published security analyses along the way. As our survey of the AI review bottleneck argued in another setting, faster AI output can transfer work to the people who must judge it rather than remove that work. Here the transferred work is about 26,000 lines that people still have to read.