Signal Protocol Verification: Google DeepMind Uses AI

LONDON, November 11, 2026 — The Signal protocol verification project, called AlphaProof Code, used a team of artificial-intelligence agents and formal theorem proving to check selected security properties in the cryptographic code underlying the messaging system. Google DeepMind says the work was completed in four weeks and is a test of whether AI can help verify software that protects private communications beyond conventional bug scanning.

The result is narrower than a claim that Signal or every application using its protocol is now proven secure. DeepMind says the work examined particular protections in the compiled implementation, with human specialists defining the properties to be checked and reviewing the output. It did not establish that every part of the Signal app, the devices on which it runs or the wider systems around it are free from vulnerabilities.

Formal verification is a method of using mathematical logic to show that a computer program satisfies a clearly defined set of properties. In the Signal project, DeepMind says its researchers worked with the messaging service’s security team to translate important protocol protections into formal specifications. AI agents then helped produce proofs that the implementation met those specifications, while the Lean proof assistant checked the resulting proof objects.

The distinction between the protocol’s design and the code that implements it is important. A cryptographic protocol can be described in a paper or mathematical model, but software engineers still have to translate that design into code that runs on real devices. Errors can enter during that process. A proof about a design does not automatically prove that a particular implementation follows the design correctly.

DeepMind says AlphaProof Code was used to examine the compiled code associated with Signal’s core cryptographic protections. The properties included safeguards for messages when a device is operating normally and protections intended to limit the consequences if a device is temporarily compromised. The company described the work as an examination of key security guarantees in a widely deployed protocol, rather than a general audit of every component in the messaging service.

The Signal Protocol is used in Signal and in other messaging products, including end-to-end encrypted conversations in Google Messages. Its security matters because users rely on the protocol to prevent people outside a conversation from reading message content. A flaw in the implementation of a widely used cryptographic system could affect many more people than a bug confined to a single application.

DeepMind describes AlphaProof Code as a multi-agent system powered by its Gemini 4 Carbon model. Human experts first specified the security properties and the conditions under which they should hold. The agents then worked through the implementation, generated formal proof steps and tried to establish that the code satisfied the stated requirements. Lean checked the proofs mechanically, providing a separate verification step rather than relying on the language model’s own assertion that it had succeeded.

That division of labour is central to the approach. A language model can propose a proof, but the proof assistant checks whether the mathematical steps follow from the assumptions and definitions. If the model produces an invalid argument, the checker rejects it. The system can therefore use AI to search for a proof while relying on a deterministic tool to validate the result.

DeepMind said the project generated millions of lines of Lean proof material and that the work was completed in four weeks. The company’s technical account refers to more than six million lines, while Axios described the effort as producing more than three million lines of mathematical proof code. The public descriptions do not explain whether the figures count different stages or categories of output, so they should not be combined into a single total.

The company also said that a small portion of the codebase, about one per cent, was flagged for additional human review. That detail matters because the project was not described as an entirely unattended process. Specialists remained responsible for deciding what should be proved, examining the parts that needed closer attention and checking whether the formal statements reflected the intended security properties.

DeepMind compared the four-week effort with the much longer period that a team of experts might otherwise need to complete comparable formalisation work. That is the company’s estimate, not an independently measured benchmark across several engineering teams. The project does show that AI agents can help with a demanding verification task, but the time and cost savings will need to be tested on other codebases before the approach can be treated as a general productivity measure.

The team also tested the system by reintroducing two bugs that had previously been fixed in the code. In the isolated test version, AlphaProof Code produced proofs showing that the altered implementation no longer satisfied the required security properties. DeepMind presented this as evidence that the process could identify known failures when they were deliberately restored. It was not an announcement that the project had discovered two new exploitable vulnerabilities in the live Signal service.

Most software testing checks whether a program behaves as expected in selected situations. Security scanners search for known patterns, suspicious code or weaknesses that have been observed before. These methods are essential, but they cannot examine every possible combination of inputs and system states. Formal verification takes a different route: it attempts to prove that a stated property holds for all cases covered by the mathematical model.

For a messaging protocol, that can mean proving that a particular class of messages remains protected under defined conditions, or that a security guarantee continues to hold when an attacker gains temporary control of a device. Such properties are difficult to establish through ordinary testing alone because the number of possible interactions can be extremely large.

Formal verification is not a substitute for good specifications. A proof can show that code satisfies the property written by the researchers, but it cannot guarantee that the property captures every real-world threat. If the specification omits a relevant attack path, the software may pass the formal check while remaining exposed to a problem outside the model. The quality of the human-defined assumptions is therefore as important as the ability of the AI system to generate proofs.

The scope of the Signal project also needs to be kept in view. Verifying selected cryptographic code does not automatically cover the application’s interface, operating-system security, device storage, account recovery, contact discovery, server infrastructure, software updates or the physical security of a user’s phone. Nor does it establish that every product using the Signal Protocol implements the same protections in the same way.

That is why the result should be read as a significant verification exercise, not a certificate that an entire messaging ecosystem is invulnerable. The project addresses a difficult part of the security problem: whether a specific implementation preserves important mathematical guarantees. Other audits, testing, secure development practices and independent review remain necessary.

Signal’s technology leadership has welcomed the work as a way to increase confidence in the protocol’s implementation. That endorsement is relevant because the project was carried out in collaboration with the organisation responsible for the messaging service. It is not, however, an independent certification of every aspect of the product, and users should not interpret it as a promise that future vulnerabilities are impossible.

The potential application goes beyond encrypted messaging. Software used in banking, medical devices, industrial control systems, power networks and government services can have consequences that are difficult to reverse when it fails. Formal verification has been used in high-assurance systems for years, but the work is specialised and expensive. AI agents could make parts of the process more accessible by helping engineers translate requirements into formal statements and search for proofs.

That possibility is especially relevant as software becomes more complex and AI-generated code enters production systems. Developers are increasingly using coding assistants to write functions, test applications and automate maintenance. If the same generation of tools can help verify critical properties, the industry could move from relying mainly on tests and human review towards a more systematic method of checking whether important guarantees hold.

The risks are also clear. An AI agent that generates code quickly can introduce errors at a speed that overwhelms manual review. A verification agent may help catch some of those failures, but only if its specifications are accurate, its tools are correctly configured and the proof process is independently checked. Organisations should not assume that attaching a theorem prover to a coding model makes every output safe for deployment.

There are practical questions about cost, repeatability and access. The Signal project involved human security specialists and a substantial amount of generated proof material. DeepMind has not established that the same process can be applied cheaply to every large software project, nor that it can replace the work of cryptographers and formal-methods engineers. Independent teams will need to reproduce the results and test the method on systems with different architectures and threat models.

The company has not presented AlphaProof Code as a finished consumer product. The announcement is a research and engineering result, and the next test will be whether the approach can be repeated outside a collaboration involving the model developer and the protocol’s own security team. Open technical material and independent scrutiny will help determine how much of the reported progress can be reproduced by other researchers.

For users, the immediate implication is limited but meaningful: a widely used cryptographic implementation has undergone a new form of mathematical checking, and its developers say selected protections were verified. There is no indication in the announcement that Signal users need to change settings or take emergency action. The work does not disclose a new breach or a newly discovered live vulnerability.

The broader significance will depend on what happens next. If AI-assisted formal verification can be independently repeated, it could become one layer in the security process for systems where a coding mistake can expose private communications, disrupt essential services or put people at risk. If the results remain tied to a narrow set of specifications and unusually intensive human oversight, the method will still be useful, but its reach will be more limited than the headline claims might suggest.