AI agents produced machine-checked proofs that Signal's encryption code meets its security specifications

DeepMind says its new AlphaProof Code agents produced machine-checked, implementation-level proofs that Signal's core cryptographic implementation meets the security properties the team specified. DeepMind published the announcement on its blog on 10 November 2026 and has open-sourced the verification artifacts on GitHub.

AlphaProof Code is a multi-LLM agentic framework that combines human experts and groups of AI agents to translate security goals into formal specifications and then prove that compiled code implements those specifications. DeepMind says agents powered by Gemini Carbon generated over six million lines of Lean formal proofs, and that human experts reviewed every specification the agents used.

The company reports the full verification of Signal's core cryptographic implementation took four weeks. Agents audited their own proofs and flagged about 1% of the codebase for human review; Lean, the proof assistant used, mechanically checked the rest. To test the system, DeepMind reintroduced two previously fixed, real bugs into an isolated Signal build and says AlphaProof Code produced machine-checked proofs that the buggy versions were insecure.

Formal verification of cryptographic systems is not new, but earlier work usually stayed at the design level. The 2016 academic analysis by Cohn-Gordon and colleagues produced formal, design-level proofs of the Signal protocol itself; that work analysed the protocol and proved properties about the design rather than the exact compiled implementation running on devices. High-assurance projects such as the seL4 microkernel have used implementation-level verification for system software. DeepMind says this is the first time AI has been used to verify the implementation of a widely deployed messaging protocol at this depth.

The distinction matters because a proof that a protocol design is secure does not automatically guarantee that a particular software implementation of that design is free of bugs or that the compiled binaries preserve the design's properties. DeepMind says its agents translated live code into Lean theorems and proved that the implementation satisfies the formal specifications, narrowing the gap where real-world vulnerabilities often appear.

DeepMind says the result could affect operators and governments that rely on secure messaging for sensitive services. Implementation-level verification offers a higher assurance for businesses, governments and critical infrastructure - for example, medical device firmware or power grid software - where bugs could have severe consequences. Because DeepMind has open-sourced the proof artifacts, security teams, researchers and developers can inspect the formal statements and the Lean proofs themselves.

What this could mean in practice depends on how these proofs are adopted. If implementation-level verification or similar audits become part of development and review practices, organisations and auditors could use machine-checked proofs as part of compliance checks or incident investigations. Wider use will depend on tooling, compute and verification workflows, which DeepMind says remain work in progress.

A practical next step for security teams, auditors and researchers is to inspect DeepMind's open repository on GitHub, where the Lean artifacts produced are available: formal specifications, Lean theorems and machine-checked proofs, including the millions of lines of Lean the project generated. Teams can replay the proofs, review the formal statements used, and consider how those artifacts map to their own threat models and audit requirements.

DeepMind's write-up also flags the limits and next steps. The company says scaling these techniques will require further research and engineering, and it points to pairing formal verification with automated defence tools such as CodeMender to respond to AI-driven threats. The agents still ask humans to resolve about 1% of issues, and DeepMind notes that broader adoption will need work on tooling, compute and verification workflows.

The DeepMind blog credits the main researchers on the project:

• Swarat Chaudhuri
• Andrew Ferraiuolo
• Anton Kovsharov
• Tej Chajed
• Sam Schlesinger
• Karn Seth
• Jonathan Katz
• Charles Sutton
• Pushmeet Kohli

DeepMind's write-up links to a technical paper and the open repository of machine-checked Lean artifacts for people who want to inspect or adapt them for other codebases.

Readers should note that DeepMind frames this work as an important step rather than a finished solution: it demonstrates that agentic theorem proving can complete a large, scoped verification task quickly, but wider use across diverse codebases and sustained integration into development and audit pipelines will take more research and engineering effort.

Sources: DeepMind blog and the project's GitHub repository.

Newzroom dot Africa has reached out to Google DeepMind, Signal and GSMA for comment and is awaiting a response. This story will be updated when they respond.

Source: Google DeepMind