Google DeepMind reports machine-checked security proofs for a compiled implementation of selected Signal protocol operations. Its new AlphaProof Code work gives developers a concrete example of AI doing difficult proof construction while a separate checker enforces a human-approved target. The specification, the compiled artifact and the trusted assumptions all matter to understanding the result.
TL;DR
- AlphaProof Code combines human-guided specification development with AI-generated Lean proofs.
- The researchers verify a particular compiled
libsignalcommand-line harness under stated models and cryptographic assumptions. - Lean checks the proof's logic. A comparator checks the approved theorem and every definition it depends on.
- The humans still decide whether the specification captures a meaningful security claim and review changes to trusted assumptions.
- I stamped the checked-proof workflow SHIP IT, with the scope and assumptions attached to every result.
What Google DeepMind actually released
The November 10 announcement describes AlphaProof Code as a framework for formal software specification and verification. The accompanying technical paper provides the details that a short announcement necessarily compresses: the target binary, the models of attackers, the cryptographic contracts and the restrictions on the guarantees.
The team reports roughly six and a half million lines of checked Lean proof. The trusted specification definitions and instruction semantics amount to about twenty-six thousand lines. Those are artifact counts, with additional tooling and symbol-name trust described in the paper. They establish no intelligence score or universal productivity ratio.
The proof campaign involved five researchers over four weeks. According to the paper, the agents generated the proof code; human effort concentrated on specifications, review and directing the work. That is a reported research campaign. Comparing it directly with the person-years of a different verification project would require matching the tasks and measuring the resources. We have no such comparison here.
The public repository contains the specifications, proofs, formal instruction semantics and checking instructions. I haven't rebuilt this enormous development for the episode. This article reports the published result and explains what its checks are designed to establish.
Formal verification starts with the question
A security specification is a mathematical statement of what a system must guarantee. It also describes the attacker and the assumptions under which the guarantee applies. Each choice changes the question the proof answers.
Suppose a claim only concerns inputs from a very restricted set. Proving it may tell you little about other inputs your application accepts. A specification that leaves an important attacker action outside its model can also miss a security concern. These are questions about the statement's meaning and strength, even when the proof of that statement is logically correct.
Section 2.1 of Google's paper makes this division explicit. A specification consists of theorem statements and the definitions they depend on, including models of the environment. Human reviewers have to trust that those definitions capture the intended claim. The proof supplied by an agent can remain untrusted because Lean's kernel checks whether it follows from the formal statement and permitted assumptions.
The researchers describe several ways to scrutinize specifications. Review agents examine their faithfulness to the source literature and implementation. The development includes checks for vacuous statements, including witnesses that relevant hypotheses can hold. The team also tests whether specifications reject deliberately broken code. These checks support review; selecting the target remains a human responsibility.
For developers using AI, that split is immediately recognizable. A worker that changes the acceptance criteria can make an impressive amount of progress on a different task. More output will not fix a question that drifted halfway through the assignment.
Why Signal's compiled implementation matters
Signal's protocol has a substantial history of formal analysis. Its official PQXDH specification discusses prior symbolic and computational work. The ratchet specification explains how message-key derivation evolves, including the Triple Ratchet's combination of classical and post-quantum components.
Protocol models can capture a design's intended security while omitting some of the complexity that implementation introduces. The technical paper points to concrete machinery inside libsignal: archived sessions, out-of-order messages, serialization and mutable session state. These are ordinary requirements of a useful messaging library. They make the connection between the design argument and the implementation harder to establish.
For this study, the researchers use unmodified libsignal crates inside a small command-line harness. They compile the code into an AArch64 Linux executable with the standard Rust compiler. The formal claims concern runs of that compiled artifact using a model of instructions and the process environment.
This is why the paper excludes the Rust compiler from the trusted base for the stated properties of that binary. A compiler error that violates a property would make the theorem false. The argument has to succeed for the compiler's output.
The remaining trust has a different shape. Readers still trust the formal instruction semantics, Lean's kernel and the contracts applied at specified boundaries. The paper also identifies extraction and reproducible-build tooling in its trusted base. A binary-level proof changes the trust boundary; it does not erase it.
Which security guarantees have conditions?
The reported results cover message confidentiality and authentication, with forward secrecy and post-compromise security under the stated models. Forward secrecy limits damage to earlier messages when current keys are compromised. Post-compromise security concerns recovery through fresh exchanges under the model's conditions. An attacker that remains active, a different session scenario or an omitted implementation feature can change which claim applies.
The paper presents both a symbolic and a computational argument. The symbolic model treats cryptographic primitives as ideal operations and proves properties within that abstraction. The computational model reasons about an efficient attacker's success probability and assumptions about the underlying primitives. These are complementary forms of assurance with different restrictions.
Low-level cryptographic routines are specified through trusted contracts. The result assumes those routines behave as specified and relies on cryptographic security assumptions. The proof therefore should not be described as an independent implementation proof for every primitive it calls.
The setting is also bounded. The paper describes the particular CLI build, group messaging as future work and an absence of multi-device state in the computational model. It lists additional session and input restrictions, and gives limits on what the quantitative bound establishes at large scale. Its computational bound gives no guarantee against quantum adversaries; the symbolic analysis covers a specified portion of that question.
Those details are useful when assessing a claim, rather than grounds for throwing the result away. Ask which guarantee you need, which artifact the theorem concerns and whether your environment satisfies the premises. A security proof becomes easier to use when those boundaries travel with the headline.
A green result needs a broken case
The researchers reintroduced two previously fixed bugs that earlier work had found in libsignal. They injected each into an isolated version and recompiled it. The resulting Lean proofs establish that those binaries violate the symbolic security theorem.
That exercise checks something important about the specification: it can reject those real broken implementations. The bugs had already been fixed. This supplies no new live Signal vulnerability, emergency update or demonstration against a user's account.
It also illustrates why specification evaluation deserves its own effort. If a proof system accepts the good version and the specification says nothing about the relevant mistake, the result can look reassuring while answering a weaker question than readers assume. A broken-case check helps expose that weakness for the cases tested.
The public artifact makes further inspection possible. Its README explains the pinned toolchains and comparator procedure. It also warns that a clean build takes several hours and substantial memory. Outsiders have a path to check the development, and independently completing that path is a separate claim from reading the paper.
The comparator checks beneath the visible theorem
Here is the detail I wanted the episode to reach. Checking the visible theorem statement alone leaves a route for weakening the task through definitions that statement uses. A predicate can change underneath an unchanged theorem name.
The gatekeeping section describes a protected approved specification copied from a baseline commit. Proof agents cannot write to its held-out directory. The gatekeeper calls a deterministic checking script, and the development retains a distinction between trusted specification files and untrusted proof files.
The comparator then checks the statement and every definition it depends on against that approved copy. It also checks that the proof uses permitted standard Lean axioms and replays the proof in a fresh kernel. A weakened helper definition changes the material being compared, even if the visible theorem text still looks familiar.
Specifications can need genuine corrections. The researchers therefore provide a separate amendment process with a critic and human-approved policy or judgment. Changes are logged and reviewed. A proposed security weakening is raised as a potential bug. The protected target changes through that process, rather than through the prover quietly editing its own assignment.
For an ordinary agent workflow, I would keep acceptance criteria outside the worker's edit permissions and review proposed changes separately. That is a practical lesson from this design. Its usefulness in another agent task needs its own evaluation. The formal result depends on much more precise machinery than a prompt saying “please check yourself.”
Verdict: SHIP IT
I'd ship the checked-proof workflow because the approved claim stays separate from the agent producing the answer. I'd keep the scope and assumptions attached to every result. The human role becomes especially important where the system decides what security means and whether the assumptions match the intended environment.
The published artifact gives that discussion something concrete to inspect. I would start with the target and the trusted base, then ask how the implementation proof connects to them. Your requirements document has finally found a way to demand more attention than the generated code.
FAQ
Does this prove every Signal application is bug-free? The result concerns selected properties of the researchers' compiled CLI harness under stated models and assumptions. It establishes no blanket whole-application guarantee.
Can the AI change the specification? Agents can propose amendments through a separate reviewed process. They cannot write to the protected approved copy themselves.
Why is Lean's kernel important? It checks the logical proof, so proof acceptance does not rely on believing the model's explanation. The kernel remains part of the trusted base.
Did we independently rebuild the proofs? No. The episode and article report the published work and its boundaries. The repository provides instructions for an independent check.
Sources
- Technical paper, including scope, assumptions and gatekeeping
- Google DeepMind announcement
- Public artifact repository and checking instructions
- Signal PQXDH specification
- Signal ratchet specification
- Demis Hassabis portrait by Christopher P. Michel / Cmichel67, CC BY-SA 4.0. Portrait-based artwork identifies lab leadership only; no authorship, proof writing, current reaction or endorsement is implied. Portrait and complete artwork adaptations use the same licence. Changes are cropping, normal resizing and compression, unflipped; no background removal, expression change or generated detail.
This article expands on an episode of **The Daily Diff, a five-minute daily video on what shipped and what broke in tech.
Watch the episode · Subscribe on YouTube · the written diff lands in your inbox every morning at thedailydiff.dev.
Top comments (0)