AlphaProof Code: AI agents formally verified Signal's code

On November 10, Google DeepMind introduced AlphaProof Code, a multi-agent system for formal software verification, along with a paper in which AI agents proved security properties of libsignal, the reference implementation of the Signal protocol. The proof is about the compiled machine code, not the protocol design on paper.

What exactly did AlphaProof Code prove?

The team took unmodified Rust code (libsignal v0.105.4 and the spqr library), compiled it with the stock rustc compiler into an AArch64 Linux program, and then proved theorems about that executable. That’s about 560 KB of code, or roughly 140,000 processor instructions.

The theorems cover the PQXDH key agreement (the part of Signal meant to hold up against a future quantum computer too) and the Triple Ratchet. According to the paper, the proofs establish forward secrecy and post-compromise security, among other things, meaning protection for messages sent before and after a device is briefly compromised, as well as authentication of both parties.

The numbers from the paper:

1. About 6.5 million lines of Lean proof, 5.3 million of which concern the binary itself.
2. The work was done by a team of five in four weeks. For comparison, the authors point out that verifying the seL4 microkernel took twenty person-years.
3. A single proof campaign typically means 40 to 80 agents on one machine for 24 to 72 hours.
4. To trust the result, you need to read about 18,000 lines of definitions and theorems plus about 8,000 lines of AArch64 semantics. Lean checks the rest.

Interestingly, the Rust compiler isn’t on the list of things you have to trust. Since the proof is about machine code, a compiler bug that broke the properties being proved would have made the proof fail.

Who wrote the proofs, and who wrote the specifications?

The proofs were written entirely by agents built on Gemini 4 Carbon, and the paper says none of the authors wrote a single line of proof code. The humans had a different job: deciding what should be proved.

The specifications came out of conversations between people and agents built on Gemini 4 Carbon and Claude Opus 5.5. One agent wrote a draft, an agent from the other model family reviewed it, and then a human signed off on the result. The authors say outright that most of their effort went into the specifications, not the proofs.

A separate agent, the “gatekeeper”, accepts a proof only when the Lean kernel accepts it and the comparator tool confirms that it proves exactly the approved specification, a copy of which was kept out of the agents’ reach. The reason is mundane: agents under pressure will weaken the goal to finish sooner (the authors cite a case from another experiment in which an agent defined a condition from the hypothesis as false, and the rest of the swarm ran with it).

The team also checked whether the specifications catch real bugs. They reintroduced two previously fixed libsignal bugs into a copy of the code, and in both cases got a Lean proof that the resulting program does not satisfy the security theorems.

There’s a side effect, too. While porting security models from the literature into Lean, the team found fifteen gaps and errors in the published analysis of the Double Ratchet, plus mistakes in the ProVerif queries from another paper on Signal. The formalization ended up testing the academic papers themselves.

Is this new for AI?

In October, Anthropic and Theorem showed formal verification of 123 open source libraries with Claude, also at the machine code level. There, the specification was generated automatically and said that the program won’t crash or violate memory safety. DeepMind cites that work and sets its own apart: here the properties being proved belong to a whole protocol facing an active attacker, and the specification had to be written by hand from the cryptographic literature.

So there are two approaches. One is broad and shallower (many libraries, one simple property), the other narrow and deep (one library, rich theorems). They appeared less than three weeks apart.

Ehren Kret, Signal’s CTO, called AI agents translating working code into correct Lean theorems “a major breakthrough”.

What should you watch out for?

First, the scope. The proof covers one-on-one conversations between two honest parties. Group messaging, multi-device state and side-channel attacks are outside it, and the Signal app itself is much more than libsignal.

Second, the assumptions. The low-level cryptographic routines are not verified, only described by contracts you have to trust, just like the AArch64 semantics and the specifications themselves.

Third, quantum computers. The computational part of the proof gives no guarantees against a quantum attacker. Secrecy of the key agreement against a future quantum computer was shown only in the symbolic model, which assumes perfect cryptography.

The authors list all of these limitations in the paper themselves.

FAQ

Can you try AlphaProof Code?

Not as a product. DeepMind hasn’t given a price or a release date. The specifications and Lean proofs are published, and anyone can check them independently.

Does the proof also apply to WhatsApp and Messenger?

Not directly. The paper says that variants of the Signal protocol run in WhatsApp, Messenger and Google Messages, but the theorems are about a specific binary built from libsignal v0.105.4.