AI Agents Prove Signal Code at Machine Level

Google DeepMind said Nov. 10 that AI agents built on its Gemini models produced machine-checked proofs that the compiled code of libsignal, the reference implementation of the Signal encryption protocol, delivers key security guarantees. The company called it the first time the implementation of a widely deployed protocol of this kind has been formally verified by any method, with or without AI.

Key takeaways

• DeepMind's new AlphaProof Code framework generated about 6.5 million lines of Lean proof for Signal's compiled code, according to the technical paper.
• Humans wrote and approved the specifications; the agents did the proofs, and the verification took four weeks.
• The proofs cover one-to-one sessions only. Group messaging and the full Signal apps are outside the result.

What AlphaProof Code verified in Signal

The target was libsignal v0.105.4, compiled unmodified with the standard Rust compiler into AArch64 Linux machine code. The proofs cover Signal's post-quantum PQXDH handshake and its Triple Ratchet, establishing forward secrecy, authentication, post-compromise security and handshake secrecy, the technical paper says.

Most earlier work on Signal checked abstract models or rewritten versions of the protocol. DeepMind's researchers said real-world bugs often hide in the gap between design and implementation, which is why they proved properties directly about the binary.

How the AI agents split the work

Researchers first worked with several models to turn Signal's security goals into formal specifications, with human experts reviewing every one, according to DeepMind's blog post. Agents powered by Gemini Carbon then wrote the proofs in Lean, a language whose kernel checks every step.

The paper says a typical proof team had 40 to 80 agents running on a single machine for 24 to 72 hours. A gatekeeper agent accepted a proof only if Lean's kernel checked it against a held-out copy of the human-approved specification. The agents also flagged about 1% of the codebase for a second human look, DeepMind said.

The trusted base that readers must accept is about 26,000 lines: roughly 18,000 lines of specification and about 8,000 lines of AArch64 semantics. The semantics model covers 467 instructions and 31 system calls.

Testing the proofs against real Signal bugs

To check that the specifications catch real mistakes, the team reintroduced two previously fixed libsignal bugs into an isolated build. In both cases the system produced a machine-checked proof that the buggy binary violated the security theorem.

"Using AI agents to translate live code into valid Lean theorems is a major breakthrough," Signal Chief Technology Officer Ehren Kret said in DeepMind's announcement.

Why formal verification has been so costly

Formal verification has long been limited by labor. The paper notes the seL4 microkernel took 20 person-years to verify and the CompCert C compiler took six. Both were written with verification in mind, unlike production code such as libsignal.

The work adds to a run of AI-assisted proof efforts this fall, including Microsoft Research's PDD Kit for agent-written Rust, which AI Newsway covered on Nov. 9.

Limits of the Signal proof

The guarantees rest on the approved specifications, Lean's kernel, the machine-code semantics and assumptions about cryptographic primitives, which are modeled as trusted contracts. The semantics does not model threads, signals or dynamic linking. Unite.AI, reviewing the paper, noted that key generation, side channels and multi-device state also fall outside the scenario.

What's next

DeepMind has open-sourced its specifications and proofs on GitHub so outside experts can recheck them. The researchers list group messaging as future work and say the approach could extend to systems such as medical device firmware and power grid software.

FAQ

Does this mean Signal has no bugs? No. It proves specific security properties of one compiled build under stated assumptions. Parts outside the specification are not covered.

Do Signal users need to do anything? No. The work verifies existing code and does not change the app.

Can others check the proofs? Yes. DeepMind released the Lean development and instructions for rebuilding and checking it.

References

• Formal Verification of Signal's Protocol with Gemini — Google DeepMind (Nov. 10, 2026)
• AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — Google DeepMind and Google (Nov. 10, 2026)
• GitHub - google-deepmind/code-verification: Verifying Signal's security at the machine-code level — Google DeepMind (Apache 2.0)
• Google DeepMind Uses AI Agents to Verify Signal's Core Machine Code — Unite.AI (Nov. 10, 2026)