What DeepMind Proved About Signal’s Code, and What to Ask of Yours

Google DeepMind announced AlphaProof Code today. In it, AI agents help people write a formal specification for a piece of software, then prove on their own that the code meets it. The team applied it to libsignal, the Signal protocol’s reference implementation. Their technical paper reports proofs of forward secrecy, authentication, post-compromise security and handshake secrecy at the machine-code level. It says a team of five did the proof work in four weeks.

That matters. As the announcement puts it, most protocol verification stops at the design level, and real vulnerabilities often hide between the design and the running code.

What caught my attention is the scope. The announcement says the proofs go “down to the exact code running on devices.” The paper is narrower. The team verified the one-to-one session code of libsignal-protocol v0.105.4, with spqr v1.6.0. They wrapped the unmodified code in a small command-line harness and compiled it with the stock Rust compiler to AArch64 Linux machine code. The results concern that build, “not Signal’s own applications.” Key generation isn’t verified, and group messaging is left for future work.

That precision is the useful part.

TL;DR

• DeepMind proved key security properties of one compiled build of libsignal’s one-to-one session code, under stated assumptions. That isn’t a proof of the Signal app.
• The explicit scope is what makes the result usable: you know exactly what it covers. Any security claim can be that precise, with or without a proof.
• Before you accept a security claim, ask what it protects, what it covers, what evidence backs it, what it assumes, and which changes would require another review.

Formal verification means proving mathematically that a program does what a precise description says, for every possible input, not just the ones someone tested.

That description is the specification. Here, it states properties such as forward secrecy in exact terms. Roughly: if an attacker steals a device’s session state today, messages from before that point stay secret.

Lean is a proof assistant: a language and tool for writing proofs. Its small core, the kernel, checks every step, and a proof with a wrong step is rejected.

“Checked by Lean” changes what you have to trust. The agents wrote about 6.5 million lines of Lean proof. You don’t need to trust the agents, because Lean’s kernel checked their proofs. You do have to trust the kernel itself, the paper’s model of AArch64 machine code, contracts that stand in for some routines the program calls (mostly low-level cryptography), assumptions about the underlying cryptography, and the specification. The paper puts the trusted part at about 26,000 lines of specifications and machine semantics. The Rust compiler isn’t on that list. The theorems are about the compiled code, so a compiler bug that broke a property would make the proof fail.

The paper is blunt about this: “The specification must be trusted,” and it “cannot be automatically checked.” DeepMind says human experts reviewed every specification before the agents started on proofs.

Here’s a hypothetical, unrelated to Signal. A business application has a rule: an authenticated employee may export customer records. A multi-tenant system could follow that rule exactly and still let an employee at one customer export another customer’s records. The business almost certainly meant something stronger. The employee must belong to that customer’s organization and hold export permission there.

Proving the first rule, however rigorously, won’t add the missing condition. Someone has to recognize what the business is protecting and write it down. Product owners know what was promised to customers. Engineers know how the system behaves. Security people know how that behavior gets abused. A requirement that matters needs all three to agree before anyone treats its verification as acceptance.

“Security reviewed” can mean a scanner run, a penetration test or a specialist reading one component. Each can be useful, but the label alone tells a buyer little about what’s still exposed.

The Signal paper is the opposite. Here’s how it answers the five questions I’d put to any security claim:

Question	How the paper answers it
What protection is claimed?	Forward secrecy, authentication, post-compromise security and handshake secrecy, each stated as Lean theorems.
Which implementation and conditions are covered?	The one-to-one session code of those library versions, in that harness, built for AArch64 Linux. Not key generation, group messaging or Signal’s apps.
What evidence supports it?	About 6.5 million lines of proof checked by Lean’s kernel. DeepMind is open-sourcing the verification artifacts.
Which assumptions remain?	Lean’s kernel, the machine model, the routine contracts, the cryptographic assumptions and the specification. The paper lists further limits, such as no multi-device state.
What changes require another review?	A new build needs a new proof that its machine code matches the model, though not a new security proof. A change to the specification goes back to human review.

Most suppliers won’t arrive with a mathematical proof, and they don’t need to. What I want is a claim exactly as strong as the evidence behind it.

Tests, reviews and proofs answer different questions. Passing tests show how the system behaved in the cases you ran. A review can catch a wrong requirement or a risk the tests never touched. A proof establishes the specified properties within its assumptions. They support each other. None replaces the others.

The heaviest scrutiny belongs where a failure does outsized harm. In most business software, that means tenant separation, authorization decisions and the integrity of financial records. For each one, pick evidence that’s strong enough and still practical: a clearer requirement, a targeted test, an independent review, or a small study of whether formal verification is feasible. Demanding the same method everywhere makes the standard impossible to keep.

Evidence is only worth something if you can connect it to the running system: the component, version and configuration the claim was accepted for.

The paper’s split between the security proof and the build-specific proof is a good model. Decide in advance which changes reopen which evidence. A new authorization model, a different cryptographic dependency or a changed deployment assumption needs fresh evidence. A wording fix in the interface doesn’t reopen the whole assessment.

Next time a supplier or your own team calls a system secure, ask:

• What exactly is protected? Get it in one sentence.
• Which component, version and configuration does that cover, and what’s left out?
• What evidence supports it, and can someone else inspect or rerun it?
• What does the conclusion assume?
• Which changes would require another review, and who decides?

If nobody can answer, you have a label, not assurance. A machine-checked proof of compiled code is still rare. A clear answer to these five questions shouldn’t be.