Google DeepMind said on Nov. 10 that its researchers guided AI agents, which can carry out tasks on their own instead of only answering questions, to prove that the code behind the Signal protocol keeps several of its main security promises. The protocol is the encryption that keeps chats private in the Signal app, and versions of it protect messages in WhatsApp, Meta's Messenger and Google Messages. The work covers Signal's own code, not the versions those other apps run. The result is a formal proof, one written in a special programming language, here Lean, so that a computer can check every step. DeepMind says it is the first time the unchanged code of a widely used encryption system like Signal's has been proven to keep its security promises, by any method. Earlier checks, the paper says, covered the design on paper, rewritten or altered copies of the code, or narrower properties such as not crashing. Signal's chief technology officer, Ehren Kret, says earlier work focused on smaller parts of the code.
The gap between design and code is where real security holes often hide, DeepMind says. Experts have spent decades checking encryption designs with math. But a program can still make mistakes its design never made. So the researchers left libsignal, Signal's own code library, untouched, turned it into the instructions a processor runs with a standard tool, and proved the security promises for those instructions.
The work was split between people and AI. Researchers worked with AI models to write down exactly what the code must guarantee, and DeepMind says human experts reviewed every one of those statements. Then a team of AI agents running on Gemini 4 Carbon, Google's AI model, wrote all of the proofs, about 6.5 million lines of Lean. Lean's checker accepted each proof only if every step held. DeepMind says the agents flagged about 1% of the code for a person to check. To test the method, the researchers put two old, already fixed Signal bugs back into a copy of the code, and the system proved that each buggy version was not secure. The proof work took a team of five four weeks, a job DeepMind says used to take expert teams years, though the researchers say earlier proof work by Signal gave them a head start, according to a news report.
The proofs cover promises Signal makes to its users. Only the people in a chat can read it. Old messages stay safe even if a key is stolen later. Messages become safe again after a phone or computer has been briefly broken into, as long as the attacker doesn't tamper with the next exchange of keys. Messages really come from the person they claim to come from. And the opening exchange of keys stays secret even from a future attacker with a quantum computer. That promise is proven only under a simpler test, which lets the attacker break the older, non-quantum-safe part of the key exchange but treats the code's other scrambling and signing tools as perfect. The other promises were proven against attackers using today's computers. Kret said in a statement DeepMind published that the work "gives us even greater confidence in our code's privacy guarantees."
The proofs have limits. A computer check shows the code meets the security goals as the researchers wrote them down, not that those goals capture every way an attack could work. The proofs cover chats between two people, and the researchers leave group chats for later work. They assume the standard math building blocks the protocol relies on are themselves secure, and they rely on Lean's checker, on the researchers' model of how the processor behaves, and on assumed behavior for some small routines the code calls. Neither proof covers people who use Signal on several devices, and the proof that measures an attacker's odds stops meaning anything over very long conversations. The proofs also assume each person already holds the other's genuine identity key, the code Signal uses to recognize a contact, so they don't cover someone posing as a contact the first time two people connect. Attacks that spy on a device's timing, power use or memory are also outside the proofs. The researchers proved things about the code library, run through a small test program, not the whole Signal app. A news report says the work found no new flaws in the parts it examined.
DeepMind has released its specifications and proofs for others to use, and says the work lays the groundwork for securing software such as medical device firmware and power grid software. According to a news report, Google declined to give the cost of the Signal work or say whether it plans to sell the method as a product.