DeepMind Uses AI to Check Encryption Protections in Signal Code

Google DeepMind has used artificial intelligence to produce mathematical proofs of selected security protections in libsignal, a software library that encrypts and decrypts Signal-protocol messages and manages their encryption keys. Announced on November 10, AlphaProof Code checks a particular compiled version of that library under stated assumptions. The researchers report a four-week campaign, with humans deciding which protections the work should establish. 1

Consider a message sent while its recipient is offline. The sender encrypts it, and a server holds the encrypted message until it can be delivered. The library helps the two people establish shared secrets and derives changing keys for their messages. It also handles messages arriving out of order. Errors in that bookkeeping can undermine an otherwise sound encryption design. The project examines whether specified protections hold through those implementation details. 2,4

A compiler translates the source code developers write into instructions a processor executes. DeepMind studied those compiled instructions for libsignal version 0.105.4, built for Linux on AArch64, an Arm processor architecture. The team put the library inside a small command-line program that exchanges messages and stores data in files. This created a defined target for the proof: the executable's behavior in a mathematical model of that computer environment. 2,3

Before proving anything, the researchers had to define what secure behavior meant. A secrecy claim, for example, needs to say which keys an attacker may steal, when the theft happens and which messages remain protected. These definitions and claims form a formal specification. Humans worked with AI to draft and review it. As Swarat Chaudhuri and colleagues write in the paper, “human authors select what to prove.” A precise but weak statement would give a correspondingly weak guarantee. 1,2

Other AI agents then wrote proofs in Lean, a language for expressing mathematics so software can check the argument. Lean's small checking core verifies that each logical step follows the rules. A separate comparison checks that the final claim and its definitions match the approved specification. Together, these checks help prevent an agent from submitting a plausible-looking argument or silently weakening the problem. The final evidence covers every case allowed by that mathematical statement and its assumptions. 1,3

The team also restored two previously fixed libsignal bugs in isolated versions of the program. The agents produced checked proofs showing that each altered version violated a specified security property. These are concrete examples of errors the claims can catch. DeepMind reports more than six million lines of generated Lean proof code: the written mathematical arguments supporting the checks. The company has released the specifications and proofs for outside examination. 1,3

The researchers used two ways of describing an attacker. One treats cryptographic operations as abstract building blocks with specified properties. The other bounds the advantage an attacker using conventional computers could gain, under restrictions on the modeled messages and sessions. The abstract argument also covers specified protections in the initial key exchange against modeled quantum attacks. Recovery of ongoing messaging after a compromise by a quantum-capable attacker remains outside the proved results. 2

Both arguments depend on assumptions about the cryptography, selected software routines and how the computer runs the program. Lean and the specifications themselves also need to be trustworthy. The result concerns the chosen executable and claims; group messaging and Signal's complete applications remain outside this project. Reviewers can inspect the public files and repeat the documented checks. Keeping that evidence current would require checking relevant changes to the code, compiled instructions or security claims as the software develops. 2,3

Sources

1. Google DeepMind announcement by Pushmeet Kohli and Swarat Chaudhuri, November 10, 2026

2. Chaudhuri and colleagues, AlphaProof Code technical paper; specification writing, build target, security models, limitations and trusted assumptions

3. Google DeepMind public repository, including compiled target, comparator and proof-checking instructions

4. Signal protocol specification, especially changing message keys and handling messages arriving out of order