AI checks Signal's encryption code with mathematical proof

Google DeepMind says AI agents have produced a mathematical proof that the core encryption code in Signal works as designed. The same protocol protects chats in Google Messages. The check took four weeks. According to the researchers, that kind of job has historically taken expert teams years.

What was checked

The target was the Signal protocol, the set of rules that keeps private conversations private for billions of people. The researchers say they proved key security properties of the actual code running on devices, not just the design on paper. One example: messages stay protected before and after a device is temporarily compromised.

How it worked

The tool is called AlphaProof Code. Human experts and AI models first turned Signal's security goals into precise mathematical statements, and people reviewed every one. Then AI agents wrote the proofs in Lean, a computer language that checks proofs automatically. The work ran to millions of lines.

The agents also flagged the parts that needed a human second look. That was about one percent of the work. Lean verified the rest, so experts could spend their time where judgment matters most.

Why the code matters, not just the design

Most checks of encryption systems stop at the design level. The researchers note that real-world flaws often hide in the gap between a design and the code that carries it out. Closing that gap makes the proofs far more complex, which is why the work is described as a first. The team says no widely used protocol of this kind had its implementation formally verified by any method before.

A test with old bugs

To see 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, the system produced a machine-checked proof that the buggy version was insecure.

What it means for you

Nothing changes on your phone, and no action is needed. What changes is the level of assurance. Signal's chief technology officer, Ehren Kret, said that verifying the protocol this way gives the company even greater confidence in its privacy guarantees.

What is still open

• The proof covers Signal's core cryptographic code, not every part of an app.
• The proof shows the code meets the properties experts specified.
• The researchers say scaling this approach needs more research.
• The team is open-sourcing its verification files so others can study them.

The researchers say the approach could later help secure other systems, such as medical device firmware and power grid software. That is a stated goal, not something yet done.