DeepMind’s AI verifies Signal’s encryption code

Google DeepMind has used AI to produce mathematical proofs of security properties for compiled Signal encryption code. Its AlphaProof Code announcement on 10 November describes human-guided agents doing the proof work, with the results checked by the Lean proof assistant.

The target was a particular build of libsignal, the library implementing Signal’s messaging cryptography. The achievement connects security claims to executable code, with precise conditions defining the guarantee. That brings mathematical verification closer to the software carrying private conversations.

The AI writes a proof that a checker can inspect

AlphaProof Code separates writing the proof from checking that it establishes the approved claim. DeepMind says humans reviewed the formal specifications, which express security requirements in mathematical language. Gemini-powered agents then generated proofs against those requirements.

Think of a specification as a precise contract: which attacker actions are allowed, which secrets may be exposed and which messages should remain protected. A proof must account for all behaviour permitted by that contract. Ordinary tests exercise selected examples; formal verification establishes a stated property across its defined model.

The released checking system uses Lean’s proof checker and a comparator that checks the theorem against the approved specification, including its dependencies. This helps prevent an agent from making its assignment easier by changing the claim it has to prove. Readers can assess the specification as well as the proof.

The proof reaches the compiled program

The verified target combines libsignal 0.105.4 and SPQR 1.6.0 in an AArch64 Linux command-line harness, according to the released repository. AArch64 is the 64-bit Arm instruction set. The harness provides a defined way to run the library’s operations.

That choice addresses a difficult engineering problem. A cryptographic design can be sound while its implementation mishandles stored keys, message ordering or session changes. Reasoning about the compiled program brings those implementation steps into the argument.

DeepMind’s paper reports about 6.5 million lines of machine-checked proof, produced by a five-person team working with agents over four weeks. The compiler’s output is part of the proof target: compiler correctness therefore sits outside the trusted assumptions.

Keys can protect messages across a compromise

The security goals include confidentiality, authentication, forward secrecy and recovery after a key compromise, within the paper’s attacker models. Signal’s ratchet specification explains why changing keys throughout a conversation is central to these protections.

Forward secrecy protects earlier messages when later keys are exposed, provided the relevant earlier secrets have been securely deleted. Post-compromise security concerns later messages: after an attacker loses access, an honest exchange of fresh secret material without active interference can allow the conversation to recover. The necessary exchanges and deletion rules determine when that recovery occurs.

Signal’s Triple Ratchet design combines its existing Double Ratchet with a post-quantum ratchet. For a reader, the useful picture is a conversation whose keys keep evolving. A stolen key has a particular reach; the protocol works to contain that reach over time.

The quantum result has a specific reach

The paper’s computational guarantees concern classical attackers; its symbolic proof also addresses handshake secrecy against a future quantum attacker. Computational analysis bounds an attacker’s success using assumptions about cryptographic difficulty. Symbolic analysis reasons about protocol actions with idealised cryptographic building blocks.

The handshake is the initial exchange that establishes a shared secret. Signal’s PQXDH specification describes post-quantum forward secrecy while retaining a classical assumption for authentication. Those distinctions are essential to understanding which threat a guarantee addresses.

For people concerned about someone recording encrypted traffic today and attempting to decrypt it with a future quantum computer, protection of that initial secret is a particularly relevant goal.

Human review defines the guarantee

Confidence depends on the specification, the proof checker and the assumptions connecting the model to execution. The study uses contracts for cryptographic primitives and some other routines, alongside a defined machine and operating-system environment. Its theorem covers that harness build; applying the result to a full messaging application requires additional work across the application’s components.

DeepMind also reintroduced two previously fixed bugs and generated proofs demonstrating their insecurity. This checked whether the formal requirements were strong enough to expose real historical failures.

The public artifacts already show how the trusted boundary can shrink. An 11 November repository update verified ten more library routines, reducing the count of trusted hooks from 37 to 27. Each proved routine moves another piece of behaviour into the checked argument.

That offers a practical direction for secure software: a precise claim, an identifiable program and a proof that other people can inspect and check. As code changes, maintaining that connection becomes an ongoing engineering task.