Google DeepMind's AlphaProof Code formally verifies the Signal protocol's cryptographic code in four weeks

Google DeepMind used a new AI framework called AlphaProof Code to formally verify key security properties in the implementation of Signal's cryptographic protocol, the lab said on 10 November. It calls this the first time AI has been used to formally verify a widely deployed cryptographic protocol at this depth. Researchers completed the project in four weeks and, Wired reports, did not find new vulnerabilities in the parts of the protocol they examined.

Human experts worked with AI models to convert Signal's security requirements into mathematical specifications. Agents powered by Gemini Carbon then generated more than six million lines of Lean proofs, and the agents flagged about one percent of the codebase for a second look by a human.

The verification covered Signal's core cryptographic code rather than the entire Signal mobile app. Researchers also tested isolated code containing two previously fixed bugs, and AlphaProof Code produced machine-checked proofs showing that both versions were insecure.

Google DeepMind is open-sourcing its verification artifacts. Google declined to share the cost of the analysis or say whether it plans a commercial formal verification product, according to Wired.