Summary
- Google DeepMind's AlphaProof Code framework combined human oversight with AI agents to formally verify Signal's PQXDH handshake and Triple Ratchet protocols at the machine-code level.
- The process generated 6.5 million lines of Lean proof code over four weeks, with a team of five people and AI flagging sections requiring human review.
- Verification confirmed libsignal's forward secrecy, authentication, post-compromise security, and handshake secrecy properties — though results assume perfect cryptography and do not guarantee computational secrecy of bytes.
- The researchers see specification — deciding what to verify — as the next frontier, not proof generation itself.
- The work is intended as a step toward applying formal verification broadly across software, not just cryptographic protocols.
What happened
Researchers at Google DeepMind have formally verified Signal's post-quantum PQXDH handshake and Triple Ratchet protocols at the machine-code level, using a system called AlphaProof Code. The team, comprising nine researchers including staff from Google DeepMind and academics from the University of Texas at Austin, describe the work as the first time AI has helped devise a proof that connects protocol-level security guarantees to a widely used cryptographic implementation.
How AlphaProof Code works
AlphaProof Code is a multi-agent framework that pairs human oversight with AI-generated reasoning. A human-guided agent translates security goals into a mathematical specification written in Lean, a formal proof language. That specification is then handed to Gemini Carbon agents, which generate Lean code proving the correctness of the underlying implementation. An automated auditing pass identifies areas needing human review before the Lean kernel checks the final proofs against the specification.
Scale and cost
The exercise produced 6.5 million lines of Lean code and took four weeks of work by a five-person team along with what the researchers described as a substantial volume of compute tokens. That compares favourably to prior formal verification projects: verifying the seL4 microkernel took approximately 20 person-years, and the CompCert C compiler required six years to certify. The researchers believe AlphaProof Code can significantly reduce those costs, though the Signal project was not trivial even with AI assistance.
What was verified — and what was not
The verification confirms the design properties of libsignal: forward secrecy, authentication, post-compromise security, and handshake secrecy. It is a theoretical result that assumes perfect cryptography. The researchers are explicit that it does not guarantee the computational secrecy of individual bytes in practice. Security leaders should read this as a meaningful assurance of correctness at the protocol and implementation design level, not an end-to-end operational guarantee.
The harder problem: knowing what to verify
Swarat Chaudhuri, a research scientist at Google DeepMind and professor at the University of Texas at Austin, told The Register that the Signal work exposed a deeper challenge. For decades, he said, the field assumed verification itself was the hard part. AI is now changing that balance. The bottleneck is increasingly specification — determining precisely what properties need to be proven. That process, he noted, remains fundamentally human-dependent, even as AI scales up the proof generation. The researchers see this as the next frontier for the field.
Broader ambition
The team's stated goal extends well beyond Signal. Chaudhuri pointed to the rise in offensive AI capabilities and the volume of insecure software in production worldwide, arguing that formal verification technology needs to be applied broadly across codebases — not only to cryptographic protocols. A related DeepMind project, AlphaProof Nexus, focuses on mathematics, and the Signal work is positioned as a proof of concept for applying similar techniques during the software design process. The work was also undertaken as a step toward a challenge issued by the Beneficial AI Foundation in April to formally verify Signal's protocol and application.
Why it matters
For CISOs, this work matters on two levels. In the near term, it provides credible, independently produced assurance that libsignal's implementation aligns with its stated security properties — relevant for any organisation relying on Signal or Signal Protocol-based products for sensitive communications. At the strategic level, it signals a genuine shift in the economics of formal verification. If AI can reduce verification costs from years to weeks, the case for demanding formal verification of critical software dependencies — not just cryptographic libraries — becomes considerably more practical. The caveat is worth holding: assuming perfect cryptography is a significant abstraction, and operational security still depends on implementation, configuration, and runtime factors that formal verification does not address. The more important takeaway for security leaders may be the specification problem Chaudhuri identifies: before AI can verify that software is correct, humans must define precisely what correctness means. That remains a skilled, judgement-intensive activity — one that security architects and CISOs should expect to be drawn into as these tools mature.
What to do now
- Review your organisation's reliance on Signal or Signal Protocol-based messaging tools in light of this additional assurance, noting it covers libsignal's design properties rather than end-to-end operational security.
- Track the development of AlphaProof Code and similar human-AI formal verification frameworks as potential tools for assurance of critical software dependencies.
- Consider engaging security architects in defining formal security specifications for high-value internal systems, as specification quality will be the limiting factor when AI-assisted verification becomes operationally accessible.
- Monitor the Beneficial AI Foundation's formal verification challenge for further independent assessments of widely used cryptographic software.
