Google DeepMind says it has used its AlphaProof Code framework to formally verify key security properties of libsignal, the reference implementation behind Signal’s messaging protocol. The research used AI agents to produce machine-checked proofs about compiled code, extending formal verification beyond an abstract protocol design and into an implementation used by widely deployed messaging services. The company outlined the work in its November 10 announcement and released a technical paper and verification artifacts.
The project focused on Signal’s post-quantum PQXDH handshake and Triple Ratchet. The paper says the proofs establish forward secrecy, post-compromise security, message confidentiality and authenticity directly for the compiled binary against classical attackers. A separate symbolic proof establishes handshake secrecy against a future quantum attacker. The proof code is checked by Lean’s kernel against specifications reviewed by human experts.
DeepMind said the work took four weeks. Researchers used a human-guided process to turn Signal’s security goals into formal specifications, then assigned autonomous AI agents to generate the proofs. The team also reintroduced two previously fixed bugs into an isolated version of the code, and the system produced machine-checked proofs showing that the modified versions did not meet the security properties.
The result does not mean the entire Signal app has been formally verified. The study examined selected security properties of libsignal in a specific AArch64 Linux build and relies on defined assumptions about cryptographic primitives and some routines called by the program. WIRED’s report said the analysis did not cover the full Signal mobile app and found no new vulnerabilities in the portions examined.
Variants of the Signal protocol are also used by WhatsApp, Meta’s Messenger and Google Messages, according to the paper. The work builds on earlier efforts to verify Signal’s post-quantum cryptography, including the SPQR system and Triple Ratchet and the earlier PQXDH upgrade covered by Abijita. DeepMind has published its specifications and proofs for outside researchers to inspect.
If this article helped you, please consider supporting our work. Every small contribution keeps Abijita.com independent and running.
