Formal verification is a mathematical proof that code does exactly what it was specified to do. It is considered the highest level of security assurance, but it takes a lot of manual work. In AlphaProof Code, according to DeepMind, experts work with models to decide what needs to be proved, and a group of AI agents powered by Gemini Carbon writes the proofs in Lean, which checks every proof automatically. In the end the agents flagged only about one percent of the code for human review.
The company chose the Signal protocol, which encrypts conversations in the Signal app and Google Messages. It says this is the first time AI has formally verified a widely deployed cryptographic protocol at this depth, and the first time the implementation of such a protocol has been verified at all, by any method. The proofs cover properties such as protecting messages before and after a device is temporarily compromised, and reach down to the compiled code. The work took four weeks; DeepMind says such a task used to take expert teams years.
To check that the system can tell correct code from flawed code, the researchers reintroduced two real, previously fixed bugs into an isolated version of the code, and in both cases obtained a machine-checked proof that the flawed version was insecure. Signal's CTO, Ehren Kret, said using AI agents to translate live code into valid Lean theorems is a major breakthrough. DeepMind is open-sourcing its verification artifacts along with a technical paper, and says extending the method to other systems will require more research.