Google DeepMind said on Nov. 10 that teams of AI agents had mathematically proved key security properties of libsignal, the reference implementation of the Signal protocol, at the level of its compiled machine code. The lab built the proofs with a new framework it calls AlphaProof Code and described the work in a blog post and a technical paper published the same day.
According to the paper, the agents generated about 6.5 million lines of proof code in Lean, whose kernel checks each proof. Those proofs rest on roughly 26,000 lines of trusted material, made up of about 18,000 lines of specifications plus about 8,000 lines describing the AArch64 processor and the program's symbol names. DeepMind wrote that this is the first time AI has been used to formally verify a widely deployed cryptographic protocol at this depth, and the first time the implementation of such a protocol has been formally verified by any method.
What was proved
The paper says the work covers Signal's post-quantum PQXDH handshake and its Triple Ratchet for one-to-one sessions, as implemented in libsignal v0.105.4. The proofs establish forward secrecy, authentication, post-compromise security and handshake secrecy, in both the symbolic and the computational models of protocol security.
The researchers compiled the unmodified Rust code with the standard rustc compiler into an AArch64 Linux executable, then loaded that executable into Lean alongside a formal model of the processor. Because the theorems are about machine code, the paper says, the compiler itself does not have to be trusted. The processor model covers 467 instructions and 31 system calls in 7,578 lines of Lean.
The scope has limits. The paper leaves group messaging for future work, and it specifies the cryptographic primitives and some library routines by contracts rather than verifying them. The processor model also does not handle threads or dynamic linking, among other features.
How the agents split the work
DeepMind describes AlphaProof Code as a framework in which human experts decide what to prove and agents do the proving. The paper says the specifications came out of "an intense back-and-forth between humans and agents powered by Gemini 4 Carbon and Claude Opus 5.5." The proofs themselves "were produced entirely by agent teams powered by Gemini 4 Carbon," and none of the authors wrote any proof code, according to the paper.
A gatekeeper agent accepts a proof only if Lean's kernel checks it and a separate tool confirms that it proves exactly a held-out copy of the approved specification. To cope with limited context windows, an orchestrator groups proof workers under team leads that send it short summaries of open obligations and blockers. DeepMind's blog says the agents flagged about 1 percent of the codebase for a second look by a human.
The paper says a team of five did the proof work over four weeks, each running agents nonstop on a workstation, a task DeepMind's blog says has historically taken expert teams years.
Testing the specifications
To check that the specifications would catch real flaws, the researchers reintroduced two previously fixed libsignal bugs and proved in Lean that the resulting binaries violate the symbolic security theorems. Writing specifications against real code also exposed problems in earlier research.
The team recorded every place its Lean statements depart from the reference papers or from libsignal, with over 200 entries for the computational proofs and about 35 for the symbolic ones. The paper says most are routine, but some are errors in the published analyses that had to be repaired before the proofs could go through. Fifteen of them are gaps or bugs in the computational analysis of the Double Ratchet, such as missing hypotheses.
Signal Chief Technology Officer Ehren Kret said in DeepMind's announcement that "using AI agents to translate live code into valid Lean theorems is a major breakthrough." He added that verifying the implementation "gives us even greater confidence in our code's privacy guarantees."
DeepMind has published the Lean development on GitHub. The lab said it sees the work as groundwork for verifying other critical systems, naming medical device firmware and power grid software, and that scaling the techniques "requires continued research."
Source: Google DeepMind Blog, “Introducing AlphaProof Code”
Additional sources: Google DeepMind (paper), “AlphaProof Code: Verifying Signal's Security at the Machine-Code Level”; GitHub, “google-deepmind/code-verification”
