Four weeks is a short clock for a cryptographic proof, and this one did not start at zero. Google DeepMind researchers say earlier formal verification by the Signal Foundation gave them a head start. The public account of the work is Lily Hay Newman’s November 10, 2026 report in WIRED, plus statements from DeepMind and from Signal. Brief it as a lab result, not as a control for a risk register. No audit of the proof by people who did not build the system has been published. DeepMind checking Signal is not the same thing as the outside world checking DeepMind.
What that account describes is narrower than a finished seal. Using AlphaProof Code, a new AI framework, DeepMind applied agentic AI to an unspecified subset of the Signal protocol’s key cryptographic guarantees. In the account DeepMind gives, AI agents contribute and self-correct, and humans still review at key points. Formal verification means writing those properties down and producing a machine-checked proof that they hold. A test suite only speaks to the cases you ran. A proof only speaks to the specification someone chose.
Newman’s report says that no new vulnerabilities turned up in the portions of the protocol examined. On older Signal versions that still contained known, long-fixed flaws, it says AlphaProof Code correctly identified those flaws and showed the protocol could not be formally verified. The flaws are not named. The report also does not say whether “identified” was a counterexample, a proof search that failed, or a specification that would not go through. A failed blessing and a located bug are different events. A tool that cannot bless code already known to be broken is at least behaving like a test, and this control is still DeepMind’s account of its own run.
Showing the work
Before this kind of AI automation, someone had to describe the desired behavior, turn it into formulas, and then build the proof. That last stretch is specialist work measured in months to years. WIRED credits agentic AI with shortening proof construction enough to make a four-week proof of concept feasible. The head start belongs in that sentence. The reporting does not split those four weeks between the new system and proofs already on the shelf. Anyone who wants to brief “AI did this in a month” should be asked for the split first.
Swarat Chaudhuri, a DeepMind research scientist, calls the workflow a human-AI collaboration process. The mandatory review points, and who owns the specification, were not described. He was clear about the failure mode.
We don’t want this sort of vibe world where AI is generating the goals and AI is generating the proofs and basically taking tests that are self-written. There’s a middle ground.
That middle ground is the governance point, even without the operating manual. An assurance process in which the same system writes the exam and the answer key is not assurance. If a vendor pitches this style of AI automation, ask who wrote the goals, which steps a human had to sign, and whether an outsider can inspect the math.
The scope fits in one description. The count of guarantees, their names, the mathematical language, and the version are not public. The reporting also does not say whether AlphaProof Code checked a mathematical model, a specified implementation, or a shipping binary. Ehren Kret, Signal’s chief technology officer, spoke of the protocol implementation, and framed the work as an expansion of older formal verification that covered smaller portions of the code.
While prior formal verification focused on smaller portions of the code, Google DeepMind’s approach enables significant expansion. As AI-driven security threats grow, rigorously verifying the Signal protocol implementation gives us even greater confidence in our code’s privacy guarantees.
That is a vendor statement about a research check, and a claim of greater confidence. The threats he mentions are not detailed. The entire Signal mobile app sat outside the work. Google Messages and WhatsApp were not the systems under test. WIRED names them, with the Signal app, because they rely on this cryptography. That reliance is a reason the protocol draws attention. It is a different claim from a check on their code.
A skeptic still cannot open the artifact that would settle the rest. No outside review of the proof has been published. Researchers are releasing the specification and proof so other formal-verification work can build on them, WIRED reports. The reporting does not show those files already available for an outsider to open, or that they are complete and peer-reviewed. Until that changes, the result remains a reported one.
No price, no product
Pushmeet Kohli, whom WIRED identifies as chief scientist at Google Cloud and DeepMind’s vice president of research, sketched the version executives like to hear.
If you can now verify the correctness of these implementations, then you can rest easy. You can imagine banks, imagine all those other companies who rely on assurances and who worry about bugs who could now say, ‘I can prove these properties.’
Imagine is the operative verb. No bank or other customer deployment has been reported. “Rest easy” is a mood, not a control. Firms that live on assurances may someday want proofs of this kind. A want is not a standard, a customer, or a contract.
DeepMind ran the analysis free of charge, as research. Google declined to share the cost. Google also declined to comment on whether it plans to sell formal verification as a product or service. Leaders weighing AI for business can brief the method. They cannot yet price an engagement, or put a product on a shortlist.
Chaudhuri was more careful about how far the method reaches.
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.
This proof of concept did not show what coverage would cost on the codebases a company already runs. Whether AI-aided formal verification can reach large amounts of code at a price anyone will keep paying is still an open question, in this project and across the sector. A wish to verify all the software of the world is a direction. It is not a coverage estimate.
Questions worth asking
-
Did this prove Signal, WhatsApp, or Google Messages are secure?
No. It was a four-week proof of concept on an unspecified subset of key cryptographic guarantees. The count is not public, the entire Signal mobile app was outside the work, and WhatsApp and Google Messages were not the systems checked.
-
Did the tool find new vulnerabilities?
WIRED reported that DeepMind found none in the portions examined. That is DeepMind’s account, via WIRED, not an outside finding.
-
How do we know it can catch real bugs?
WIRED reported that on older Signal versions with known, long-fixed flaws, AlphaProof Code correctly identified those flaws and showed the protocol could not be formally verified. The flaws are unnamed, the meaning of “identified” is unexplained, and the control remains DeepMind’s account of its own test.
-
Has anyone outside the project checked the proof?
No such audit has been published. DeepMind checking Signal is not the same thing as the outside world checking DeepMind.
-
Who wrote the goals, and what stops the system from grading its own exam?
The operating rules were not described. Chaudhuri argues for a human-AI collaboration and against a setup where AI writes both the goals and the proofs, but the reporting does not say who owned the specification or which reviews were mandatory.
-
How much was new AI, and how much was earlier human proof?
Researchers say Signal Foundation verification gave them a head start, and Kret says that earlier work covered smaller portions of the code. The split is not quantified.
-
Can a company buy this, and what would it cost?
Not on the current record. The run was free research. Google declined to disclose the cost and declined to comment on a commercial product or service.
-
Will this scale to the software a business actually depends on?
This proof of concept did not show cost or coverage for production systems. Chaudhuri said there is a long distance to all the software of the world, which is a stretch goal rather than a timeline for one codebase, and workable cost at large scale remains open.
Partial scope, an unpublished price, and DeepMind’s own account of catching flaws humans had already fixed: that is the size of the result. Brief it as a lab result, not as a control you can put in a budget.