Google DeepMind says its AI agents proved Signal's encryption code secure in four weeks
The proofs cover the code that runs, not just the design, and a computer checks them. Signal's apps and group chats are not covered.
Signal is a messaging app whose encryption design many other apps copy. On 10 November 2026 Google DeepMind said its AI agents had written computer-checked proofs that the code behind that encryption does what it promises. The proofs are in Lean, a language in which a computer checks every step.
The system, AlphaProof Code, worked on libsignal (Signal’s encryption library, version 0.105.4) after it was compiled into machine code, so the proofs concern the instructions a processor runs and not only the design. They cover setting up a conversation, sending and receiving. The properties include that messages stay protected before and after a device is briefly compromised.
The paper counts about 6.5 million lines of proof, resting on about 26,000 lines of trusted definitions. For scale, the paper puts an AI-built Lean proof of Fermat’s Last Theorem at about 13 million lines. A team of five did the work in four weeks; the blog post says such jobs have taken expert teams years. Each proof team had 40 to 80 agents powered by Gemini 4 Carbon and ran for 24 to 72 hours on one machine.
As a test, the researchers put two old, already fixed libsignal bugs back in. Both times the agents proved the faulty version insecure. Neither the post nor the paper reports a new bug in Signal’s code.
What it means
Proving that real security software is correct has been slow, specialist work, so it is rarely done for code people use. Here AI agents did most of it in weeks, and a computer checks the result. People still have to decide what “secure” means: the proofs only show the code meets the definitions humans approved.
Caveats
- Self-reported by Google DeepMind. We found no independent review yet; Signal staff gave feedback on the definitions and Signal’s technology chief is quoted in the post.
- The proofs cover a command-line build of libsignal for one processor type, not Signal’s own apps, and the paper says carrying them over takes extra trust.
- Out of scope, per the paper: group messaging, more than two parties, several devices per person, and side channels (leaks through timing or memory).
- Everything rests on the trusted definitions and a model of the processor, written with AI help and reviewed by people. A mistake there would not be caught.
- The proof with numerical security bounds covers only classical attackers, not quantum computers.