Most software security is testing. You run the code, throw bad inputs at it, and hope the bug you missed is not the one somebody else finds. Formal verification is different. You state, in mathematics, what the code is supposed to guarantee, and then you prove it actually delivers. It is the strongest assurance we have, and so slow and expensive that almost nobody does it for production code.
That is why I paid attention to what Google DeepMind announced on November 10.
What happened
DeepMind says its researchers built a new agentic framework called AlphaProof Code and used it to formally verify the actual code underneath the Signal protocol — the technology behind private conversations in Signal and Google Messages. DeepMind describes this as the first time AI has been used to formally verify a widely deployed cryptographic protocol at this depth, and the first time an implementation like this has been verified at this depth by any method.
The division of labor matters. Human experts worked with a mix of models to translate Signal’s security goals into formal specifications, and reviewed every one. Then AI agents, powered by Gemini Carbon, did the proving work, generating over six million lines of Lean — the language the proofs are written and machine-checked in. The agents also flagged the small part that needed a second look from a human. DeepMind puts that at about one percent.
Two details keep this from being just a press release. First, the team did not stop at the design. They proved properties of the compiled code, down to the code that runs on devices — where real flaws often hide, in the gap between a good design and an imperfect implementation. Second, they tested the tester: they put two real, previously fixed bugs back into an isolated copy, and in both cases the system produced a machine-checked proof that the buggy version was insecure. The process took four weeks, on a job DeepMind says historically takes expert teams years. DeepMind is open-sourcing the artifacts.
Source: Google DeepMind, “Introducing AlphaProof Code,” November 10, 2026 — deepmind.google/blog/introducing-alphaproof-code
The case for it
The strongest case is that this attacks the right bottleneck. We have never lacked security properties worth proving. We lacked the man-hours. Proving production code by hand means a few expensive experts spending years on one system, so it happens for a handful of critical pieces and almost nothing else. If AI agents can do the bulk of the proving — the long, mechanical, checkable part — while humans keep the part that takes judgment, deciding what needs to be true, verification stops being a luxury and starts being something ordinary critical software could actually get.
The checkability is the other half. An agent’s proof here is not an opinion you have to trust. Every proof is checked by Lean. If it is wrong, the checker rejects it. And the target was well chosen: a flaw in a messaging protocol is everybody’s problem at once.
The case against it
The honest case against starts with the specification. A proof only proves what was specified. If the security goals were stated wrong, or a property was left out, the proof can be perfect and the conclusion still incomplete. DeepMind says experts reviewed every specification, which is the right process — but the trust has not disappeared. It has moved, from the code to the shorter list of statements about the code. That list is where a reader should spend their skepticism.
Scope is the second limit. This verifies Signal’s core cryptographic code and the properties specified. It does not prove the whole app on your phone is safe, or that a future version will not introduce a new flaw. Every change needs the work done again. A proof is a statement about one version, under stated assumptions — not a permanent clean bill of health.
Third, this is a research result from a frontier lab, not a tool I can download and run on my own projects this weekend. DeepMind released the artifacts, not a general product. The gap between “a top lab did this once” and “this is routine practice” is still real.
Where I land
I land firmly on the side that this matters — with the limits kept in plain view.
Most AI news is a model scoring a few points higher on a test. This is different in kind. AI agents did sustained, verifiable work — work whose output a machine can independently check — on code that protects real conversations, and the system proved it could tell good code from buggy code when deliberately handed the buggy kind. That is the pattern I want more of: AI doing the volume, humans doing the judgment, and a checker standing over both.
What I will watch next is boring on purpose. Does anyone outside DeepMind build on the released artifacts? Does the approach get applied to a second, unrelated system, by a smaller team? And does the cost come down far enough that verifying code in medical devices or grid software — examples DeepMind itself points to — becomes an expectation instead of a research event?
If that happens, November 10 will look like the week proving software stopped being something only the richest projects could afford.