Google DeepMind has introduced AlphaProof Code, a framework that combines human supervision and AI agents to prove selected security properties of Signal’s cryptographic implementation. The November 10 research moves beyond abstract protocol analysis to a compiled program.
Human experts review the mathematical specifications before agents generate proofs. Lean’s kernel checks those proofs against the approved statements, making the specification and checker central to the result.
The technical paper describes a particular build of libsignal v0.105.4, linked into a command-line harness and compiled for AArch64 Linux. Its analysis covers one-to-one sessions using PQXDH and the Triple Ratchet; group messaging remains future work.
The researchers report proofs covering properties such as forward secrecy, authentication and post-compromise security. These guarantees depend on trusted specifications, the machine model, Lean’s kernel and assumptions about cryptographic primitives and external routines.
The practical value is evidence connecting stated security goals to an implementation that people use. The scope remains specific: the work does not certify the entire Signal application, its surrounding infrastructure or every possible security property. Human review of what the system is asked to prove remains essential.
