Google DeepMind’s AI Agents Mathematically Prove Signal’s Encryption Code Is Secure in Four Weeks

Google DeepMind has announced that artificial intelligence agents have produced a machine-checked mathematical proof that the code behind the Signal protocol delivers the security protections it promises, completing in four weeks a task that the laboratory says has long been regarded as one of the grand challenges of software security. The announcement, made on Tuesday 10 November 2026, marks the first time that AI has been used to formally verify a widely deployed cryptographic protocol at this depth, according to Google DeepMind, and the first time that the implementation of such a protocol, rather than merely its design on paper, has been formally verified by any method at all.

The work was carried out with a new system called AlphaProof Code, a multi-agent framework that splits formal verification the way a research team would divide a large project. Human experts decided what needed to be proved, and teams of agents powered by Google’s Gemini Carbon model did the proving, generating more than six million lines of proof in Lean, a computer language whose checker verifies every step mathematically. The result is not a test result or an expert opinion. It is a proof that a computer has checked line by line, and that any other researcher can now inspect, because Google DeepMind has published the full set of verification artefacts as open source.

The timing of the announcement was deliberate. The same day, Google made its most capable model, Gemini 4 Carbon, generally available to paying developers, enterprises and its highest-tier subscribers, after two weeks in which it had been restricted to a small group of cybersecurity defenders. The model that powered the proof is now the model that anyone with a paid account can use, and the proof itself is the strongest demonstration yet of what Google says Carbon was built to do: long, careful, verifiable work on problems that resist shortcuts.

What DeepMind actually proved

The target of the verification was libsignal, the open-source Rust library that implements the Signal protocol, in version 0.105.4, used exactly as published and compiled with the standard Rust compiler for the ARM processors that run in most phones. That choice matters. Most formal verification in cryptography stops at the design level, proving that a protocol described in a research paper is sound. DeepMind’s agents went further, proving properties of the compiled code itself, down to the machine instructions that a processor actually executes. As the laboratory put it in its announcement, real-world vulnerabilities often hide in the gap between a design and its implementation, and bridging that gap is what makes these proofs vastly more complex.

The proof covers the two core mechanisms of a one-to-one Signal conversation. The first is the PQXDH handshake, the post-quantum key agreement that lets two devices establish a shared secret even against an adversary with a future quantum computer. The second is the Triple Ratchet, the mechanism that continually refreshes the encryption keys as messages flow back and forth, so that the compromise of one key does not expose the conversation. Together, the verification establishes four properties that cryptographers regard as the foundations of a secure messenger: forward secrecy, which means that past messages stay secret even if a device is later compromised; authentication, which means that each side is genuinely talking to the person it believes it is talking to; post-compromise security, which means that a conversation can heal itself and become secret again after a temporary compromise; and handshake secrecy, which means that the initial key exchange itself leaks nothing useful to an eavesdropper.

The scale of the exercise is difficult to overstate. The agents generated roughly 6.5 million lines of Lean proof, according to the research paper, a figure that an independent audit by a developer who cloned the published repository broadly confirmed, counting about 7.5 million lines of Lean code across the whole repository. A five-person team at Google DeepMind completed the work in four weeks. Human experts reviewed about one percent of the codebase, the parts the agents themselves flagged as needing a second look, while the Lean kernel, the small trusted checker at the heart of the system, verified the rest automatically. The researchers named on the work are Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, Charles Sutton and Pushmeet Kohli.

Signal’s own engineers were involved in the process. The DeepMind announcement thanks Signal’s Rolfe Schmidt, Michael Rosenberg and Ehren Kret for feedback on the methodology, and Kret, Signal’s chief technology officer, said the work gives the company even greater confidence in its code’s privacy guarantees, according to reporting on the announcement. That endorsement matters because the proof is about Signal’s code, and the organisation that maintains that code has examined how the verification was done.

How AlphaProof Code did it in four weeks

Formal verification has always been a labour of love and endurance. To prove that a piece of software does what it claims, a human expert must translate its intended behaviour into precise mathematics, and then prove, step by step, that the code satisfies that mathematics. The most celebrated success in the field, the verification of the seL4 microkernel, took about twenty person-years, according to The Register, while developing the verified CompCert C compiler took six years. Against that background, four weeks for a team of five looks less like an incremental improvement and more like a change in what is possible.

AlphaProof Code works by dividing the labour. Human researchers collaborate with a mix of models to translate Signal’s security goals into formal mathematical specifications, with human experts reviewing every specification. From there, agents powered by Gemini Carbon take over the proving, generating the millions of lines of Lean code that connect the specification to the compiled machine code. The agents then audit their own work, highlighting the areas that need a second look by a human. Because Lean checks the rest automatically, the experts can concentrate their attention where human judgement matters most. As DeepMind put it, the agents wrote the proofs, but the humans decided what “secure” should mean and approved every trusted statement.

The team also built in a control experiment, the kind of test that separates a genuine verification from a system that merely rubber-stamps whatever it is shown. They took an isolated copy of Signal’s code and deliberately reintroduced two real bugs that the library had previously shipped and later fixed, known in the paper as the “weak state” and “small subgroup” flaws. In both cases, AlphaProof Code produced a machine-checked proof that the altered version was insecure, refusing to certify code it knew to be broken. The analysis found no new vulnerabilities in the portions of the protocol it examined, according to WIRED’s reporting on the announcement, which is the outcome the researchers would have hoped for but could not have assumed.

The project also answers a challenge issued in April 2026 by the Beneficial AI Foundation, which asked whether the Signal protocol and the Signal app could be formally verified using Lean. DeepMind’s work covers the protocol library rather than the full app, so the challenge is not yet fully answered, but the laboratory describes its result as a step towards it, and the foundation’s challenge is credited in the announcement as part of the motivation for the work.

What the proof does not cover

Any honest account of this announcement must spend as much time on its limits as on its achievements, because the researchers themselves do. The proof assumes that the underlying cryptographic building blocks are sound. It verifies that the protocol’s logic uses those blocks correctly; it does not prove that the blocks themselves are unbreakable. It covers one-to-one sessions in a specific build of the library, running as a fresh process, not the full Signal application as installed on a phone. Key generation was not verified. Group messaging, sealed sender, server-side code, multi-device state and side-channel attacks, in which an attacker learns secrets from timing or power consumption rather than from the mathematics, all sit outside the scope of the work. The post-quantum healing mechanism known as SPQR was not proved either.

The Register, which interviewed Chaudhuri about the work, put the point plainly: the result is theoretical in that it assumes perfect cryptography and does not guarantee the computational secrecy of individual bytes, but it remains a meaningful assertion of correctness. That framing is the right one. A mathematical proof about code is not a certificate that a product can never be hacked. It is a guarantee about a defined implementation, a defined execution model, a defined set of properties and a defined set of assumptions. What makes this proof significant is that the definitions are unusually precise and unusually close to the code that actually runs, and that the guarantee was produced by machines in weeks rather than by humans over years.

For Signal users, there is no emergency patch or account change attached to the announcement, and nothing in the work suggests that anyone should change how they use the app. The value of the proof is structural. It means that the most scrutinised part of one of the world’s most trusted messaging systems now carries a kind of assurance that no widely deployed protocol has carried before, and that the method used to produce it can, in principle, be applied to other software.

The same day’s second announcement: Gemini 4 Carbon goes on general sale

The verification was not the only news from Google on 10 November. The company also made Gemini 4 Carbon, its strongest model, generally available to all paying developers and enterprises through the Gemini API in Google AI Studio and Android Studio, and to subscribers of its top-tier Google AI Ultra plan in the Gemini app, Google Antigravity and AI Mode in Search. The model had first been announced on 28 October, but access had been limited to a subset of cybersecurity defenders through Google’s Fairwind Program. The 10 November launch opened it to everyone else.

Carbon is built on the same foundation as Gemini 4 Argon, which Google released in October, with additional post-training for deep reasoning, extended verification and multi-step agent workflows, according to the model card. Google describes Carbon as the model for tasks that test the limits of a model’s intelligence: complex, multi-step coding and debugging, open-ended scientific research and discovery, and long-horizon agentic work. Argon, the company says, remains the right choice for most software engineering and knowledge work. Carbon is for the hardest jobs, and it consumes more tokens doing them.

The pricing reflects that positioning. Through 30 November 2026, Carbon costs two dollars per million input tokens and ten dollars per million output tokens, the same introductory rate as Argon. From 1 December, the price doubles to four dollars per million input tokens and twenty dollars per million output tokens, and every token is billed, including the tokens the model spends thinking. There is no free tier. For everyday users on free or AI Pro plans, Carbon is not yet available at all.

On benchmarks, Google says Carbon ranks first on CursorBench 4.0, Perplexity’s WANDR and Zapier’s AutomationBench, at more than twice lower cost per task than the next best external model, and scores 59 on the Artificial Analysis Intelligence Index version 5.0, compared with 50 for Argon. Those are the company’s own chosen measures, and independent benchmarks will matter more than launch-day claims, but the direction is clear: Google is positioning Carbon as a reasoning-first model for work that unfolds over hours rather than seconds.

The company is also previewing a feature called /swarm in Google Antigravity, which turns a single prompt into a coordinated team of agents that a user can track in real time, assigning Carbon to the roles that demand the deepest reasoning, such as architectural design and auditing, while faster, lighter models handle parallel work. And the same launch week brought Gemini Robotics 2.5, unveiled for trusted testers and robotics partners, which Google says reached a 96 percent success rate in an autonomous kitting task on Apptronik’s Apollo 2 humanoid robot during factory pilots with Mercedes-Benz in Kecskemét, Hungary, and Sindelfingen, Germany.

Carbon’s cybersecurity credentials were part of the launch as well. Google says that in simulated cyberattack testing, Carbon blocked 99 percent of attack trajectories from an adaptive red-teaming agent, lowering the per-attempt breach rate to 0.8 percent, down from 3.1 percent on Argon, and that it achieved a zero percent prompt injection success rate on the Gray Swan benchmark, the first time that milestone has been reached. Its Cloud Vulnerability Research team recently used Carbon to prove that two bugs in a popular open-source project were in fact exploitable vulnerabilities, comparable in severity to a recent high-profile exploit, helping maintainers reclassify the bugs as critical and issue a patch. In a separate exercise with the security firm Wiz, the model uncovered previously unknown vulnerabilities at two major software providers in under two hours, compressing weeks of research into a single afternoon.

Why the Signal protocol was the test that mattered

To understand why DeepMind chose Signal, it helps to understand what the Signal protocol is and how far it reaches. The protocol was developed by Open Whisper Systems, the non-profit founded by Moxie Marlinspike and Trevor Perrin, and its central mechanism, the Double Ratchet, was designed so that every message is encrypted with a fresh key, and so that the keys themselves are constantly refreshed. If one key is somehow exposed, it unlocks at most a single message, and the conversation heals itself as new keys are generated. That design has become the template for modern encrypted messaging.

The protocol’s influence extends far beyond the Signal app itself. The same protocol family also powers end-to-end encryption in WhatsApp, used by billions of people, and in Google Messages, according to industry reporting, which means that the code DeepMind verified sits, in one form or another, at the heart of a large share of the world’s private digital conversation. When Google DeepMind says the protocol protects billions of private conversations, that is the scale it is describing. A flaw in this code would not be a flaw in one app. It would be a flaw in the infrastructure of private communication itself.

That is also why the distinction between verifying a design and verifying an implementation matters so much. The history of cryptography is full of protocols that were sound on paper and broken in practice, because the code that implemented them made a small mistake: a random number generator that was not random enough, a check that was skipped under an unusual condition, a buffer that overflowed. The most famous example is Heartbleed, the 2014 flaw in the OpenSSL library, in which a single missing bounds check exposed the memory of servers across the internet, including passwords and private keys, for years before anyone noticed. The protocol behind it, TLS, was not broken. The implementation was. DeepMind’s work is an attempt to close exactly that gap, by proving things about the compiled code rather than the diagram.

There is also a competitive context that cannot be ignored. The announcement comes in the same month as Anthropic’s enormous public listing, and in a year in which every major laboratory has been racing to show that its models can do more than chat. Google’s claim is distinctive: not that its model is the fastest or the cheapest, but that it can produce mathematical certainty about software that people’s safety depends on. That is a different kind of benchmark, and it is one that competitors will now have to answer.

Analysis: Why It Matters

Proof is stronger than testing, and that changes the security argument

Most software security rests on testing. Engineers write tests, attackers probe for weaknesses, and everyone hopes that the probing was thorough enough. Testing can show that a bug exists. It can never show that no bug exists, because there are always inputs nobody tried. A formal proof inverts that logic. If the specification is right and the checker is sound, the proof shows that no input within the defined model can violate the stated properties. That is a categorically stronger claim, and it is why formal verification has always been described as the gold standard of software assurance, even while it remained too slow and expensive for almost everything except the most critical systems. What DeepMind has shown is that the cost side of that equation may be collapsing. If a proof that would once have taken years can now be produced in weeks, the question for every organisation that writes security-critical software is no longer whether formal verification is affordable, but whether it can afford not to do it.

The bottleneck has moved from proving to specifying

Perhaps the most interesting observation in the whole announcement comes from Chaudhuri himself, who told The Register that formal methods researchers spent thirty or forty years believing that verification was the hard part, and that now the machines can do the verification, the question has become what to verify. That is a profound shift. Writing a specification, deciding precisely what “secure” means for a given system, is a human judgement about values and threats, not a mathematical exercise. It requires deciding which properties matter, which attackers to defend against, and which risks to accept. No agent can make those decisions on its own, because they are decisions about what the world should be like, not about what follows logically from a set of axioms. The researchers’ own conclusion is that the next frontier is not proof but specification, and that the hard problem of the coming decade will be teaching organisations to say clearly what they want their software to guarantee. That is a management and governance challenge as much as a technical one, and it will reward the organisations that think hardest about their own requirements.

Defence is finally getting the same AI leverage as offence

For the past two years, the dominant story about AI and cybersecurity has been an alarming one: AI makes attackers faster, letting them find vulnerabilities, write phishing messages and automate intrusions at a scale no human team can match. DeepMind’s announcement is the clearest counter-example yet to that narrative. The same capabilities that let an agent generate millions of lines of code can be turned to the task of proving that code correct, and the same models that can be used to find flaws can be used to certify their absence. Chaudhuri made the point directly, arguing that the world is full of insecure systems that are going to be exploited, and that the technology must now be applied to code at large to work out what needs guarding. The race in cybersecurity has always been between those who find flaws and those who fix them. For the first time, the defenders have a tool that scales at the same speed as the attackers’ tools, and the long-term balance of that race may depend on how quickly it is adopted.

A model launch and a proof on the same day is not a coincidence

It is worth noticing that Google chose to announce the general availability of Gemini 4 Carbon and the AlphaProof Code result on the same day, with the proof featured prominently inside the Carbon launch post itself. That is marketing, but it is also an argument. The proof is the evidence for the claim that Carbon is a different kind of model, one built for long, careful, verifiable work rather than for quick answers. Every laboratory can claim that its model reasons well. Very few can point to a machine-checked proof about the encryption that protects billions of conversations and say, in effect, that this is what the model did. Whether the market accepts that argument will depend on what Carbon does next, but the strategy is clear: Google is competing on trust and verifiability, not only on benchmark scores, and it is using its own research as the demonstration.

The limits are the point, not a footnote

It would be easy to treat the limitations of the proof as a disappointment, a list of asterisks attached to a bold claim. That would be a mistake. The limitations are precisely what make the claim credible. A proof that pretended to cover the whole Signal app, every device, every side channel and every future version would be a proof that nobody should believe, because no such proof can exist. By stating exactly what was verified, under which assumptions, and for which build of the code, the researchers have given other experts something they can check, challenge and build on. That is how science works, and it is how security should work too. The honest scope of this proof is what separates it from the many AI announcements that promise everything and demonstrate nothing. The next step, as Chaudhuri himself acknowledged, is to extend the technique from cryptographic protocols to software in general, and to apply it during the design process rather than after the code is written. That work has, in his words, a long distance to go, but the direction of travel is now visible.

What to Watch Next

1. Whether independent researchers reproduce or challenge the proof now that the Lean artefacts are public on GitHub, and whether any of them find a gap in the specification that the agents did not catch.
2. Whether Signal adopts formal verification as a routine part of its own development process, and whether the Signal Foundation publishes its own assessment of the DeepMind work.
3. How quickly DeepMind extends AlphaProof Code beyond cryptography, to medical device firmware, power grid software and other critical infrastructure, as its announcement suggests it intends to do.
4. Whether other AI laboratories respond with their own verification results, turning formal proof into a new front in the competition between frontier models.
5. What Gemini 4 Carbon does in its first weeks of general availability, and whether its reasoning performance in real products matches the benchmark claims Google made at launch, particularly after its price doubles on 1 December.
6. Whether regulators and standards bodies begin to treat machine-checked proofs as evidence of due diligence for critical software, and what that would mean for companies that cannot yet produce them.

Sources

• Google DeepMind — Formal Verification of Signal’s Protocol with Gemini (10 November 2026)
• The Register — Google DeepMind melds humans and AI agents to vet Signal’s secure messaging techniques (10 November 2026)
• Google — Gemini 4 Carbon is now available (10 November 2026)
• Dev.to — 6.5M lines of Lean: I counted DeepMind’s Signal proofs (10 November 2026)
• GoTechPresso — Google DeepMind’s AI Agents Wrote 6.5 Million Lines of Proof (11 November 2026)
• Google DeepMind on GitHub — AlphaProof Code verification artefacts (code-verification repository)