Skip to content
NewsResearch

DeepMind's AlphaProof Code mathematically verifies Signal's encryption in four weeks

· by

The short version

Google DeepMind used AI agents to formally verify the actual production code behind Signal's encryption protocol, a task the company says traditionally takes years, and caught two deliberately planted bugs in the process.

DeepMind's AlphaProof Code mathematically verifies Signal's encryption in four weeks

Google DeepMind said its AI agents produced a mathematical, machine-checked proof that Signal's actual production encryption code, not just its design, meets its security specification, according to a DeepMind blog post by researchers Pushmeet Kohli and Swarat Chaudhuri published November 10.

What

The system, called AlphaProof Code, is a multi-model agentic framework that splits formal verification into two jobs: humans and AI models together decide what to prove, then AI agents do the proving, per the blog post. Human experts translated Signal's security goals into formal specifications, then agents built on Google's Gemini Carbon model generated more than six million lines of proof in the Lean formal-verification language, with roughly 1% of the codebase flagged back to humans for review. DeepMind says this is the first time AI has formally verified a widely deployed cryptographic protocol at the level of its actual running code, and the first time any method, AI or not, has verified that implementation gap for a protocol this widely used. To test the system, researchers reintroduced two previously fixed, real bugs into an isolated copy of Signal's code; AlphaProof Code produced a proof in both cases showing the buggy version was insecure. DeepMind put the total verification effort at four weeks, a task it says historically takes expert teams years.

What this changes for AI-driven software security

Most formal verification work stops at the design stage, checking that a protocol's blueprint is sound rather than that the shipped code matches it, per DeepMind's description of prior work. Signal CTO Ehren Kret said the new approach "enables significant expansion" beyond that limited scope, calling the use of AI agents to translate live code into valid Lean theorems "a major breakthrough" that gives Signal "even greater confidence" in its privacy guarantees as AI-driven security threats grow, per the same post. For security teams at other companies running cryptographic or safety-critical code, the result is a data point that formal verification, previously too slow and expensive for anything beyond a protocol's design, may now be tractable for production implementations on a weeks-not-years timeline. DeepMind is open-sourcing its formal verification artifacts and published a technical paper alongside the announcement, giving outside researchers a path to inspect the method rather than take DeepMind's word for it.

What to watch next

DeepMind's post says the technique could extend to medical-device firmware and power-grid software, paired with its separate CodeMender agent for automated defense; watch for a named pilot in either sector and for independent cryptography researchers to review the open-sourced artifacts and attempt to reproduce the Signal result.

Sources