Google DeepMind researchers employed a new agentic AI framework, AlphaProof Code, to formally verify core cryptographic guarantees of the Signal Protocol within a four-week proof-of-concept effort. The analysis targeted the protocol underpinning Signal, Google Messages, and WhatsApp, mathematically confirming the correctness of specific properties without discovering new vulnerabilities in the current implementation. To validate the tool's efficacy, researchers tested AlphaProof Code against older Signal versions containing known, patched flaws; the system successfully identified these vulnerabilities and demonstrated that the flawed protocols could not be verified. This work represents a significant milestone for AI-assisted formal verification, a method long considered a "holy grail" for software security due to its ability to mathematically prove code functions as intended, historically hindered by extreme time and labor costs. DeepMind scientist Swarat Chaudhuri emphasized that while the results are promising, scaling such verification to entire software ecosystems remains a distant goal, noting the current analysis did not extend to the full Signal mobile application. The team is releasing the developed specifications and proofs to support broader formal verification research.