Google DeepMind Uses AI Agents to Verify Signal’s Cryptographic Code

Google DeepMind used its AlphaProof Code framework to verify key security properties in Signal’s cryptographic protocol down to machine code, showing how AI-assisted checks can reach software implementation.

Researchers and AI agents translated Signal’s security goals into mathematical specifications, which human experts reviewed. Agents powered by Gemini Carbon then generated proofs that Lean checked, producing more than 6 million lines of machine-checked proof.

The work covered forward secrecy, authentication and post-compromise security. It also tested implementation details, where flaws can arise even when a protocol’s design is sound.

The framework found security weaknesses in isolated versions of Signal’s code that contained previously fixed bugs that had been reintroduced. The findings concern those isolated versions.

The verification was completed in four weeks, a process that could take years. Human experts audited 1% of the codebase.

Google DeepMind open-sourced the project’s formal verification artifacts for researchers to build on. Cryptographic protocols also underpin services such as online banking and web browsing.

In separate research, Google DeepMind’s AI-assisted RSA work identified two weaknesses in traditional 1,024-bit cryptosystems; the company said modern 2,048-bit systems were unaffected.