Introducing AlphaProof Code: a breakthrough in verifying complex

Summary

November 10, 2026 Research Introducing AlphaProof Code: a breakthrough in verifying complex software at depth Pushmeet Kohli and Swarat Chaudhuri Read the technical paper Share How Google DeepMind researchers built a new agentic framework that formally verified the code of Signal’s cryptographic protocol — long considered to be a grand security challenge Today, we’re sharing a milestone in software security long considered to be a grand challenge: Google DeepMind researchers guided AI agents to mathematically prove key security properties of the actual code underlying the Signal protocol, the technology that protects billions of private conversations in apps like Signal and Google Messages. This breakthrough discovery was made using AlphaProof Code, a novel agentic framework for formal verification at unprecedented depth that combines human expertise with AI agents. Formal verification—mathematically proving code runs correctly without flaws—is the highest standard of security assurance; however, it is difficult and often labor-intensive. Our work marks the first time AI has been used to formally verify a widely deployed cryptographic protocol at this depth.