The proofs target the compiled binary
Google DeepMind introduced AlphaProof Code on November 10, together with a technical paper and the GitHub repository google-deepmind/code-verification. The verification target is libsignal v0.105.4 (with spqr v1.6.0), the reference implementation of the Signal protocol, limited to one-to-one sessions and covering the post-quantum PQXDH handshake and the Triple Ratchet. Rather than stopping at the protocol design, the team compiled an AArch64 Linux executable with stock rustc 1.98.1 and proved that this binary provides forward secrecy, authentication, post-compromise security and handshake secrecy. DeepMind's blog post says this is the first time the implementation of a widely deployed protocol like this has been formally verified; the paper phrases it more narrowly, saying the work rigorously connects symbolic-level analysis to the assembly implementation for the first time.
Humans set the specs, agents write the proofs
Specifications were worked out in a back-and-forth between researchers and agents powered by Gemini 4 Carbon and Claude Opus 5.5, with humans deciding what to prove and giving final approval. The proofs were produced entirely by agent teams powered by Gemini 4 Carbon, and none of the authors wrote proof code. A typical run used 40 to 80 agents on one machine for 24 to 72 hours. A team of five worked for four weeks and produced about 6.5 million lines of Lean proof; the part a reader must read and trust is about 26,000 lines of specifications and AArch64 semantics. DeepMind says the agents flagged only about 1% of the code for human review. To check that the system can tell flawed code apart, the team reintroduced two previously fixed libsignal bugs and proved that the resulting binaries violate the security theorems. Signal CTO Ehren Kret says in the blog post that the approach significantly expands on earlier formal verification work.
What is not covered
No new vulnerabilities were reported. The paper's trusted base includes the Lean kernel, the AArch64 semantics, the specifications and contracts for 37 hooked routines; cryptographic primitives are idealized or assumed secure, and the computational-model proof covers classical attackers only. Multi-device state, group messaging, threads and dynamic linking are out of scope. The blog post says only that the verification artifacts are being open-sourced; it does not say whether the AlphaProof Code framework itself will be made available.
via: Google DeepMind Blog: AlphaProof Code: a breakthrough in verifying complex software at depth, Technical paper: AlphaProof Code: Verifying Signal's Security at the Machine-Code Level, GitHub: google-deepmind/code-verification