A formal verification task that historically required expert teams years to complete was accomplished in four weeks on Thursday when Google DeepMind researchers used agentic AI to mathematically prove key security properties of the Signal protocol, according to HPCwire.
Formal verification uses mathematics to prove that code runs correctly without flaws, representing the highest standard of security assurance. Most protocol verification previously stopped at the design level, but the new framework reached down to the compiled code running on devices.
The system, called AlphaProof Code, operates as a multi-LLM agentic framework. Human experts collaborated with models to translate Signal security goals into formal mathematical specifications, reviewing every one. Agents powered by Gemini Carbon then executed the proofs, generating over six million lines of Lean, a computer language that mathematically proves code accuracy.
The agents audited their own proofs, highlighting areas that required a second look by a human. That review covered just one percent of the codebase, saving substantial time and allowing Google DeepMind experts to focus on complex judgments.
"While prior formal verification focused on smaller portions of the code, Google DeepMind’s approach verifies much larger sections of the code." Using AI agents to translate live code into valid Lean theorems is a major breakthrough,” said Ehren Kret, CTO of Signal.”
Ehren Kret, CTO of Signal, told HPCwire.
To test the framework’s reliability, researchers reintroduced two real, previously fixed bugs into an isolated version of Signal’s code. In both instances, the system produced a machine-checked proof confirming that the buggy versions were insecure.
The research demonstrates how AI can bring elite security assurance to critical infrastructure, laying groundwork to secure medical device firmware and power grid software. However, broader adoption faces practical hurdles.
“We are very excited by this result, but there is a long distance to go before we are able to scale this to all the software of the world, and we want to do that,” said Swarat Chaudhuri, a DeepMind research scientist.
Swarat Chaudhuri, a DeepMind research scientist, told WIRED.
WIRED said that while AI-aided formal verification is gaining traction, it remains unclear how practical the approach will be for widespread use and how effectively it can secure larger quantities of code. Google DeepMind is open-sourcing its formal verification artifacts for community use.
