On this page
Google DeepMind said on 10 November 2026 that a new AI system called AlphaProof Code has produced machine-checked mathematical proofs of key security properties in the code behind the Signal protocol. In its announcement, the company said the work took four weeks and generated more than six million lines of proof. It is a significant result, but a narrower one than "Signal is proven secure": it covers specific parts of the cryptographic library, under stated assumptions, and not the Signal app as a whole.
What did Google DeepMind announce?
DeepMind's blog post, written by Pushmeet Kohli and Swarat Chaudhuri, describes AlphaProof Code as an agentic framework for formal verification that combines human expertise with AI agents. The company says the agents that wrote the proofs were powered by a Gemini model it calls Gemini Carbon.
The target was Signal's core cryptographic code. DeepMind describes the protocol as "the technology that protects billions of private conversations in apps like Signal and Google Messages".
According to the technical write-up published with the proofs, the team verified a test harness built from libsignal version 0.105.4, Signal's cryptographic library, compiled into a program for AArch64 (64-bit Arm) processors. The proofs were written in Lean, which DeepMind describes as a computer language that mathematically proves the accuracy of code.
The headline numbers are large:
- About 6.5 million lines of machine-checked Lean proof code, according to the technical write-up.
- About 26,000 lines of trusted specifications and processor semantics that the proofs rest on.
- Four weeks of work by a team of five people, as reported by The Register.
- Human review focused on areas the agents flagged, which DeepMind says amounted to "just one percent of the codebase".
What does "formally verified" mean in plain language?
Most software is checked by testing: you run it many times and look for failures. Testing can show that bugs exist, but it cannot show that none remain.
Formal verification takes a different route. People write a precise mathematical statement of what the software must do, called a specification. A proof then shows that the code meets that statement in every possible case, and a small, trusted checking program confirms each step of the proof.
The benefit is that nobody has to trust the author of the proof. The DeepMind write-up says its AI-written proofs are treated as untrusted and count only because Lean's checker accepts them. That matters when the author is an AI model that can make confident mistakes.
The catch is the specification. A proof is only as meaningful as the statement being proved, and the write-up is open that specifications "cannot be automatically checked". DeepMind says several models helped translate Signal's security goals into formal specifications, with human experts reviewing every one.
What exactly was proved?
The write-up says the proofs cover Signal's PQXDH handshake, which sets up an encrypted conversation, and the Triple Ratchet, which keeps changing the keys as messages are exchanged. Signal introduced the Triple Ratchet in a blog post on 2 October 2025, describing it as its existing Double Ratchet combined with a new post-quantum ratchet.
Four properties were proved for one-to-one conversations:
| Property | What it means for a user |
|---|---|
| Forward secrecy | Stealing today's keys does not expose past messages |
| Post-compromise security | A conversation recovers its protection after a temporary compromise |
| Authentication | You are talking to the person you think you are |
| Handshake secrecy | The keys agreed at the start of a conversation stay secret |
The unusual part is the level at which this was done. DeepMind's blog notes that most protocol verification stops at the design level, while real flaws often sit in the gap between design and implementation. Here the proofs concern the compiled machine code. The Register reports the researchers' claim that this is the first time AI has helped devise a proof linking protocol-level security guarantees to a widely used cryptographic implementation.
As a test, the team put two real, previously fixed libsignal bugs back into an isolated copy of the code. DeepMind says that in both cases the system produced a machine-checked proof that the buggy version was insecure. Neither the blog post nor the write-up reports any new flaw in Signal's code.
What was not proved?
This is where the fine print matters. The technical write-up lists limits that readers should keep in mind:
- Idealised cryptography. The main guarantees are "symbolic": in the write-up's words, "they assume perfect cryptography and say nothing about the computational secrecy of bytes". A separate computational proof covers only classical attackers, not quantum ones.
- One-to-one chats only. The write-up states: "We leave group messaging as future work." Multi-device state is also outside the scope.
- Parts of the code are excluded. Key generation is not verified, and neither is the post-quantum "healing" provided by Signal's newest ratchet.
- A library, not an app. The verified program is a harness around libsignal. The Signal app, its user interface, the phone's operating system and anything else on a device are outside the proof.
- Trusted foundations. The result depends on the human-reviewed specifications, the model of the processor and Lean's checker being right.
The Register summarised the position by calling the result "theoretical in that it assumes perfect cryptography".
Why does it matter for people who use Signal?
For everyday users, nothing changes today. No update is needed and no weakness was disclosed. The value is added confidence in machinery that was already heavily studied. Signal's own 2025 post says formal verification was part of the Triple Ratchet design from the start, using other tools.
Signal's chief technology officer, Ehren Kret, is quoted in DeepMind's announcement: "Using AI agents to translate live code into valid Lean theorems is a major breakthrough."
Our analysis: the proof does not protect anyone against the more common ways private messages leak, such as a stolen unlocked phone, malware on the device or a contact who shares a screenshot. Those sit outside any protocol proof, and they are a reminder that encryption is one layer among several. Our guide to cybersecurity challenges and solutions covers the wider picture.
How does this fit the wider push for AI-assisted proofs?
Formal verification has historically been slow and expensive. The Register notes that verifying the seL4 microkernel took 20 person-years and that the verified CompCert C compiler took six years to develop. Four weeks for a five-person team is a very different scale of effort, although The Register also reports it took "quite a few tokens", meaning a heavy use of AI computing.
The work also lands in an active field. The Beneficial AI Foundation launched Signal Shot on 20 April 2026, a project to formally verify the Signal protocol and app with Lean. The Register describes DeepMind's result as a step toward that challenge.
It is also a practical example of agentic AI: teams of AI agents working for long stretches on a task with humans setting the goals. Chaudhuri told The Register: "It's a system that is fundamentally built for human AI collaboration."
He was also clear about where the hard problem now lies. "We really believe that the next frontier is not going to be proof but specification in this kind of research," he said. On ambition, he added: "The dream is definitely to scale this up."
DeepMind says it is open-sourcing its formal verification artifacts for community use, so outside researchers can inspect the specifications and proofs. That independent scrutiny, particularly of the specifications, will decide how much weight the result carries. DeepMind itself says that scaling these techniques requires continued research.
Sources
FAQ
Frequently asked questions
No. The proofs cover specific security properties of parts of libsignal, Signal's cryptographic library, for one-to-one conversations. The full app, group messaging, key generation and the device it runs on are outside the scope, and the main guarantees assume idealised cryptography.
AlphaProof Code is a Google DeepMind system announced on 10 November 2026. It uses teams of AI agents, guided by human experts, to write formal specifications and proofs about software in the Lean language. Lean's checker then confirms that each proof is valid.
DeepMind's blog post and technical write-up do not report any new flaw. The team did reintroduce two real bugs that had already been fixed, and says the system proved in both cases that the buggy version was insecure.
No. The research was carried out on existing code and did not lead to any announced change for users. Keeping the app and the phone's operating system up to date remains sensible general practice.
DeepMind's announcement names Signal and Google Messages as apps protected by the protocol. The verification was performed on Signal's own libsignal library, so it does not automatically say anything about how another app has built the protocol into its product.
Spotted an error? Tell us. Read how we report and correct stories in our editorial policy.
Written by
Mainstream Tech
Newsroom
News and analysis on technology, AI, business, politics and international affairs, from our newsroom in London.
More from Mainstream
