Watch the video, transcript and sources
https://www.youtube.com/watch?v=-v4XdcxtfyU
+ AI writes machine-checked security proofs
+ Humans approve the claim and assumptions
- Whole-app security guarantees remain outside this resultAn AI security audit can leave you reading a confident explanation and wondering who checked it. Google DeepMind's AlphaProof Code announcement comes with formal proofs that Lean can check against an approved specification. The useful separation is clear: models write candidate proofs, humans decide the claim, and a theorem prover checks whether the proof establishes it.
The study targets selected security properties of a particular compiled libsignal command-line harness. That scope matters every time someone shares the headline. A reader still has to inspect the specification, its cryptographic assumptions and the model of how the machine runs.
Humans write the assignment
Google's technical paper says five researchers worked over four weeks. Agents produced the proof code, while the researchers concentrated most of their effort on specifications. A specification states the desired behavior, the attacker's capabilities and the assumptions the argument needs.
Reviewers have to decide whether that mathematical statement captures the security people actually want. Lean can reject a logical mistake in a proof. Human judgment still has to catch a weak question that leaves an important attack outside the claim.
For this work, the team builds on earlier analyses of Signal's handshake and message-key ratchet. Existing research already studied the protocol designs. Google's reported contribution connects security arguments to the unmodified production library's compiled implementation. Signal CTO Ehren Kret describes the approach as an expansion beyond earlier verification's smaller scopes.
The compiled artifact has a name
The researchers compile the Rust library using the standard compiler into an AArch64 Linux executable, wrapped in their small CLI harness. They then state theorems about the binary using a formal instruction model.
A compiler error that breaks a stated property would make the theorem false. For this claim about this binary, the compiler leaves the trusted base. The instruction semantics, Lean's kernel and specified contracts remain trusted.
The paper reports about six and a half million lines of checked proof, resting on roughly twenty-six thousand lines of trusted specification definitions and instruction semantics. Those numbers describe the artifact. They establish no intelligence score or independently measured productivity multiplier. Please resist ranking developers by their node_modules folder while the formal-methods people are trying to work.
Useful guarantees have conditions
The checked arguments cover message confidentiality and authentication, with forward secrecy and post-compromise security under the stated models. Those latter properties describe limits on stolen-key damage and recovery after fresh exchanges. The guarantees retain conditions on sessions, inputs and attacker behavior.
Low-level cryptographic routines sit behind trusted contracts. The arguments assume those routines behave as specified and rely on cryptographic security assumptions. The symbolic proof idealizes cryptography; the computational proof reasons about attacker success probabilities.
The result concerns the researchers' command-line harness. Group messaging is future work, and the computational model excludes multi-device state. This does not establish bug-freedom for every Signal installation.
The researchers also reintroduced two previously fixed bugs into isolated copies and compiled them. Checked proofs showed those binaries violated the symbolic security theorem. That gives useful evidence that the specification rejects those broken implementations. It supplies no new live vulnerability or emergency update.
Google publishes the specifications, proofs and checking instructions. A full clean build takes hours and substantial memory. I haven't rebuilt that artifact for this episode; we're reporting the published work and reading its boundaries.
The goalpost check reaches underneath the headline
The paper spells out a trap: a logically correct proof can establish a very weak claim. An impossible assumption can make a theorem vacuous. A changed definition buried beneath the visible theorem can weaken the target too.
Human reviewers approve the specification, and the gatekeeper keeps a held-out copy that proof agents cannot edit. Agents may propose corrections through a separate amendment process. Changes to trusted assumptions are adjudicated by humans directly or under a policy they set, and amendments are reviewed after each campaign. A proposed security weakening is escalated as a potential bug.
The specific payoff is Lean's comparator. It compares the theorem and every definition it depends on with the protected approved copy. It checks allowed axioms and replays the proof in a fresh kernel. Quietly weakening a helper definition therefore changes the material being compared.
That still leaves humans responsible for the target's strength. For an ordinary AI workflow, the practical lesson is to keep acceptance criteria outside the worker's edit permissions and review proposed changes separately. The worker can ask to change its assignment. It cannot award its own passing grade.
Verdict: SHIP IT
I'd ship this 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. This is a verdict on the workflow, within the published evidence boundaries.
Which would you review first: the specification or the proof?
Sources
Portrait credit: Christopher P. Michel / Cmichel67, Demis Hassabis in 2025, CC BY-SA 4.0. Portrait adaptations and portrait-based artwork are shared under that licence; Cropped, resized and compressed; unflipped, with no background removal, expression change or generated detail. Lab identity only; no authorship, proof writing, current reaction or endorsement is implied. Cartoon commentary: Expanding Brain / Imgflip, cropped and captioned artifact-count satire, at most two seconds; Tom and Jerry / Boomerang Official GIF, silent resized/captioned excerpt of about two seconds, with uploader source. Brief transformed process commentary; no actual researcher or executive reaction. Hosting is not a licence or legal clearance; no blanket reuse.
Source-footage disclosure: the public technical paper's prose is unchanged. Local Inter/reflow, a cursor, finite zoom and markers make the selected passages visible. No proof rebuild or private Signal UI is shown.
And that's the diff for today. I'm Niko from Axrisi. Merge responsibly.