AlphaProof Code Verifies Signal’s libsignal in Lean

Google DeepMind has introduced AlphaProof Code, which it describes as a multi-LLM agentic framework, and says agents powered by Gemini Carbon formally verified compiled AArch64 machine code of Signal’s libsignal library. According to DeepMind’s 10 November 2026 blog post by Pushmeet Kohli and Swarat Chaudhuri, those agents generated over six million lines of Lean and flagged 1% of the codebase for human review.

The scope of the claim needs to be stated before the first-time language that follows it. The accompanying Apache 2.0 repository presents two AI-generated proofs of security for compiled AArch64 machine code of libsignal, in a command-line harness with hooked cryptographic primitives. The proofs cover libsignal v0.105.4 and spqr v1.6.0, and come in two flavours, one symbolic and one computational. The cryptographic primitives were hooked and idealised; they were not themselves proven. This is not a formal proof of the whole Signal application, and it is not a demonstration that Signal is universally secure.

What DeepMind says the agents did

DeepMind’s blog is the source for the headline production figures. It says the Gemini Carbon agents “did the proofs, generating over six million lines of Lean,” and that the agents flagged “just one percent of the codebase” for human review. It also says “our verification process took just four weeks – a task that historically takes expert teams years.” That comparison is DeepMind’s claim about the effort involved, not an independently audited stopwatch result.

The same post makes two first-time claims, which should be attributed to DeepMind rather than restated as settled fact. DeepMind says this is “the first time AI has been used to formally verify a widely deployed cryptographic protocol at this depth,” and “the first time the implementation of a widely deployed protocol like this has been formally verified by any method.” Those are the laboratory’s own characterisations of the work.

As a test of the pipeline, DeepMind says it “reintroduced two real, previously fixed bugs into an isolated version of Signal’s code.” In both cases, it says, the system “produced a machine-checked proof that the buggy version was insecure.” The bugs had already been fixed in the real codebase; they were put back into an isolated copy so the tools could be asked whether the broken versions could be shown to be unsafe. That is a useful check on the method. It is not the same thing as a hunt for new, live vulnerabilities in Signal as users run it.

The blog also quotes Ehren Kret, Signal’s chief technology officer, as saying: “Using AI agents to translate live code into valid Lean theorems is a major breakthrough.” That sentence appears in DeepMind’s post. TSN has not seen an independent Signal blog or press note confirming or expanding on it, so the quote should be read as DeepMind’s attribution of Kret’s remarks, not as a separate Signal publication.

The paper associated with the release is titled “AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level.” The Lean developments and review materials are published in the GitHub repository and on DeepMind’s reviewers’ site. The work is being released under an Apache 2.0 licence, which means other researchers can inspect, run and criticise the artefacts rather than having to take the blog’s summary on trust.

What the proofs cover, and what they do not

The narrowness of the artefact is the story’s main caveat, and it is not a quibble. Formal verification is only as wide as the thing that was formalised. Here, that thing is compiled AArch64 machine code of specific versions of libsignal and spqr, built for a command-line harness, with the cryptographic primitives hooked out and treated as ideal. A proof in that setting can be real, machine-checked, and still silent about the rest of the Signal application: the mobile clients, other architectures, the user interface, the build and distribution chain, and the actual cryptographic implementations that were replaced by hooks for the proof. Idealised primitives are a standard technique in protocol proofs, but they mean the mathematics assumes those components behave as specified. It does not prove that they do.

That is why DeepMind’s first-time claims should stay inside quotation marks of attribution. If the laboratory is right, this would be an unusually deep, automated formal pass at a widely deployed messaging protocol’s implementation. If the scope is forgotten, the same sentences can be misread as a clean bill of health for Signal as a product. They are not. The pinned versions matter as well: a proof about libsignal v0.105.4 and spqr v1.6.0 does not automatically extend to later or earlier releases, or to every way those libraries are compiled and shipped.

The historical-bug test should be read in the same spirit. DeepMind says the system produced machine-checked proofs that two previously fixed bugs, once reintroduced in isolation, made the code insecure. That is evidence that the pipeline can notice known, broken variants, which is a stronger demonstration than a blog post that only describes a successful proof of the good code. It still depends on those bugs having been selected, reinserted and tested in an isolated copy. It is not, by itself, a claim that every possible flaw in libsignal would have been found, or that the live application is free of others.

The work also sits in a wider, uneven shift toward machine-checked reasoning. TSN has already covered AlphaProof Nexus, DeepMind’s earlier Lean-based system for mathematical problems, and Axiom’s formalisation of the classification of finite simple groups in Lean. Those efforts were about mathematics. AlphaProof Code is an attempt to point similar agentic tools at production cryptographic code. That is a different, and in some ways harder, target, because the artefact is a compiled implementation rather than a textbook theorem. It is also a different kind of AI-agent story from Anthropic’s Claude Fable 5.2 and Mythos 5.2 models, which are general-purpose systems rather than a Lean verification pipeline.

The next evidence that would change the reading is not another laboratory summary of the six-million-line figure. It is independent checking of the published Lean, a clear account of what the hooked primitives assume, and, in time, whether the same method can be applied to other architectures, later library versions, or a build that does not replace the cryptography with an idealised stand-in. Until then, AlphaProof Code is best described as DeepMind presents the artefact: a pair of machine-checked proofs about compiled libsignal in a restricted harness, produced unusually quickly by the laboratory’s own account, with a narrow and publicly inspectable scope.