DeepMind uses AI to verify security properties in Signal’s cryptographic code

Google DeepMind released AlphaProof Code on November 10, reporting AI-assisted mathematical verification of selected security properties in Signal’s cryptographic implementation. The team published specifications and proofs from a four-week project, allowing outside researchers to inspect what was established and under which assumptions. Lean, a theorem prover, checks the agents’ proof work.

The target is libsignal’s one-to-one session code. Researchers linked the unchanged library to a small command-line harness and compiled an AArch64 Linux executable, analyzing session initialization and message sending and receiving. Some low-level cryptographic operations are assumed to satisfy specified contracts. Key generation remains outside the verified scope. The result does not establish the security of the entire Signal mobile application.

PQXDH establishes a shared secret when two parties begin communicating, including when the recipient is offline, using public key material previously uploaded to a server. The subsequent Triple Ratchet combines the established Double Ratchet with a post-quantum key-evolution mechanism. The verification reaches the machinery that updates message keys as a conversation proceeds. Signal’s specification also stores skipped message keys to handle out-of-order delivery, then removes a stored entry when retrieving that key. Arrival order and key retention are part of the state changes the implementation handles.

In Signal’s specifications, forward secrecy protects messages whose keys were erased before a later compromise of current state. Post-compromise security concerns recovery for future messages after an intrusion ends and fresh secrets enter the key schedule. PQXDH targets post-quantum forward secrecy, while its current mutual authentication still relies on elliptic-curve hardness.

Humans first decided which security properties to establish. AI helped translate those goals into specifications that people reviewed and approved; Gemini Carbon-powered agents then produced proofs. Lean checks whether the submitted reasoning follows from the approved statements. Choosing a meaningful security requirement remains a human responsibility.

What remains outside the generated proof

The paper reports about 6.5 million lines of Lean proof code, alongside roughly 26,000 lines of trusted specifications and AArch64 semantics. A large checked proof still rests on the definition of security and assumptions about execution. Connecting the result to machine code reduces reliance on assuming that compilation preserved the intended behavior.

The checking process also compares the target statement and its definitions with a held-out challenge. Comparator, used by the project, checks that the proof establishes the same claim, uses permitted axioms and passes the Lean kernel. This guards against accepting a proof that quietly substitutes an easier requirement. Comparator also assumes a trustworthy challenge and its dependent definitions, and correctness of the checking kernel.

The research uses two security models. Symbolic reasoning treats cryptographic operations as abstractions with stated properties; computational reasoning relates an attacker’s success to assumptions about cryptographic difficulty. The computational documentation explicitly uses classical portions of the underlying analyses. Its documentation separates security-game definitions and cryptographic assumptions from checked proofs, with additional tests for consistency and non-vacuity. That scope supplies no blanket guarantee against quantum attacks.

Researchers separately reintroduced two previously fixed bugs into test binaries. In both cases, Lean checked a proof that the selected symbolic security statement failed.

The public repository maps paper results to Lean code and documents how to reproduce the executable and recheck proofs. Its instructions describe several hours of checking and roughly 15–34 GiB of peak memory use.

The repository generally uses Apache 2.0 licensing; copied Signal libsignal code retains its AGPL 3.0 license.