Google DeepMind Uses AI to Verify Signal’s Security Code, but Bigger Promise Is Still Ahead

Google DeepMind says it used artificial intelligence to formally verify key security properties in the Signal protocol in a four-week proof-of-concept, finding no new vulnerabilities in the portions it examined. The work matters because it suggests AI may help make one of software security’s slowest, most exacting tasks practical enough to use on the messaging systems people rely on every day.

What DeepMind did

According to WIRED’s reporting, DeepMind applied agentic AI and its formal verification tools, including AlphaProof Code, to examine key cryptographic guarantees in the protocol behind Signal. The project was not a full audit of the app itself, but a focused proof-of-concept aimed at showing that AI can help mathematically validate important security properties in real-world software.

That distinction matters. Formal verification is not the same as conventional testing or code review. It uses mathematics to prove that software meets specified properties, which can be especially important in systems handling sensitive communications and cryptographic functions. In this case, the analysis served as an outside validation of the cryptography used by Signal, Google Messages, and WhatsApp, all of which rely on the underlying protocol in some form.

How the project worked

DeepMind completed the proof-of-concept in about four weeks, according to WIRED. The company framed the effort as a milestone rather than a finish line, saying the work does not amount to full verification of all software, and researchers emphasized that humans were still essential to the process. The AI could self-correct in parts of the workflow, but people reviewed the important steps.

That human-AI mix is central to the result. DeepMind researcher Swarat Chaudhuri said the team does not want a system where AI generates the goals and the proofs without meaningful oversight. The point, as the researchers described it, is to use AI to speed up a deeply technical process while keeping formal reasoning under human control.

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

— Swarat Chaudhuri, DeepMind research scientist

Why it matters

The practical significance is bigger than a single messaging app. If AI can reduce the cost and time required for formal verification, companies could use a much stronger security method on far more software than they do today. That could matter for messaging platforms, cloud services, financial systems, safety-critical products, and any codebase where an undetected flaw can expose data or undermine trust.

For users, the appeal is straightforward: stronger confidence that the underlying code does what it is supposed to do. For the security industry, the implication is more disruptive. Formal verification has long been seen as powerful but too slow and resource-intensive for broad deployment. DeepMind’s result does not erase those limits, but it hints that AI may help narrow them.

There is also a competitive and strategic angle. Google did the work as a free research project, and it would not disclose the cost. That leaves open whether the company sees this as the seed of a commercial product or as a research capability meant to bolster its broader security and cloud story. Google also would not say whether it plans to offer a formal verification product.

How formal verification fits into software security

Formal verification has a reputation for being precise, expensive, and difficult to scale. Instead of trying to find bugs by running software under many conditions, it seeks mathematical proof that the code satisfies a set of rules. That makes it attractive for cryptographic systems, where even a narrow defect can have outsized consequences.

Signal is a particularly meaningful test case because it is widely associated with privacy and end-to-end encrypted messaging. The fact that the protocol is also used in parts of Google Messages and WhatsApp helps explain why this work drew attention beyond one app. A verified protocol can offer reassurance not just for a single product, but for a family of products built on related cryptographic foundations.

DeepMind also said it is releasing the specification and proof from the Signal work so others can use it. That could help researchers compare methods, reproduce the analysis, and adapt pieces of the workflow for other systems. The real question is how reusable the materials will be outside this narrow case.

What the analysis found — and what it did not

DeepMind reported no new vulnerabilities in the protocol portions it examined. That is the cleanest takeaway from the project, but it should not be overstated. Researchers said they did not formally verify the full Signal mobile app, only the protocol elements under study.

The limitations are important because security tools can produce false confidence if readers confuse narrow proof with broad assurance. DeepMind’s own framing pushes against that risk. The company said the result is one milestone, not a complete route to verifying all software.

The work did, however, uncover a useful contrast with older software. On older Signal versions that already had known, fixed flaws, AlphaProof Code identified the vulnerabilities and showed the protocol could not be formally verified in those cases. That detail suggests the tool was not merely rubber-stamping the code; it could distinguish between verified and broken implementations.

Background: how we got here

Signal Foundation has already done prior formal verification work on smaller portions of the system, and that history appears to have helped speed DeepMind’s project. Signal CTO Ehren Kret said the earlier work contributed to the pace of the analysis, which is a reminder that AI was not starting from zero. It was building on an existing body of cryptographic care and documentation.

That context matters because the achievement is not only about model capability. It is also about the quality of the underlying specifications, the discipline of the software community, and the way prior human work can be folded into AI-assisted analysis. In that sense, the project is as much a collaboration with established security practice as it is a demonstration of machine reasoning.

Formal verification itself is not new. What is new here is the attempt to make it faster and more approachable with AI tools. Before those tools, the work was often slow and labor-intensive, which limited how widely teams could use it. DeepMind’s proof-of-concept is an early answer to the question of whether that bottleneck can be reduced.

By the numbers

What Signal and Google said

Signal welcomed the added scrutiny, with CTO Ehren Kret describing the work as a confidence boost for the app’s privacy guarantees. His comment reflects why security-minded companies often value outside validation: even when the code is believed to be sound, independent confirmation can strengthen trust.

DeepMind’s Pushmeet Kohli, Google Cloud chief scientist and DeepMind vice president of research, presented the result as a practical way to reduce uncertainty in code correctness. The emphasis from both companies was not on hype but on confidence, verification, and the possibility of making a rigorous method easier to deploy.

As AI-driven security threats grow, rigorously verifying the Signal protocol implementation gives us even greater confidence in our code’s privacy guarantees.

— Ehren Kret, Signal chief technology officer

What the result says about AI and security

The DeepMind project lands at a moment when AI is increasingly relevant to both offense and defense in cybersecurity. That makes the result especially timely. If AI can help verify code, it could also become a more important tool for defenders trying to stay ahead of faster, more sophisticated threats.

Still, the research does not settle the hardest questions. The central open issue is whether AI-assisted formal verification can scale across large codebases at a cost that makes sense. The answer will determine whether this remains an impressive demonstration or becomes a routine part of secure software development.

There is also the question of human oversight. DeepMind’s researchers were clear that AI should not be left to define the task and prove the result without review. That caution may prove essential if the technique is expanded beyond carefully selected protocols into messy, legacy-heavy codebases that were never written with formal proofs in mind.

What happens next

The immediate next step is less about a product launch than about reuse. DeepMind said it will release the specification and proof from the Signal work, which could let other researchers inspect the methods and test whether they transfer to similar systems.

Beyond that, the questions are straightforward but unresolved:

• Can the method scale to entire applications rather than protocol fragments?
• How much human review will still be necessary for trustworthy results?
• Can the process be made affordable enough for routine use?
• Will Google turn the research into a commercial formal verification offering?

Google would not say whether it plans such a product, and it would not disclose the cost of the research. That means the market impact remains uncertain even as the technical signal, pun intended, is clear: AI has now been shown to help verify important cryptographic software properties in a real system, at least in a narrow and well-defined setting.

The larger takeaway

The most important thing about this project is not that AI found a bug or announced a breakthrough. It is that AI helped verify the absence of new vulnerabilities in a protocol where correctness really matters. That is a subtler but potentially more valuable achievement.

If the approach matures, it could change how developers think about secure software. Instead of using formal verification only on the smallest, most critical components, they may begin to apply it more broadly. For now, DeepMind has shown a credible path toward that future — and also how far there still is to go.