Google DeepMind has introduced AlphaProof Code, an AI framework it used to formally verify key security properties of the code behind the Signal protocol. The company says the work reached the compiled code that runs on devices, rather than stopping at a description of how the protocol should work.
Formal verification uses mathematical proofs to check whether code meets specified requirements. Google DeepMind says this is the first time the implementation of a widely deployed cryptographic protocol has been verified at this depth, with or without AI.
Researchers set the goals and agents built the proofs
Researchers worked with AI models to turn Signal’s security goals into mathematical specifications. Human experts reviewed every specification. Agents powered by Gemini Carbon then generated more than six million lines of Lean, a language used to write proofs that a computer can check.
The agents also flagged areas for further human review. According to Google DeepMind, those areas amounted to one percent of the codebase, while Lean checked the proofs for the rest. The verification took four weeks and covered protections specified by the researchers, including protection of messages before and after a device is temporarily compromised.
To test whether the framework could identify faulty code, the researchers reintroduced two previously fixed bugs into an isolated version of Signal’s code. Google DeepMind says the system produced a machine-checked proof that the buggy version was insecure in both cases.
The company says it is open-sourcing the formal verification artifacts for community use.
