AlphaProof Code: how AI proved Signal's security properties

On 10 November 2026, Google DeepMind said its AlphaProof Code system had proved key security properties of libsignal, the code behind Signal's end-to-end encryption. The proofs are about machine code compiled from the unmodified source, not a simplified model of it. AI agents wrote about 6.5 million lines of proof in Lean, a language whose checker accepts only correct proofs. A team of five people did the project in four weeks.

For comparison, the verified seL4 operating-system kernel, often called the field's biggest success, took about twenty person-years. The CompCert verified C compiler took six. DeepMind calls its result the first proof of protocol-level security for the unmodified code of a widely deployed cryptographic protocol. This post explains what was proved, how the agents did it, and what the proof does not cover.

What is formal verification?

Formal verification means proving, with mathematics, that a program always meets a written rule. Testing checks the cases you thought of. A proof covers every possible input and every possible attack that would break the rule.

The catch has always been cost. Proofs about real software are long and tedious, so only a few critical systems got them. The proofs here were checked by Lean, a programming language that doubles as a proof checker. Every step must follow from earlier steps, and a small core program called the kernel checks each one. If any step is wrong, the proof is rejected.

What exactly did DeepMind verify?

The target was libsignal version 0.105.4, the reference implementation of the Signal protocol, with its SPQR component. Variants of the protocol also run in WhatsApp, Messenger and Google Messages. The proofs cover one-to-one chats, in two parts:

• PQXDH handshake: how two people agree on a shared secret, including protection against future quantum computers.
• Triple Ratchet: how a fresh key is made for every message. It combines Signal's Double Ratchet with SPQR, a newer post-quantum ratchet.

The proved properties include:

• Forward secrecy: if your phone is hacked today, messages you sent earlier stay safe.
• Post-compromise security: after a temporary hack ends, the conversation heals and later messages become safe again.
• Authentication: you are really talking to the person you think you are.
• Confidentiality: only the two people in the chat can read the messages.

The team compiled the unmodified Rust code with the standard Rust compiler into a program for AArch64, the chip family used by nearly all Android phones and all iPhones. The proofs are about that program's machine code. So nobody has to trust that the Rust compiler is correct. To make this possible, the team wrote a formal model of AArch64 in Lean covering 467 instructions and 31 system calls. They tested it against two independent references: the Unicorn emulator and Arm's official Sail model.

How does AlphaProof Code work?

AlphaProof Code splits the work the way a research team would. Humans decide what to prove. AI agents write the proofs. Lean checks everything. The workflow has four parts:

1. 1Specification: a writer agent and a human turn security models from research papers into Lean statements. Reviewer agents from a different model family critique each draft. The human approves the final version.
2. 2Code: the real Rust code is compiled, and the machine code is loaded into Lean together with the AArch64 model.
3. 3Proof: a team of 40 to 80 agents ran on a single machine for 24 to 72 hours per campaign. An orchestrator splits the work, team leads manage groups of proof workers, and an integrator merges finished proofs.
4. 4Gatekeeping: a gatekeeper agent accepts a proof only if Lean's kernel checks it and a tool called comparator confirms it proves exactly the approved statement.

The specifications were developed with agents powered by Gemini 4 Carbon and Claude Opus 5.5. The proofs were produced entirely by agent teams powered by Gemini 4 Carbon. The paper says none of the authors wrote any proof code.

Why can you trust a proof that an AI wrote?

The design treats the AI as untrusted. A prover agent can make mistakes or even try to cheat. It does not matter, because Lean's kernel rejects any proof with a logical error. Trust moves from the long proof to the short statement being proved.

That statement still needs human care. The paper says the definitions a reader must trust come to about 18,000 lines, plus about 8,000 lines of the AArch64 model. That is large, but far smaller than 6.5 million lines of proof.

The team also had to stop agents from cheating in a quieter way. The paper notes: "Agents under pressure to finish a goal will sometimes weaken it", for example by adding a hypothesis that makes the claim easier. So agents cannot edit the statement. They can only propose an amendment to a separate critic agent that never sees the proof attempts. The critic accepts a change only if it is necessary, small and does not weaken security. Changes to trusted assumptions need human approval.

This is the same problem OpenAI faced when its agents found Linux kernel exploits: a goal like "got root" or "proof done" can be met in ways nobody intended. Both teams fixed it with an independent checker.

Did the proofs catch real bugs?

No new bugs in Signal were reported. To test whether the specifications were strong enough, the team put back two real bugs that earlier researchers (Cheval and colleagues) had found in libsignal and that were already fixed:

• Weak state: a message that failed to decrypt on a new session was tried against older sessions, and the new session's state, holding a copy of a secret key, was stored anyway.
• Small subgroup: the receiver did not check one property of the sender's key, so a replayed, altered handshake could create a second session with the same shared secret.

For both bug-injected programs, Lean proofs showed that the security theorem fails. That is the result you want: a specification that rejects known bad code.

Writing the specifications also found mistakes in published research. The paper lists fifteen gaps or bugs in an earlier mathematical analysis of the Double Ratchet, such as missing assumptions, and errors in printed queries from an earlier automated analysis. The team had to repair them before the proofs could go through.

What does the proof not cover?

The paper is clear about its limits. The main ones:

• Building blocks are assumed: the security of primitives such as X25519, Kyber and HMAC is assumed, not proved. Those are checked by other projects.
• One test program: the theorems are about a small command-line tool the team built around libsignal, not the Signal apps. The same Rust code runs in the Android and iOS apps, but those builds were not verified.
• One-to-one only: group chats, sealed sender and server-side code are future work.
• Partly post-quantum: the main mathematical theorem assumes classical attackers. It does not prove that SPQR heals against a quantum attacker.
• Simplified setting: fixed message lengths, no multiple devices, and a security bound that becomes meaningless for very long sessions, around 25,000 messages if nearly every message starts a new ratchet step.
• Side channels: the machine model describes what the program computes, not how long it takes or how much power it uses. Our reading is that timing and power attacks fall outside the theorems.

Our view: the cost is also missing. DeepMind did not publish what the compute cost. A team of five experts for four weeks is cheap compared with twenty person-years, but that team included specialists in cryptography and Lean. This is not yet a tool any developer can point at their code.

What does this change for software security?

The authors' main lesson is in one line: "once proofs become cheap, the hard question is what to prove." Most of their human effort went into the specifications, not the proofs.

That shifts where skill matters. If agents can write millions of lines of proof, the scarce skill becomes stating security precisely. It means knowing the attacks, the models in the research papers and the real behaviour of the code. The paper suggests a future where programmers write formal security specifications and AI writes and proves the code.

It also matters for defence. AI is now finding exploitable bugs at scale. Proofs offer the opposite guarantee: not "we found no bugs" but "this class of bug cannot exist here, under these assumptions."

Research ideas for students

Formal verification is easier to start than it looks. Some projects:

• Learn Lean: the official site lean-lang.org lists free tutorials. Start with small proofs about lists and numbers.
• Read a real specification: DeepMind released its Lean development. Pick one theorem and write a plain-English explanation of what it promises.
• Mutation testing for specifications: write a small program and a specification, then add bugs on purpose and check whether the specification rejects them. This is how the team tested theirs.
• Specification gaps: compare a protocol's published security analysis with its real code, and list every difference. The team logged more than 200 places where its computational statements departed from the papers or the code.

If you want to turn one of these into a paper, our guide to reading a research paper helps with the dense formal-methods literature. Our course on designing experiments covers how to test a claim like "this specification catches real bugs".