DeepMind says AlphaProof Code verified parts of Signal’s code

Google DeepMind said on 10 November that researchers used a framework called AlphaProof Code to formally verify key security properties of the code underlying the Signal protocol. The post says this is the first time AI has been used to verify a widely deployed cryptographic protocol at this depth, and the first time this implementation has been formally verified by any method. It says the agents, powered by Gemini Carbon, proved that the compiled code meets specified properties, including protection of messages before and after a device is temporarily compromised, down to the code running on devices.

The post says the work generated over six million lines of Lean, a language used to state mathematical proofs about code, and that the verification took four weeks. It says the agents marked areas for a second look by a person, and that those areas were one percent of the codebase. It does not say that humans wrote none of the proof, and it does not give a count of machine-code instructions. DeepMind says it put two previously fixed bugs back into an isolated copy of Signal’s code, and that the system produced a machine-checked proof that each buggy version was insecure.

Ehren Kret, Signal’s chief technology officer, is quoted saying that earlier formal verification covered smaller portions of the code, and that DeepMind’s approach expands that coverage. He said the work gives Signal greater confidence in the privacy guarantees of the implementation. The post is DeepMind’s account. It does not attach the proof files.