Google DeepMind uses AI to formally verify Signal’s cryptographic code

AI agents verify Signal’s implementation

AlphaProof Code is a multi-LLM agentic framework designed for formal verification, which mathematically proves that code runs correctly without flaws. Google DeepMind researchers used it to examine the actual implementation of Signal’s cryptographic protocol, rather than stopping at the protocol’s design.

The work focused on security properties including keeping messages protected before and after a device is temporarily compromised. According to Google DeepMind, the researchers first worked with a mix of models to translate Signal’s security goals into formal mathematical specifications. Human experts reviewed every specification before the proof work began.

AI agents powered by Gemini Carbon then generated more than six million lines of Lean, a computer language used to mathematically prove the accuracy of code. The agents also audited the proof and identified areas requiring additional human review. Google DeepMind says those areas represented one percent of the codebase, while Lean automatically checked the rest.

A four-week process for a long-standing security challenge

Cryptographic protocols support digital communication including online banking and web browsing, and a single flaw can expose millions of people. Experts have therefore spent decades formally analyzing such systems, but most protocol verification has focused on the design level.

Google DeepMind says its approach bridged the gap between a cryptographic design and the compiled code running on devices. That makes the verification substantially more complex, because vulnerabilities can appear between an intended design and its implementation.

Despite that complexity, the company says the verification process took four weeks, compared with expert-team tasks that historically take years. To test whether AlphaProof Code could distinguish correct code from buggy code, researchers 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.

“Using AI agents to translate live code into valid Lean theorems is a major breakthrough,” said Ehren Kret, Signal’s chief technology officer, according to the Google DeepMind announcement. Kret said rigorous verification of the Signal protocol implementation gives Signal greater confidence in its code’s privacy guarantees.

What the work could mean for software security

Google DeepMind says the research could help extend formal verification to businesses, governments and critical infrastructure as AI-driven security threats grow. It identifies systems such as medical device firmware and power grid software as potential areas for applying the techniques.

The company also says AlphaProof Code can help users write a specification before autonomously proving that an implementation meets it, with every proof checked by Lean. Google DeepMind has open-sourced its formal verification artifacts for community use, while stressing that scaling the techniques will require continued research.

The work is presented as a foundation for combining formal verification with automated defense agents such as CodeMender. For users, the immediate significance is the additional mathematical assurance claimed for Signal’s core cryptographic code. For the wider software market, the research points to a way of applying deep, machine-checked verification to production systems that has traditionally required extensive manual effort.