Google DeepMind Verifies Signal Crypto Code With AI Agents

Google DeepMind generated more than 6 million lines of machine-checked proofs verifying Signal's cryptographic protocol down to machine code, completing in four weeks a formal verification effort that traditionally spans years.

The project used DeepMind's AlphaProof Code framework to test key security properties in Signal's implementation, not just its protocol design. Researchers and AI agents first translated Signal's security goals into mathematical specifications, which human experts reviewed. Agents powered by Gemini Carbon then generated proofs that the Lean proof assistant checked mechanically.

The verified properties covered forward secrecy, authentication and post-compromise security. The work also reached implementation-level details, the layer where flaws frequently appear even when a protocol's underlying design is sound.

What did the verification find?

The framework identified security weaknesses in isolated versions of Signal's code. Those versions contained previously fixed bugs that had been reintroduced, and DeepMind stressed the findings concern only those isolated builds, not Signal's production code. The result demonstrates the tooling can catch regression-class defects that slip past design-level review.

Human experts audited 1% of the codebase, meaning the overwhelming majority of the proof burden fell to the machine side of the pipeline. That ratio frames the operational trade-off: verification depth scaled by orders of magnitude, while human oversight concentrated on specification quality rather than line-by-line proof checking.

DeepMind open-sourced the project's formal verification artifacts so other researchers can extend the work. The stakes reach beyond messaging. Cryptographic protocols underpin online banking and web browsing, and reusable verification tooling could shorten audit cycles across both industries.

How does this fit DeepMind's broader crypto research?

In separate research, Google DeepMind's AI-assisted RSA work identified two weaknesses in traditional 1,024-bit cryptosystems. The company said modern 2,048-bit systems were unaffected, a distinction that matters for institutions still running legacy key sizes.

Together, the two efforts position AI agents as a working component of cryptographic assurance, not a research curiosity. Formal verification has historically cost too much in expert time for widespread adoption; a four-week turnaround on a protocol as widely deployed as Signal changes that calculus.

The immediate watch item is uptake. If independent auditors and protocol teams begin building on the released Lean artifacts, AI-assisted verification could shift from a DeepMind demonstration to a standard step in cryptographic release engineering within the current development cycle.