Table of Contents
Google DeepMind has used AI agents to mathematically prove key security properties of Signal’s cryptographic protocol at the compiled machine-code level. Its new AlphaProof Code framework connects guarantees about private messaging to the behavior of libsignal, the protocol’s reference implementation, rather than stopping at an abstract description of how the protocol should work.
The work covers Signal’s PQXDH handshake and Triple Ratchet messaging system. Researchers used human-reviewed specifications and autonomous proof-writing agents to establish confidentiality, authentication, forward secrecy, and post-compromise security under defined cryptographic and operating assumptions.
DeepMind announced the result after a four-week verification effort. The agents generated about 6.5 million lines of Lean proof code, checked by the theorem prover’s kernel. DeepMind calls it the first verification connecting protocol-level security guarantees to an unmodified, widely deployed cryptographic implementation at this depth.
From Encryption Design to Executable Code
Formal verification starts by stating precisely what software must do and then proving that it satisfies those requirements. Testing checks selected inputs and scenarios; a formal proof establishes a specified property across the behaviors allowed by its mathematical model.
Encrypted messaging requires more than showing that an encryption algorithm works. A messaging protocol must manage identities, establish shared secrets, update keys, and respond correctly when an attacker compromises parts of a conversation’s state.
PQXDH establishes the initial shared secret using a combination of conventional and post-quantum cryptography. The Triple Ratchet updates cryptographic state as messages are exchanged. Forward secrecy protects earlier messages when keys are later exposed, while post-compromise security concerns recovering protection for subsequent messages after a compromise, under the protocol’s recovery conditions.
The technical paper targets the one-to-one session code in libsignal-protocol version 0.105.4, with the SPQR post-quantum ratchet library at version 1.6.0. Researchers linked the Rust implementation into a small command-line harness and compiled it with the standard Rust compiler for AArch64 Linux, the 64-bit Arm architecture.
Proving properties about that executable reaches into implementation details that design-level analysis leaves out. The work reasons about protocol state machines, message serialization, authentication checks, memory allocation, and the instructions produced by the compiler. The verified libsignal code amounts to roughly 560 kilobytes, or about 140,000 AArch64 instructions.
Its scope is the compiled library in that harness, not the entire Signal mobile application. Low-level cryptographic routines and several supporting functions are represented by trusted contracts describing their behavior, rather than having their implementations proved instruction by instruction.
How Agents Build Proofs Without Setting Their Own Rules
AlphaProof Code separates deciding what to prove from constructing the proof. Human researchers work with specification-writing and reviewer agents to translate security goals from the research literature into Lean definitions and theorem statements. Humans review and approve those specifications before autonomous agents attempt the proofs.
That division addresses a problem in automated verification. A mathematically valid proof can still establish too little if its specification is weak or makes unrealistic assumptions. Researchers had to combine earlier models of Signal’s handshake and ratchet, which had often been analyzed separately, and extend them to the newer protocol.
Gemini Carbon-powered agents then wrote the proofs. Lean’s kernel checks whether their reasoning is valid, so accepting a result does not depend on trusting an agent’s explanation. A separate comparator checks that the submitted proof establishes exactly the approved theorem, including its dependent definitions, rather than an easier substitute.
The paper puts the trusted specifications and machine-code semantics at about 26,000 lines: roughly 18,000 lines of statements and definitions, plus 8,000 lines describing AArch64 behavior. These are distinct from the millions of proof lines that Lean checks automatically. DeepMind says an agent auditing pass highlighted about 1% of the codebase for additional human review.
The researchers also tested whether their specifications could reject insecure implementations. They reintroduced two previously fixed libsignal bugs into isolated copies, recompiled them, and produced machine-checked proofs that the modified binaries violated the symbolic security theorem. The system formally proved the failure rather than simply flagging suspicious code.
Two Security Models, With Different Guarantees
The researchers developed separate symbolic and computational proofs. The symbolic, or Dolev–Yao, model treats cryptographic operations as idealized building blocks: attackers can manipulate messages but cannot break the underlying encryption or forge authentication without the relevant keys.
The computational model instead bounds an efficient attacker’s probability of breaking message confidentiality or authenticity in terms of assumptions about the cryptographic primitives. It connects those security arguments to the compiled executable through a byte-level model of libsignal.
The two approaches have different reach. The symbolic proof includes handshake secrecy against an attacker who later breaks Diffie–Hellman, a capability associated with a future quantum computer. The computational proof covers classical attackers, not quantum adversaries. Neither establishes the post-quantum recovery, or “healing,” that SPQR is designed to provide.
The computational result also uses a restricted attack model, including limits on attacker-supplied initial handshake messages for sessions subsequently used for messaging. Its numerical bound becomes uninformative for multiple long sessions with many key-update epochs. Those conditions define the security statement proved; the result is not an unrestricted guarantee for every Signal deployment.
A team of five carried out the proof work over four weeks, with agents running continuously and researchers directing specifications and proof campaigns. The interview with researcher Swarat Chaudhuri identifies specification design as a remaining human-intensive task as automated proof generation becomes more capable.
Pushmeet Kohli said the team aims to extend the approach to systems such as medical device firmware and power grid software. Researchers building on the Signal result can use the public GitHub repository, which includes the specifications, proofs, machine-code semantics, and instructions for rebuilding the binary and checking the headline theorems against their approved statements.
