Signal: what AI has really proved about its code

Google DeepMind says it used AlphaProof Code to prove certain properties of Signal’s compiled code. The result sheds light on AI’s potential, but also on the precise limits of formal proof.

To assess whether software encrypts messages correctly, it is not enough to run tests and observe its behaviour in a few situations. It must also be possible to establish, through verifiable reasoning, that certain properties hold in every execution covered by the model. Google DeepMind says it used its AlphaProof Code system to do this with compiled code from the Signal protocol, using AI agents and the Lean proof checker.

The experiment concerns specific cryptographic guarantees, not the absolute security of the Signal app. Above all, it shows how AI can contribute to demanding formal verification, while leaving important choices to researchers and entrusting the final mathematical check to specialised software.

From the cryptographic model to the code being run

An encryption protocol sets out the rules that make it possible, for example, to protect an exchange and authenticate the participants. But a sound design is not enough: the programme that implements it may contain an error. Formal verification seeks to establish mathematically that code complies with properties defined in advance, under assumptions that are also explicit.

DeepMind says it worked on compiled code from libsignal, the library that implements the Signal protocol. This step matters: the team did not stop at a theoretical description of the protocol, but sought to link security guarantees to the code produced after compilation.

The system, named AlphaProof Code, divides the work among several models and agents. According to Google DeepMind’s published account, researchers first translated the security objectives into mathematical specifications, then agents powered by Gemini built formal proofs. DeepMind’s blog post mentions more than six million lines produced in the Lean language. This does not mean that the AI wrote six million lines of software: these are artefacts used to formalise and check the demonstrations.

What Lean checks, and what researchers decide

Lean is a proof assistant. It checks that a proof follows the system’s logical rules and establishes the stated result. On its own, it does not decide whether the chosen properties meet all a user’s expectations, or whether the starting assumptions accurately describe the real world.

This distinction is central. According to DeepMind, experts helped define what had to be proved and reviewed the specifications. The agents then explored possible proofs, while Lean checked their formal validity. The system can therefore reduce some of the work involved in finding a proof, but the scope of the proof remains a human choice.

A formal proof is therefore not a universal audit. If a property is not included in the specifications, the proof does not cover it. If a cryptographic function is assumed to be secure without its implementation being verified, that assumption remains a link outside the result. The correct conclusion is conditional: the code satisfies the formalised properties, within the defined scope and under the assumptions adopted.

Four weeks, two bugs reintroduced

DeepMind says the experiment lasted four weeks. To test whether the method could distinguish compliant code from a faulty version, the team also reintroduced two known bugs, previously fixed, into an isolated version of the code. The company says the system then produced machine-checked proofs showing that these variants no longer met the guarantees under examination.

This test is useful because it puts the method up against concrete errors, rather than measuring only its ability to produce a proof for a correct version. But it does not establish a generalisable detection rate: two reintroduced defects represent neither all categories of vulnerability, nor all software, nor all the ways a system could fail.

The scope of the proof remains precise

The guarantees examined concern the cryptographic core and individual exchanges. The scope described leaves out the application as a whole, group conversations and use across multiple devices. Nor do they amount to verification of WhatsApp or Google Messages, even though these services use elements of the Signal protocol. A shared library or protocol does not make the applications that incorporate it, their versions and their configurations identical.

Nor does verification mean that no unknown vulnerabilities remain. It reduces uncertainty about defined properties and the code included in the analysis. Other components, interfaces, operating systems, key management or functions left outside the scope may raise separate questions.

For users, the immediate benefit is therefore less a new setting than a method of checking that could make certain guarantees harder to dispute or inadvertently breach. For teams designing critical software, the question is whether agents can reduce the human cost of proofs that have until now required substantial specialist work. DeepMind points to possible applications in other software, but the ability to extend this approach to larger systems remains to be demonstrated.

The specifications and proofs published by DeepMind give other specialists the means to examine and reproduce the work. It is this possibility of scrutiny, combined with a clearly defined scope, that makes it possible to assess AI’s contribution: not a general certification of ‘security’, but help in establishing certain properties of the code, with humans choosing what matters and a formal checker checking the proof.