Google DeepMind used AI to verify key Signal code properties

AlphaProof Code is a multi-agent AI framework for formal software specification and verification.[1] The researchers used it to verify key security properties of libsignal, Signal’s reference implementation, including properties of the PQXDH handshake and Triple Ratchet.[1] The verified properties include forward secrecy, authentication, post-compromise security and handshake secrecy.[1] The paper says those protocol components are designed to protect messages when some keys are compromised and against future quantum-computing adversaries; the verification concerns the stated properties, not an unrestricted claim that all Signal use is secure.[1]

The framework combines a human-guided agent that writes Lean specifications, formal semantics for AArch64 machine code and autonomous prover agents.[1] The team compiled unmodified libsignal code with the standard Rust compiler into AArch64 Linux machine code, then used contracts to specify low-level cryptographic primitives.[2] The agents generated about 6.5 million lines of machine-checked Lean proof code, relying on about 26,000 lines of trusted specifications and AArch64 semantics.[1] AlphaProof Code accepts a proof only when Lean’s kernel checks it against the approved specification.[1]

The researchers used two standard models of protocol security to verify the code.[2] Their model treats cryptographic primitives as abstract black boxes with standard security properties, and the proof bounds an efficient attacker’s success probability by the hardness of those underlying primitives.[2] The researchers state that the results rely on Lean’s kernel and assumptions about the security of those primitives.[2] The work therefore links specified protocol guarantees to compiled implementation code under those assumptions; it is not evidence that every implementation, configuration or threat has been covered.[1][2]

The researchers describe the work as connecting protocol-level security guarantees to the unmodified code of a widely used cryptographic protocol implementation for the first time.[1] They say the results suggest AI could make formal verification practical for real-world systems.[1] The proof-of-concept was conducted in four weeks, and the researchers describe it as a milestone toward a grand challenge launched in April 2026.[1][3] Signal protects communications for billions of people, and protocol variants are used in Signal, WhatsApp, Meta’s Messenger and Google Messages.[1] The Lean development is available online at the project website.[1]