AlphaProof Code and Signal: checked machine-code security proofs and trusted assumptions

What this video covers

• AI agents produce candidate proofs; Lean's kernel checks whether they establish the human-approved formal claim.
• The verified target is a particular compiled libsignal CLI harness, with trusted semantics and cryptographic contracts.
• Proving the compiled binary removes the Rust compiler from the trusted base for that binary's stated properties.
• The researchers report two isolated reintroductions of previously fixed bugs that violate their symbolic security theorem.
• The comparator checks the theorem and every dependent definition against a protected approved specification; amendments pass through a separate reviewed process.

Transcript

Who checks an AI security proof?

0:00 An AI security audit still sounds like trusting a chatbot. Google's new Signal result comes with mathematical proofs a separate kernel checks. In this video, what did Google prove? And how do they stop an agent moving the goalposts? Here's the useful answer. Models write candidate proofs, and Lean checks the proofs against a human-approved claim about selected compiled code. Humans still own the claim and assumptions.

0:21 You can check the result without believing the model's victory speech. A separate check catches quietly changing the question. We'll follow it down to the definitions. It's Tuesday, November tenth, and this is The Daily Diff. AlphaProof Code is Google's framework for writing software specifications with human guidance and generating checked proofs with AI agents. This study targets libsignal, the Rust library implementing Signal's messaging protocol, inside a particular command-line program.

0:45 Google announced the work today. Its paper says five researchers worked over four weeks. Agents wrote the proofs, while humans spent most of their effort on the specifications. Requirements have found a way to become even more expensive meetings. The specification says what the program must do,

How does a claim become a proof target?

0:59 what an attacker controls, and which assumptions the argument needs. Reviewers ask whether it captures the security people care about. A beautifully checked answer to a weak question leaves that question intact. The team builds on earlier research into Signal's handshake and its message-key ratchet. Formal analyses already studied those designs. Google's claim connects their security arguments to an unmodified production library's compiled implementation, where the design has to survive contact with actual code. Signal's chief technology officer, Ehren Kret,

1:27 describes an expansion beyond earlier verification's smaller scopes. Implementation details include out-of-order messages and archived sessions for delayed messages. Real software keeps the receipts your elegant diagram threw away. The researchers compile the unmodified Rust library with the standard

Why prove the compiled binary?

1:41 compiler into an Arm sixty-four Linux executable. Their theorems describe that binary using a formal instruction model, reaching across the gap between source and optimized machine code. A compiler error that breaks a stated property would make its theorem false. The compiler therefore leaves the trusted base for this binary. You still trust the instruction model and Lean's checker. The trust boundary moved, and it has an address. About six and a half million lines of checked proof rest on roughly twenty-six

2:06 thousand trusted specification and instruction-semantics lines. These are artifact counts. Treating them as intelligence scores is like ranking developers by the size of their node modules folder.

Which security properties survived the implementation gap?

2:16 The arguments cover message confidentiality and authentication, with forward secrecy and post-compromise security under stated models. Those last two describe limits on stolen-key damage and recovery after fresh exchanges. Each guarantee has conditions on the attacker and session. Cryptographic primitives sit behind trusted contracts. The proof assumes those routines behave as specified and relies on cryptographic security assumptions. One proof idealizes cryptography; the other reasons about attacker success probabilities.

2:42 Both have restrictions on the scenarios they cover. Ask which build, which property, and which assumptions. This result concerns the researchers' command-line harness. Group messaging is future work, and the computational model excludes multi-device state. Calling every Signal installation bug-free wanders outside the theorem. The researchers reintroduced two previously fixed Signal bugs into

Can the specification reject broken code?

3:02 isolated copies and compiled them. Checked proofs showed those binaries violated the symbolic security theorem. That tested whether the specification could reject real broken implementations. Your green checkmark needs a red test. Google publishes the specifications and proofs with checking instructions. The repository says a clean build takes hours and substantial memory. Reading the announcement is considerably easier on the laptop. The hardware model and trusted contracts still need review.

3:26 I haven't rebuilt the enormous artifact for this episode. We're reporting the published result and its boundaries. Outsiders have a path to inspect it, which matters more to me than another AI victory lap. Now the trap.

Can a correct proof answer the wrong question?

3:36 Lean can accept a correct proof of a statement that asks for almost nothing. Impossible assumptions can make a theorem vacuous. Changing a definition buried underneath the headline theorem can weaken the goal. The paper designs checks against this. The gatekeeper keeps a held-out approved specification that proof agents cannot write to. They can propose corrections through a separate amendment process. Security weakening gets escalated as a potential bug. The prover's declaration of success has no authority here.

4:00 Humans adjudicate changes to trusted assumptions, directly or through their policy, and review amendments after each campaign. Expert judgment stays on the hook. The agent can request a different assignment. It cannot give itself a passing grade.

What catches the moving goalposts?

4:13 Here's the promised check. Lean's comparator compares the theorem and every definition it depends on with that protected approved copy. It also checks allowed axioms and replays the proof in a fresh kernel. Quietly weakening a helper definition therefore changes the thing being compared. An accepted proof has to establish the approved target. That still leaves humans responsible for choosing a strong target and honest assumptions. For your own AI workflow, keep the acceptance criteria outside the

4:37 worker's edit permissions and review proposed changes separately. Google's result makes that separation concrete. The proof writer does the work; the checking boundary decides whether it counts. If you'd rather read this than hear me say it, the diff lands in your inbox every morning, free at the daily diff dot dev, link below. So today's verdict is SHIP IT.

Would I ship this proof workflow?

4:54 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. Subscribe, hit the bell, and tell me in the comments if you'd have stamped it differently. And that's the diff for today. I'm Niko from Axrisi. Merge responsibly.

Sources

1. AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — technical scope, trusted base and gatekeepingSwarat Chaudhuri and colleagues / Google DeepMind and Google
2. Introducing AlphaProof Code — November 10 announcement and attributed Signal CTO responsePushmeet Kohli and Swarat Chaudhuri / Google DeepMind
3. Code-verification repository — initial commit, public artifacts and checking instructionsGoogle DeepMind / GitHub
4. The PQXDH Key Agreement Protocol — older official specification and prior-analysis contextEhren Kret and Rolfe Schmidt / Signal
5. The Double Ratchet Algorithm — Triple Ratchet sectionTrevor Perrin, Moxie Marlinspike and Rolfe Schmidt / Signal
6. Google DeepMind leadership — Demis Hassabis's relevant lab identityGoogle DeepMind
7. Demis Hassabis in 2025 — authentic portrait, cropped/resized/compressed and unflipped; no background removal or generated expression/detail; lab identity only, no authorship, proof writing, current reaction or endorsementChristopher P. Michel / Cmichel67 / Wikimedia Commons
8. Portrait licence — CC BY-SA 4.0; attribution, adaptation disclosure and ShareAlikeCreative Commons
9. Expanding Brain template — cropped/captioned artifact-count satire, brief transformed <=2s commentary; no benchmark, hosting licence, legal-clearance or blanket reuse claimImgflip / user-uploaded meme template
10. Tom and Jerry — Boomerang Official actual animated reaction, silent resized/captioned 1.875s excerpt; brief transformed process commentary, no actual researcher or executive reaction, hosting licence, legal-clearance or blanket reuse claimBoomerang Official / GIPHY / Tom and Jerry
11. Boomerang GIF source link — uploader-provided provenanceBoomerang
12. AlphaProof Code discussion — attention context, anonymous opinions excluded from factual proof claimsHacker News
13. Code-verification licence — Apache 2.0 for Google code, third-party licences retainedGoogle / GitHub