Google DeepMind's AlphaProof Code Formally Verifies Signal's Cryptographic Protocol

Google DeepMind says it has reached a milestone in software security long considered a grand challenge: its researchers guided AI agents to mathematically prove key security properties of the actual code underlying the Signal protocol, the technology that protects billions of private conversations in apps such as Signal and Google Messages by encrypting messages end to end so that only the sender and intended recipient can read them. The announcement was published on the Google DeepMind blog by Pushmeet Kohli and Swarat Chaudhuri.

The result was achieved with AlphaProof Code, a novel agentic framework for formal verification at unprecedented depth that combines human expertise with AI agents. Formal verification — mathematically proving that code runs correctly without flaws — is the highest standard of security assurance, but it is difficult and often labor-intensive. Conventional testing samples a program's behavior; a formal proof rules out flaws across every possible execution — a level of assurance so costly to produce that it has rarely reached widely deployed software.

According to the company, the work marks the first time AI has been used to formally verify a widely deployed cryptographic protocol at this depth. It is also the first time the implementation of a widely deployed protocol of this kind has been formally verified by any method, with or without AI.

How Google DeepMind verified Signal

AlphaProof Code is a multi-LLM agentic framework that splits the work of formal verification the way a research team would: human experts work with AI to decide what to prove, and a group of AI agents carries out the proofs.

First, Google DeepMind researchers collaborated with a mix of models to translate Signal's security goals into formal mathematical specifications, with human experts reviewing every one. Agents powered by Gemini Carbon then did the proofs, generating more than six million lines of Lean, a computer language that mathematically proves the accuracy of code.

The agents next audited the proof and highlighted the areas that needed a second look from a human — just one percent of the codebase, which the company describes as a massive time savings. Because Lean automatically checks the rest, experts were able to focus their review where human judgment matters most.

Proving security down to the running code

Cryptographic protocols underpin nearly all digital communication, from online banking to web browsing, and a single flaw can expose millions of people at once. That is why experts have spent decades formally analyzing them, though most protocol verification has stopped at the design level.

Google DeepMind's agents went further, proving that the compiled code fulfills key security properties — such as keeping messages protected before and after a device is temporarily compromised, guarantees cryptographers know as forward secrecy and post-compromise security — down to the exact code running on devices. Real-world vulnerabilities often hide in the gap between design and implementation, and bridging that gap makes these proofs vastly more complex.

Even at this level of complexity, the verification process took just four weeks — a task that historically takes expert teams years, according to the company — establishing that Signal's core cryptographic code delivers the security protections the researchers specified.

To confirm that AlphaProof Code can distinguish correct code from buggy code, the team reintroduced two real, previously fixed bugs into an isolated version of Signal's code. In both cases, the system produced a machine-checked proof that the buggy version was insecure — a check that matters, since a verifier unable to flag flawed code would provide false assurance.

In AlphaProof Code, AI agents help users write a specification and then autonomously prove that the implementation meets it. Every proof is checked by Lean to verify the agents' work.

Signal's response

"While prior formal verification focused on smaller portions of the code, Google DeepMind's approach enables significant expansion," said Ehren Kret, Chief Technology Officer of Signal. "Using AI agents to translate live code into valid Lean theorems is a major breakthrough. As AI-driven security threats grow, rigorously verifying the Signal protocol implementation gives us even greater confidence in our code's privacy guarantees."

The future of security

Google DeepMind argues that clearing this long-standing challenge demonstrates how AI can bring elite security assurance to businesses, governments, and critical infrastructure, helping defend against agent-driven cyber threats. Verifying Signal's core cryptography, the company says, lays the groundwork to secure other vital systems, from medical device firmware to power grid software.

Scaling these techniques requires continued research. Paired with automated defense agents such as CodeMender, formal verification can help counter the speed and scale of modern cyber threats and create software with mathematical proof that its protections work.

Google DeepMind is open-sourcing its formal verification artifacts for community use, hosted at google-deepmind.github.io/code-verification. The full technical paper is available as a PDF. For the security research community, that publication provides a way to inspect the machine-checked proofs and methodology directly — and how far verification at this depth spreads beyond Signal, into the medical, industrial, and infrastructure systems the company names, is the development to watch next.

Acknowledgements

The research was developed by Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, Charles Sutton, and Pushmeet Kohli.

The team thanked Eric Wieser for help with open-sourcing the code, Owen Jones for program management support, and Martín Abadi, Christopher Henson, Katerina Hristova, Henryk Michalewski, Jonathan Protzenko, and George Tsoukalas for helpful discussions. The researchers also thanked Signal's Rolfe Schmidt, Michael Rosenberg, and Ehren Kret for feedback on the methodology, as well as Tulsee Doshi, Four Flynn, Kate Olszewska, Alicia Huang, Andy Liu, Benoit Schillings, Raluca Ada Popa, Melvin Johnson, Koray Kavukcuoglu, Demis Hassabis, and Sundar Pichai for their support of the project.