Google DeepMind uses AlphaProof Code to verify Signal Protocol code

10 November 2026: Google DeepMind has announced that its new AlphaProof Code framework used AI agents to mathematically verify selected security properties of the machine code underlying the Signal messaging protocol. The team completed the project in roughly four weeks, a notable result for a type of software assurance that can demand substantial specialist effort.

The breakthrough is not a claim that every part of Signal is now provably secure. It is that formal verification reached production-level protocol code rather than stopping at a model of how the cryptography ought to behave. The scope of the proof determines both the research’s significance and its limits.

In its AlphaProof Code announcement, DeepMind describes a longer-term ambition: using AI to make mathematical assurance practical for security-critical software, from messaging systems to medical devices and power infrastructure.

What did Google DeepMind actually prove about Signal?

Formal verification starts with a precisely expressed requirement, then uses mathematical reasoning to show that a system meets it under stated assumptions. Unlike conventional testing, which samples particular inputs and scenarios, a valid formal proof covers the behaviours represented by its mathematical model.

DeepMind says it verified key security properties of machine code involved in the Signal protocol. Pushmeet Kohli, Google Cloud’s chief scientist and a DeepMind research leader, describes this as a first for the production code of a widely deployed protocol at this depth. That is the team’s priority claim, not evidence that no part of Signal had ever been formally analysed before.

DeepMind’s public summary does not provide a property-by-property account detailed enough to claim that it proved resistance to every attack class. In particular, cryptographic correctness should not be confused with a blanket guarantee against compromised devices, malicious backups, metadata exposure or every possible side-channel attack.

Why verifying machine code is harder than proving a protocol design

Signal’s cryptographic protocols have a history of formal analysis. Those earlier results matter, but proving a protocol design secure does not automatically prove that the instructions executing on a phone match the design. Implementations add detail: branches, data representations, library calls, optimisation, and assumptions about the execution environment.

Consider a security proof that assumes a secret is erased when a session ends. A protocol-level proof can describe that condition without showing that a particular compiled implementation actually performs the required erasure. Likewise, a sound cryptographic design does not excuse an implementation that mishandles a state transition. The closer verification gets to the deployed instructions, the smaller this design-to-execution gap becomes.

Machine-code verification still has boundaries. Someone must specify what an instruction means, which environmental behaviours are trusted and which binary or code revision the proof concerns. An app update, a different build configuration, or a changed dependency could require new evidence. A result for one verified component cannot simply be stamped onto the complete software supply chain.

How AlphaProof Code uses AI without letting it mark its own homework

DeepMind describes AlphaProof Code as an agentic formal-verification framework that uses large language models, including Gemini Carbon, to help develop specifications and proofs. AI agents can break large goals into smaller proof obligations, propose intermediate arguments and revise attempts that fail checking. The important control is that the result must be judged against formal requirements, with expert review at critical points.

This addresses a well-known failure mode in formal methods: a developer can accidentally write a specification that reproduces the same mistaken assumption as the code. The resulting proof may be mathematically valid yet establish the wrong requirement. The risk becomes sharper when an AI system is asked to infer both the intended behaviour and the proof solely from the implementation it is supposed to audit.

A credible workflow therefore separates the security goal, the implementation and the checking process. Human reviewers should be able to ask who approved the specification, whether the proof covers the intended code, and whether an independent checker accepts the evidence. This is closer to an auditable engineering process than asking a chatbot to declare an application secure.

The four-week result needs a careful comparison

Kohli says comparable formal-verification efforts can demand decades of combined specialist effort, whereas his team completed this work in a month. That describes the reported project duration, not a published, controlled speed comparison against an equivalent human-only team.

The researchers also benefited from earlier Signal verification research. The paper discloses no end-to-end cost figure, detailed accounting of human review hours, or public benchmark showing what happens on unrelated codebases. Four weeks is impressive for this specific project, but it is not enough information to calculate a reliable cost per verified line of production code.

The most meaningful repeatability test would give independent teams the same stated security goals and code revisions, then measure total human time, compute cost, accepted proofs, uncovered gaps and the effort required after a code change. A system that quickly produces proofs requiring weeks of expert repair might still be valuable, but its economics would look different from a largely automated verifier.

What happened when AlphaProof Code examined older Signal versions?

WIRED reports that the team also applied AlphaProof Code to older versions containing known, already-fixed weaknesses. It identified those flaws and could not establish the same guarantees for the vulnerable versions. No new vulnerabilities were reported in the portions of current code examined.

That negative-control exercise is important. A verification system that approves only the current version is harder to assess than one that also rejects a deliberately vulnerable historical example for the right reason. Nevertheless, detecting previously known flaws is not proof that the framework would find every unknown bug in a fresh implementation.

What does this change for developers working with AI coding agents?

Most AI coding tools are evaluated by whether they create a plausible patch and pass tests. DIY AI’s coding-agent benchmark framework treats independent acceptance checks as more meaningful than an Agent’s own success message. Formal verification takes the principle further: for selected high-risk properties, it asks for a mathematical argument instead of another batch of passing examples.

A practical way to use that idea is to avoid trying to prove an entire website or mobile app. Start with the code whose failure would have the clearest security consequences: permission checks, cryptographic state transitions, signing logic or payment authorisation. Define a narrow invariant, such as an unauthorised actor never receiving an elevated capability. Then identify the exact implementation boundary that must satisfy it.

AI can assist with proof construction, but production teams still need versioned specifications, reproducible builds, independent checking and a policy for invalidating proofs after relevant changes. The human-supervision issue also appears in our coverage of Microsoft’s proposed Humanist AI code of conduct: agents need enforceable boundaries and reviewable evidence, rather than relying entirely on their own descriptions of success.

Five questions to ask before trusting an AI-generated security proof

• What exact property was proved? Look for a formal statement, not just terms such as ‘secure’ or ‘verified’.
• Which executable code does it cover? Establish the revision, build settings, library boundaries and platform assumptions.
• Who approved the specification? A proof of a requirement copied from buggy code may miss the real security goal.
• Can somebody else check the proof? Reproducible proof artefacts and a separate checker are more useful than a model-generated explanation.
• What happens after an update? The team should know which changes invalidate the proof and what must be rerun.

DeepMind is releasing proof artefacts, not promising a security product

DeepMind says it is open-sourcing the formal specifications and verification artefacts from the Signal project so that other researchers can examine and extend the work. This should not be read as confirmation that the full AlphaProof Code framework, its underlying models or a managed verification service are available to download or buy.

The next convincing milestone would be independent reproduction, followed by similarly deep verification on a different real-world codebase without extensive preparatory work. The harder commercial question is whether the method can remain affordable as versions, dependencies and platforms change.

For Signal users, the news is additional assurance about selected cryptographic implementation properties, not a reason to stop updating devices or practising normal account security. For software developers, the larger prospect is more interesting: AI-generated work could eventually be accompanied by machine-checkable evidence for the parts of a system where a wrong answer is unacceptable.