Google DeepMind's AI proves Signal's encryption code secure, writing 6M lines of proofs with humans checking just 1%

Google DeepMind says AI agents have mathematically proven that the Signal protocol is secure down to the code that actually runs on devices. The company says it is the first time the implementation of a widely deployed cryptographic protocol has been formally verified by any method, with or without AI.

According to a DeepMind blog post dated Nov 10, agents powered by Gemini 4 Carbon in its new agentic framework, AlphaProof Code, wrote more than 6 million lines of proofs in the Lean language, leaving human experts to review only the critical 1%. The job took four weeks, work DeepMind says has historically taken expert teams years. Most protocol verification stops at the design level, but these proofs cover the compiled code. When researchers reinserted two real, previously fixed bugs, the system produced a machine-checked proof that the buggy version was insecure both times.

"Using AI agents to translate live code into valid Lean theorems is a major breakthrough," said Signal CTO Ehren Kret. The protocol protects billions of conversations in apps like Signal and Google Messages. DeepMind's post on X passed 1,000 likes in about two hours, with one reply asking whether it covers "the app people actually install or just the reference impl." DeepMind is open-sourcing the verification artifacts and named medical device firmware and power grid software as next targets.