Google DeepMind said Tuesday it used AlphaProof Code to examine selected security guarantees in a compiled Signal messaging binary, bringing machine-checked review to implementation details where coding errors can weaken a sound protocol design.
The test covered a small command-line program linked with libsignal, Signal’s reference implementation, and focused on one-to-one session setup and message exchange. It did not verify all of libsignal: the paper excludes key generation. Researchers checked the program’s compiled AArch64 binary.
A paper by Google DeepMind and Google researchers says AI agents generated about 6.5 million lines of proof code in Lean. The system relied on about 26,000 lines of trusted security specifications and AArch64 machine-code semantics. Lean’s kernel checked the agents’ proofs against those specifications.
Computational analyses of PQXDH with the Triple Ratchet addressed classical attackers and examined message confidentiality, authenticity, forward secrecy and post-compromise security under stated assumptions about cryptographic primitives. Separately, a symbolic proof established handshake secrecy against a future quantum attacker.
Google DeepMind said the work took four weeks. The agents flagged roughly 1% of the codebase for closer human review. As a check, the team restored two historical bugs in test binaries; machine-checked proofs showed that each violated a symbolic security theorem.
Signal Chief Technology Officer Ehren Kret said the expanded verification increased his confidence in the privacy protections provided by Signal’s code. Google DeepMind said it released the verification materials for public use.
