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

Google DeepMind has introduced AlphaProof Code, an AI system that produces mathematical proofs that software meets its security specifications. According to a blog post by DeepMind researchers Pushmeet Kohli and Swarat Chaudhuri, the team tested it on the encryption protocol of the messaging app Signal. The system finished in four weeks verification work that usually takes years. Earlier efforts to verify the protocol covered only its theoretical design. AlphaProof Code instead checked the cryptographic core code that runs on users' devices. First, human experts wrote the formal security requirements. AI agents built on Gemini Carbon then helped refine the specifications and proved, on their own, that the code satisfies them. The agents wrote more than six million lines in the Lean proof language and flagged about one percent of the codebase for human review. Two bugs the researchers planted for testing were caught immediately. Signal CTO Ehren Kret said the approach strengthens trust in data privacy as AI-driven threats grow. DeepMind plans to apply the method to power grids and medical devices through systems such as CodeMender. Formal verification has usually been too slow and expensive for most production software. If the result holds up more widely, more critical code could be proven correct, not just tested.