Google DeepMind announced on Tuesday that its AI agents have mathematically proved that the code behind Signal’s encryption protocol does what it promises, a milestone the lab calls the first formal verification of a widely deployed cryptographic protocol at this depth. The work, carried out by a new system called AlphaProof Code, took four weeks, a task DeepMind says would historically have taken expert teams years. The lab is open-sourcing the proofs and specifications so other researchers can build on them.
How the proof was built
AlphaProof Code works the way a research team would, DeepMind says, splitting formal verification into stages and letting AI agents handle the heavy lifting. Human experts first worked with several AI models to turn Signal’s security goals into formal mathematical specifications, reviewing every one of them before any proving began.
Agents powered by Gemini Carbon, a DeepMind model, then wrote the proofs in Lean, a language built for machine-checked mathematics, producing more than six million lines of proof code. The agents then audited their own work and flagged just one percent of it for a second look by humans, with the Lean checker verifying the rest automatically.
What was actually proved
Crucially, the team did not stop at Signal’s design. Most protocol verification checks the design on paper, but DeepMind’s agents proved that the compiled code itself delivers the key security properties, down to the exact code running on devices in practice.
That matters because real flaws often hide in the gap between a design and its implementation, and bridging that gap is what makes these proofs far harder to produce. The verified properties cover Signal’s post-quantum handshake, known as PQXDH, and its Triple Ratchet, which keeps refreshing encryption keys as a conversation continues.
To check that the system can tell good code from bad, the researchers reintroduced two real, previously fixed bugs into an isolated copy of Signal’s code. In both cases AlphaProof Code produced a machine-checked proof that the buggy version was insecure, a result DeepMind presents as evidence the framework catches flaws rather than rubber-stamping whatever it is shown.
What it does not prove
The result is narrower than a clean bill of health for Signal, and DeepMind does not present it as one. The proof covers the core cryptographic protocol code, not the full Signal mobile app, and it treats the low-level cryptographic building blocks as assumed-secure rather than proving them from scratch.
It also targets one compiled platform, and the analysis found no new vulnerabilities in the parts it examined. Signal’s chief technology officer, Ehren Kret, called the approach a great breakthrough that gives greater confidence in the code’s privacy guarantees as AI-driven security threats grow.
Our Read
The headline here is not that Signal is now unhackable, and anyone reporting it that way would be overstating the result. The headline is that formal verification, long the slowest and most expensive form of security assurance, has just been compressed from years to weeks on one of the hardest targets in software.
That changes the economics of proving code correct, which is why DeepMind is already pointing the method at medical device firmware and power grid software. Paired with automated defense agents like the lab’s CodeMender, verification of this kind could become a routine step in shipping software, rather than a luxury reserved for the most sensitive systems.
There is also a quiet competitive signal in the announcement. DeepMind built the proofs with Gemini Carbon, and the Signal result is the first public demonstration of what that model can do at serious depth. For a lab whose models are usually judged on benchmarks, a machine-checked proof of real-world code is a different kind of result to show.
The lab’s rivals have their own verification efforts, but none has yet shown a machine-checked proof of a protocol used by billions of people. That gap is the real measure of this announcement: not the size of the proof, but the fact that it exists at all for code this widely deployed.
Why It Matters
Software security has always rested on testing, which can only show that known bugs are absent, not that unknown ones are too. A machine-checked proof raises the bar: it shows the code meets its stated properties by construction, and it can be re-checked by anyone with the open-sourced artifacts.
If this approach scales, the most sensitive software in the world could carry proofs instead of promises, and users would no longer have to take a vendor’s word for it. That is the promise DeepMind is selling, and the Signal proof is the first evidence it can deliver on it at real-world scale.
The timing is pointed. Recent breaches have shown how much sensitive data can leak when AI systems are built fast and checked late, and formal verification offers the opposite discipline: proof before deployment, not apologies after a breach in the first place.
Background
Formal verification has been used for decades on small, critical systems, from aircraft controls to chip designs, but applying it to production software at this scale was long considered impractical. DeepMind’s result answers a challenge issued in April by the Beneficial AI Foundation to formally verify the Signal protocol, and the lab says its next targets include other vital systems.
Source: DeepMind’s announcement and The Register’s report.
0 Comments