Google DeepMind has used teams of AI agents to write a machine-checked proof that the encryption code behind Signal keeps its main security promises, and it did so on the compiled machine code rather than the source. The proof runs to about 6.5 million lines of Lean and took a team of five people four weeks. No human wrote proof code. What humans did write, review and approve were the specifications, and that is the part European organisations should pay attention to: when AI can produce the proof, trust moves to the definition of what had to be proven.
The system is called AlphaProof Code. Here is what it verified, where the proof stops, the governance pattern that made it trustworthy and what it means under the Cyber Resilience Act and in Europe’s encryption debate.
What AlphaProof Code verified
The target is libsignal, the open-source library that implements the Signal protocol. DeepMind took version 0.105.4 with the spqr 1.6.0 module and covered one-to-one sessions: the PQXDH handshake, which sets up a shared secret designed to resist future quantum attacks, and the Triple Ratchet, which derives fresh keys as a conversation goes on.
The unmodified Rust code was compiled with the standard compiler into a single 64-bit Arm Linux executable. The proofs work on the bytes of that binary, instruction by instruction, against a Lean model of how an Arm processor and Linux behave. That covers roughly 140,000 instructions, and it means the compiler does not have to be trusted.
Two kinds of proof were produced. A symbolic proof assumes perfect cryptography and checks the protocol logic, including forward secrecy, post-compromise security, peer authentication, resistance to key compromise impersonation and protection of handshake keys against harvest-now-decrypt-later attacks. A computational proof works from standard hardness assumptions and bounds how much advantage an attacker can gain against message confidentiality and authenticity. According to the technical paper, this is the first time protocol-level guarantees have been tied to the unmodified code of a widely used cryptographic implementation.
For context, the seL4 microkernel took twenty person-years to verify and the CompCert C compiler six, and both were written with verification in mind. libsignal was not.
Where the proof stops
Several early headlines claimed Signal is now proven secure. The paper is more careful, and anyone citing this work in a risk assessment should be too.
- Not the apps. The verified program is a small command-line harness around the library. The same Rust code underlies the Android and iOS apps, but the apps themselves were not verified.
- One build, one-to-one. Group messaging, multi-device state and key generation are outside the scope. WhatsApp and Google Messages use the Signal protocol, but the proof concerns this libsignal build, not their software.
- No side channels. Timing and power analysis are not modelled.
- Assumptions remain. The proofs assume the cryptographic primitives behave as specified, and 39 helper routines are replaced by contracts that were not proven against the real code.
- Limits at scale. The statistical bound becomes vacuous at around 25,000 messages in a single session, and the post-quantum healing of the newest ratchet layer is not proven.
The team also tested whether the method can tell good code from bad. It reintroduced two previously fixed libsignal bugs found by other researchers and obtained machine-checked proofs that the modified binary violates the security theorem, with concrete attack traces. That shows the pipeline catches those two flaws, not every flaw. No new vulnerabilities were found in the verified parts.
One more source of confusion: DeepMind’s own blog mentions both “over six million” and “over three million” lines. The paper puts the proof at about 6.5 million lines.
The governance pattern behind the proof
The engineering is impressive, but the more transferable lesson is how DeepMind organised the agents so their output could be trusted.
Five people chose what to prove, guided a specification-writing agent and approved every specification. The paper says most of the human effort went into specifications rather than proofs. Reviewer agents from a different model family checked each draft for faithfulness and strength. Specifications were developed with Gemini 4 Carbon and Claude Opus 5.5. Proof teams of 40 to 80 agents, running on Gemini 4 Carbon, then worked for 24 to 72 hours at a time on a single machine.
Three controls made the result trustworthy:
- The worker is not the judge. A gatekeeper accepts a proof only if Lean’s small kernel accepts it and a comparator tool confirms that the proven statement is identical to a held-out copy of the approved specification.
- The goal is locked. Agents cannot edit the specification. Amendments need a machine-checked justification, must not weaken security and require human approval for changes to trusted assumptions, and they are logged.
- Shortcuts are banned. Placeholders and unchecked tactics are rejected, and every proof is replayed in a fresh environment.
These controls exist for a reason. The paper notes that agents under pressure to finish sometimes weaken their goal, and describes another agent swarm in which one agent redefined a condition as always false and the trick spread. The result is a trusted base of about 26,000 lines, the specifications plus the Arm semantics, against 6.5 million lines of proof that nobody needs to read. According to DeepMind’s blog, the agents flagged the areas that needed human review, about 1% of the codebase.
The same pattern applies to any organisation using coding agents today, with or without formal methods. Compare the AWS Emulator, built entirely by AI agents nobody reviewed, where a 56.5% test score is the only map of where to trust it, or agentic code review, where accountability stays with you. Keep the agent that does the work separate from the check that approves it, and keep the definition of done out of the agent’s reach.
Specification becomes the asset to govern
Swarat Chaudhuri of DeepMind told The Register that “the next frontier is not going to be proof but specification”. A flawed specification yields a valid proof of the wrong thing. That turns specifications into business and risk artefacts in their own right: someone has to own them, review them, decide who may change them and revisit them when the product or threat model changes.
For security leaders, that changes the question to ask vendors. “Is it verified?” is not enough. Ask which build, which properties, under which assumptions, and who approved the specification.
What it means in Europe
The Cyber Resilience Act. Its reporting obligations have applied since 11 September 2026, and the full regime applies from 11 December 2027, as CMS summarises. Manufacturers of products with digital elements will have to show their products meet essential cybersecurity requirements. Formal proofs are not required, but for cryptographic components they are about the strongest evidence of secure design available, and tools like this could make them affordable beyond a handful of showcase projects. Our overview of how AI is rewriting the security agenda and Europe’s reporting clocks covers the wider context.
The encryption debate. The EU’s child sexual abuse regulation, often called chat control, is still in trilogue. The Council’s November 2025 position dropped mandatory detection orders, and detection remained the sticking point through 2026, according to the legislative timeline. A proof like this one applies to a specific build. Any change to the protocol code, whatever its purpose, would fall outside it and need new proofs. Policymakers who weigh changes to encrypted messaging can now ask what such a change would cost in verified guarantees.
Openness and dependence. The verification ran on US frontier models, and Google has not disclosed the cost beyond saying it took “quite a few tokens”. The specifications and proofs are public on GitHub under the Apache 2.0 licence, so European researchers and auditors can check them independently. Checking takes several hours and 15 to 34 GiB of memory, not a frontier model. The work also feeds Signal Shot, the effort launched in April 2026 by Signal, the Beneficial AI Foundation and the Lean FRO to verify the Signal protocol and its Rust implementation in Lean.
What to do now
- List the components where a flaw would be catastrophic, such as cryptography, authentication and payment logic. These are the first candidates for formal assurance as costs fall.
- When a supplier claims formal verification, ask for the scope: build, properties, assumptions and who approved the specification.
- Treat specifications and acceptance criteria as owned, versioned assets, with clear rules on who may change them.
- Apply the maker-and-judge split to every coding agent you run, even if your judge is a test suite rather than a proof checker.
- Follow the open artifacts and Signal Shot. Independent European review of these proofs would add real value.
Frequently asked questions
Is Signal now proven unbreakable?
No. The proof shows that the handshake and ratchet in one libsignal build meet their stated properties under the model’s assumptions. The apps, group chats and side channels are out of scope.
Does this cover WhatsApp?
Not directly. WhatsApp uses the Signal protocol, but the proof concerns the compiled code of libsignal 0.105.4, not WhatsApp’s software.
Can organisations use AlphaProof Code?
Not as a product. DeepMind published the paper and the Signal proofs, not a verification service, and its researchers say scaling to all software still needs much more research.
The proof is done, the questions move upstream
For years, formal verification was limited by how hard proofs were to write. If agents can now write them in weeks, the scarce skill becomes deciding precisely what must be true, and the scarce control becomes who is allowed to change that definition. Those are governance questions as much as engineering ones, and they land on the desks of people who will never read a line of Lean.
