DeepMind Tests AI-Driven Formal Verification on Signal's Cryptography

A Milestone in Two Directions

Google DeepMind has completed a mathematical proof of several core cryptographic guarantees in the Signal protocol, using a new AI framework to accelerate work that would traditionally take months or years. The project, carried out over four weeks, serves dual purposes: it offers independent validation of encryption mechanisms protecting billions of messages across Signal, WhatsApp, and Google Messages, and it demonstrates the potential of AlphaProof Code, DeepMind's formal verification tool.

The team uncovered no new vulnerabilities in the current Signal protocol. When researchers applied the same framework to older versions containing known, patched flaws, AlphaProof Code correctly identified them and showed those versions could not pass formal verification. DeepMind is releasing the specification and proof to support further work in the field.

Why Formal Verification Matters

Formal verification uses mathematical logic to confirm that software behaves exactly as intended, rather than relying on testing alone. For cryptographic systems, this means proving that a protocol's security properties hold under all conditions, not just the scenarios covered by quality assurance.

The approach has been described as a gold standard in software security, but its adoption has been constrained by cost. Writing specifications, translating them into formal logic, and constructing proofs manually can consume thousands of hours per project. Agentic AI systems, which can reason through multi-step problems and generate code, now promise to compress that timeline.

DeepMind's Signal analysis illustrates the shift. The team formalised the protocol's cryptographic guarantees and produced machine-checked proofs in weeks, a process that would have required a small team of specialists working for far longer using traditional methods.

Scope and Limits

The analysis focused on key parts of the Signal protocol, the cryptographic layer that underpins end-to-end encryption in multiple messaging platforms. It did not extend to the Signal mobile application itself, which includes thousands of lines of code for user interface, storage, networking, and other functions beyond the core protocol.

Swarat Chaudhuri, a research scientist at DeepMind, emphasised that the result is one step in a longer journey. "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," Chaudhuri said.

The project's limited scope reflects a broader challenge in formal verification. Even with AI assistance, the method works best on well-defined, modular components such as cryptographic protocols or individual algorithms. Verifying large, interconnected software systems remains impractical for most organisations.

How AlphaProof Code Fits In

AlphaProof Code is DeepMind's latest framework for automated theorem proving. It builds on earlier work in mathematical reasoning, adapting those techniques to software verification. The system takes a specification describing what a piece of code should do, then attempts to construct a formal proof that the implementation meets that specification.

In the Signal project, AlphaProof Code worked from a detailed description of the protocol's security properties, including forward secrecy and authentication. It generated proofs in Lean, a proof assistant used by mathematicians and computer scientists to check logical arguments. The proofs are machine-verifiable, meaning they can be independently confirmed by other tools.

The framework's ability to identify known vulnerabilities in older Signal versions adds credibility to its findings. When a protocol cannot be verified, the system provides feedback that can help developers locate the problem, turning formal verification into a diagnostic tool as well as a validation mechanism.

AI-Aided Verification's Wider Moment

DeepMind's work arrives during a surge of interest in AI-assisted formal verification. Researchers at institutions including Carnegie Mellon, MIT, and the University of California, Berkeley, have published results showing that large language models can accelerate proof construction, sometimes by an order of magnitude.

Yet practical adoption remains uneven. Formal verification is most common in safety-critical industries such as aerospace, medical devices, and automotive systems, where regulatory pressure justifies the cost. In commercial software development, where release cycles are measured in weeks and codebases change constantly, the technique has struggled to gain traction.

AI could change that calculus if it can reduce the expertise required to write specifications and construct proofs. But the technology is not yet mature enough to handle the full complexity of modern applications, which integrate third-party libraries, cloud services, and user-generated content in ways that resist formal modelling.

What This Means for Signal

For Signal, the DeepMind analysis provides another layer of assurance. The protocol has already been audited multiple times by independent security firms, and its design has been peer-reviewed in academic literature. Formal verification adds mathematical certainty to those assessments, particularly for the core cryptographic operations that determine whether messages remain confidential.

The protocol is used not only by Signal's own app but also by WhatsApp, which has more than two billion users, and by Google Messages, the default SMS application on many Android devices. Any vulnerability in the protocol would have global consequences, making independent verification valuable even when no new flaws are found.

DeepMind's decision to release the specification and proof also benefits the wider cryptographic community. Other researchers can build on this work, extending formal verification to additional parts of the protocol or adapting the methods to different systems.

Open Questions

The Signal project was designed as a proof of concept, not a comprehensive security audit. The scope was deliberately narrow, focusing on the protocol's abstract design rather than its implementation in any particular programming language or platform. Real-world bugs often arise from implementation details, memory management, or interactions with operating systems, none of which were covered here.

It also remains unclear how much domain expertise is still required to use tools like AlphaProof Code effectively. Writing a specification that accurately captures a protocol's security properties is a skilled task, requiring deep knowledge of both cryptography and formal methods. If AI verification tools still depend on expert-written specifications, the bottleneck may have shifted rather than disappeared.

Finally, there is the question of trust. Formal verification produces a proof that software behaves correctly, but that proof is only as reliable as the specification it is based on. If the specification omits a critical security property, or defines it incorrectly, the proof will not catch the error. Human judgement remains essential, even when the proof itself is automated.

A Step, Not a Solution

DeepMind's Signal analysis demonstrates that AI can accelerate formal verification for well-defined cryptographic protocols. The four-week timeline and the ability to detect known vulnerabilities in older versions both suggest that the technology is maturing. But the project's limited scope also highlights the distance between verifying a single protocol and securing entire software ecosystems.

For organisations considering formal verification, the lesson is that AI can make the technique more accessible, but it does not eliminate the need for expertise or careful scoping. The method works best on components where correctness is critical and the specification can be written clearly, such as cryptographic primitives, consensus algorithms, or safety-critical controllers.

DeepMind has released its Signal specification and proofs under an open licence, inviting further research. Whether AI-driven formal verification becomes a standard practice in software engineering, or remains a specialised tool for high-stakes systems, will depend on how quickly the technology can scale beyond proof-of-concept projects like this one.