What Google DeepMind announced
On 10 November 2026 Google DeepMind described a result it calls a milestone in software security. Its researchers directed AI agents to prove mathematically that the real code behind the Signal protocol meets key security properties. The protocol protects private conversations for billions of people in apps such as Signal and Google Messages, according to the company.
The work used AlphaProof Code, which DeepMind presents as a new agentic framework for formal verification that pairs human expertise with AI agents. Formal verification means proving mathematically that code behaves correctly, which the company calls the highest standard of security assurance, though slow and labour-intensive. DeepMind claims two firsts: AI had not previously verified a widely used cryptographic protocol to this depth, and no method, AI-assisted or not, had verified the implementation of such a protocol before.
How the verification worked
DeepMind says AlphaProof Code splits the job much as a research team would. Human experts and AI decide what needs proving, and a group of agents then carries out the proofs. Researchers worked with several models to turn Signal's security goals into formal mathematical specifications, and human experts reviewed each specification.
Agents powered by Gemini Carbon then wrote the proofs, producing over six million lines of Lean. Lean is a language whose checker confirms that proofs are valid. The agents audited their own output and flagged the parts needing a closer human look, which DeepMind puts at one percent of the codebase. Lean verified the rest automatically, so reviewers could concentrate where judgment matters.
DeepMind stresses that the proofs go beyond the protocol's design. They address the compiled code that runs on devices, including guarantees such as keeping messages protected before and after a device is briefly compromised. The company argues that flaws often sit between design and implementation, which makes proofs at this level far more complex. It reports the verification took four weeks, a task it says has historically taken expert teams years.
Testing, limits and next steps
To check that the system distinguishes sound code from faulty code, DeepMind reinserted two genuine bugs, both fixed earlier, into an isolated copy of Signal's code. According to the company, the system returned a machine-checked proof of insecurity for the buggy version in both cases.
DeepMind says the result lays groundwork for securing other critical systems, naming medical device firmware and power grid software, and that it could help defend against agent-driven cyber threats. It adds that scaling the techniques needs further research, and that pairing formal verification with automated defence agents such as CodeMender could help counter the speed and scale of modern attacks. The company is open-sourcing its verification artifacts and has published a technical paper. It credits Signal staff with feedback on the methodology. All claims in this report come from DeepMind's own announcement.