--- title: "An AI Just Did the Math Homework on Signal’s Encryption" description: "Google DeepMind formally verified chunks of the Signal protocol in four weeks, a job that used to take humans forever" author: "Nate Ledger" published: 2026-11-11T14:08:57Z modified: 2026-11-11T22:18:04Z url: https://rews.cc/a/an-ai-just-did-the-math-homework-on-signal-s-encryption-4091ff language: en tags: ["ai", "security", "openai", "signal", "deepmind", "tech"] publisher: "Rews (https://rews.cc)" --- # An AI Just Did the Math Homework on Signal’s Encryption *Google DeepMind formally verified chunks of the Signal protocol in four weeks, a job that used to take humans forever* By Nate Ledger · November 11, 2026 · https://rews.cc/a/an-ai-just-did-the-math-homework-on-signal-s-encryption-4091ff ## In brief - Google DeepMind’s AlphaProof Code formally verified key cryptographic guarantees of the Signal protocol in a four-week project - The work independently validates encryption used by Signal, Google Messages and WhatsApp, and found no new vulnerabilities - The analysis was limited in scope and did not cover the entire Signal mobile app - The system correctly flagged known, long-fixed vulnerabilities when run on older Signal versions - DeepMind is releasing the specification and proof to support future formal verification work Here is a fun thing about the encryption that protects a huge share of the world’s messages: everybody trusts it, and mostly for good reasons, but “everybody trusts it” is not the same thing as “somebody has proved it.” Cryptographers have poked at the Signal protocol for years, and it holds up, and that collective confidence is worth a lot. Still, the gold standard in software assurance is formal verification, where you do not merely test the code or stare at it very hard, but actually write down a mathematical specification of what the software is supposed to do and then prove, with math, that it does it. [WIRED’s Lily Hay Newman reports](https://arstechnica.com/ai/2026/11/signals-encryption-just-passed-an-ai-powered-mathematical-checkup/) that Google DeepMind has now done exactly that for key parts of Signal — and the interesting part is not the proof, but who did the proving, or rather what. What did it was an AI framework called AlphaProof Code. DeepMind researchers used agentic AI to formally verify a number of the Signal protocol’s key cryptographic guarantees, in a proof-of-concept project that took four weeks. Four weeks is the whole story here, so let me explain why. Before the AI era, formal verification was brutal work: a human had to describe the properties of the software worth proving, translate those descriptions into formal formulas, and then grind out the proof itself. People in the field have long called verification a holy grail of software security precisely because it was so slow and expensive that almost nobody ever got to drink from it. Agentic AI attacks the back half of that problem — the formula-writing and proof-grinding — and compresses it dramatically. ![A robotic claw places a coral puzzle piece into a cream padlock made of interlocking puzzle pieces against a teal background.](https://rews.cc/img/7a4f3fc96065d394807b17af477f645203a23b66.webp) There are two ways to read the result, and DeepMind seems happy with both. The narrow read: the cryptography underneath the Signal app, Google Messages and WhatsApp just got another independent mathematical once-over, and the portions DeepMind examined yielded no new vulnerabilities. If you send a lot of messages, that is genuinely nice to hear. The broad read: DeepMind wanted a demonstration that AI-assisted formal verification is practical enough to aim at real, consequential, widely deployed cryptography rather than toy examples, and Signal is about as real as targets get. Now the caveats, which are also the interesting part. The analysis was limited in scope; it did not formally verify the entire Signal mobile app, which is a much larger and messier object than the protocol’s cryptographic core. And the DeepMind researchers are careful to frame this as one milestone in a longer process rather than a finish line. Swarat Chaudhuri, a DeepMind research scientist, told WIRED: > We are very excited by this result, but there is a long distance to go before we are able to scale this to all the software of the world, and we want to do that. ![A small yellow gear sits beneath a cream bell jar with a coral base, surrounded by large dark gears on a bright blue background.](https://rews.cc/img/42b038ec4cb1af34e3548c476f634406f706eec9.webp) I like the control experiment the team ran, because it tells you the tool is measuring something rather than just handing out clean bills of health. The researchers pointed AlphaProof Code at older versions of Signal containing known, long-since-fixed vulnerabilities. The system correctly identified them — which is to say, it showed those old versions could not be formally verified. A verification tool that verifies everything is a rubber stamp; a verification tool that fails the bad versions and passes the good ones is an instrument. DeepMind is also releasing the specification and the proof it developed for the Signal analysis, so other formal verification work can build on it. That matters more than it might sound. One of the quiet costs of verification has always been that every team starts from scratch, writing its own spec for software somebody else wrote. A published, reusable spec turns verification from a bespoke craft into something a bit more like an accumulating literature. The economic story is a simple one. Bugs in cryptographic software are enormously valuable to find — to defenders, because they protect billions of conversations, and to attackers, for the same reason. Formal verification was always the theoretically correct way to find entire classes of them; it was just priced out of reach for almost everything anyone actually runs. If AI keeps cutting that price, you should expect more of the world’s foundational code to get proved rather than merely trusted. Whether it scales “to all the software of the world” is an open question. But the world has a lot of software, and until recently, essentially none of it could afford a proof.