Google DeepMind announced that its AlphaProof Code system has mathematically proven selected security properties of real code that protects the private messages of billions of people. This is a significant step, but the slogan “the end of software bugs” would be premature. Here’s what actually worked—and what didn’t.
What DeepMind Announced
On November 10, 2026, Google DeepMind announced that researchers had used the AlphaProof Code agent system to formally verify the key cryptographic guarantees of the protocol used in the Signal messaging app. This is an encryption protocol that, in a modified form, also protects other major messaging services. The project lasted four weeks, and according to DeepMind, it was a research collaboration conducted free of charge.
The depth of verification is crucial: not just a protocol design on paper, but, according to DeepMind, the actual implementation code, down to the level of compiled machine code. Most previous work stopped at the architecture or smaller parts of the code. DeepMind claims that this is the first verification of such an extensive implementation of the protocol by an AI system and has published a technical paper as well as the underlying artifacts.
What Is Formal Verification (and How Does It Differ from Testing)?
When testing, you check whether the program works for selected inputs. What you haven’t tested, you can’t see. In formal verification, you mathematically prove that the program satisfies a predefined requirement for all possible inputs. The proof is written in a language that is checked by a special program, so the correctness of the proof does not need to be assessed by a human.
It’s like the difference between testing a bridge with a few trucks and using a mathematical calculation to determine that it can withstand any load up to a certain limit. However, the calculation is only valid under the assumptions you enter into it.
How AlphaProof Code Did It
- People and models first wrote down what should hold true. They translated the protocol’s goals into mathematical specifications, and human experts reviewed each one before the proofs were run.
- Agents then generated the proofs. The system generated more than 6 million lines of proof in a language designed for machine verification.
- Humans checked only a small portion of it. According to DeepMind, the agents flagged approximately one percent of the code for further human review.
- The proofs also cover post-attack scenarios. They include privacy protection both during and after a temporary compromise of the device.
An important validation test: when the system was run on older versions with vulnerabilities already patched, it found these errors and demonstrated that these versions cannot be validated. The validator therefore does not allow bad code to pass, which is exactly what we expect from it.
What it is not
- This is not proof that “Signal is perfectly secure.” Only selected properties of the cryptographic code’s core were verified under specified assumptions—not the entire application, nor all the ways it could fail.
- This is not “100 percent” certainty about the software. A proof is only as good as its specification. If a requirement is written incorrectly or incompletely, the program may mathematically satisfy something that nobody intended.
- It is not a tool that every developer can download today. It is a research system and a set of published artifacts, not a finished product for everyday use.
- He did not find any new bugs in the protocol’s new features. Researchers did not report any new flaws in the examined sections. Furthermore, the protocol itself has been analyzed by academics for years.
Why is this important anyway?
Formal verification has long been considered too expensive and too slow for widely used production code. If AI agents can generate machine-verified proofs for real-world implementations in a matter of weeks, the focus of the work shifts: from writing proofs to writing precise specifications and verifying the assumptions on which the proofs are based. In other words, whoever writes the specification is, in fact, deciding what “secure” means.
Experts also point out that the question of cost remains open: whether such verification can be scaled beyond exceptionally critical code, such as encryption libraries.
What does this mean for developers?
- Formal verification will likely first become widespread in areas where the cost of an error is high: cryptography, protocols, operating system kernels, and healthcare and transportation software.
- For everyday web or mobile development, testing, code reviews, secure configurations, and updates remain the foundation. Formal proofs do not replace them.
- Learning to write clear requirements—specifying exactly what must hold true and what must never occur—is useful even without proofs.
Summary
AlphaProof Code has demonstrated that AI can collaborate with humans to perform machine verification of real cryptographic code on a scale that was practically unattainable until recently. This is a true milestone. However, it does not spell the end of software bugs, because the proof only addresses what we chose to write down, and the other layers of the system remain the responsibility of humans. The good news is that verification is shifting from an academic luxury to something that can be done within a reasonable amount of time. And that’s worth keeping an eye on.
