DeepMind AlphaProof Code Formally Verifies Signal at Machine-Code Level

Google DeepMind formally verified the security of Signal's cryptographic protocol at the processor instruction level using AlphaProof Code, a multi-LLM agentic framework. Teams of 40 to 80 Gemini Carbon agents generated approximately 6.5 million lines of Lean proof code in four weeks, a task DeepMind said would otherwise take expert teams years or decades. The verification covers libsignal, Signal's reference implementation, and operates at the machine-code level, meaning neither the Rust compiler nor Signal's source code is trusted in the resulting proofs. DeepMind described the result as the first time the actual production code of a widely deployed protocol has been formally verified by any method, with or without AI, and at this depth. AlphaProof Code splits verification labor between human experts, who focus on engineering the formal specification, and AI agents, who carry out the proof work. Lean's automated checking rejects any incorrect proof step the AI writes, so the correctness guarantee does not depend on trusting the AI's output directly. Researchers validated the system by reintroducing two previously fixed Signal bugs into the codebase; AlphaProof Code produced machine-checked proofs of insecurity in both cases. DeepMind is open-sourcing the formal specifications and verification artifacts, and Swarat Chaudhuri said the team plans to work with the open-source community on improving them. DeepMind cited medical device firmware and power grid software as domains where the approach could apply.