Signal encryption code verified by DeepMind AI in four weeks

What is formal verification?

It means using maths, rather than testing, to show that software does what it is meant to do. It is considered the strongest security guarantee available, but it has been slow and laborious. Most verification of cryptographic protocols stops at the design stage. DeepMind says it went further and checked the actual implementation, which is where real-world bugs often hide. It claims this is the first formal verification of a widely deployed protocol's implementation by any method, with or without AI.

How does the AlphaProof Code system work?

AlphaProof Code combines several AI models with human experts. DeepMind researchers and AI models turned Signal's security goals into formal specifications, and humans reviewed each one. Agents powered by Gemini Carbon then wrote the proofs: more than six million lines of Lean, a language that lets a computer check proofs automatically. The agents audited their own work and flagged about 1% of the code for a second human look.

The proofs cover properties such as keeping messages protected before and after a device is temporarily compromised.

Did it find any bugs?

No new vulnerabilities turned up in the parts of Signal that were analysed. To test whether the system can tell good code from bad, the team put two real, previously fixed bugs back into an isolated copy of Signal's code. In both cases, DeepMind says, the system produced a machine-checked proof that the buggy version was not secure.

There are limits. The whole Signal mobile app was not verified, and DeepMind had a head start from earlier formal verification work by the Signal Foundation. Signal CTO Ehren Kret said that earlier work covered smaller pieces of code, while DeepMind's approach allows significant expansion.

Researcher Swarat Chaudhuri said the team wants to avoid a world where AI writes both the goals and the proofs, effectively grading its own exam. That is why humans reviewed the specifications and flagged sections.

Cost and scale are unclear. DeepMind ran the Signal analysis for free as research and has not said what it cost or whether a commercial product is planned. It is open-sourcing its verification artefacts, and suggests the method could later reach medical device firmware and power grid software.