Google DeepMind introduces AlphaProof Code with machine-checked libsignal proofs

Google DeepMind introduced AlphaProof Code and released its formal-verification artifacts on Nov. 10, including a technical paper and Lean proofs for specified security properties of compiled libsignal code. The paper’s machine-checked theorems connect an examined machine-code build to guarantees for message confidentiality and authenticity, forward secrecy, post-compromise security and handshake secrecy under its models and assumptions.

The technical paper describes a stock-rustc AArch64 Linux build of unmodified libsignal-protocol v0.105.4 with spqr v1.6.0, linked into a small command-line harness. Its theorems address one-to-one PQXDH setup and Triple Ratchet initialization, sending and receiving. The result does not prove that Signal as a whole is secure.

The work does not cover the Signal mobile apps, group messaging, sealed sender, server-side protocols, key generation or side channels. Several cases excluded by the models also remain outside the proved scope.

AlphaProof Code is a human-guided, multi-agent proof framework. People approve specifications written in Lean, prover agents generate proofs, and a gatekeeper accepts a result only after Lean’s kernel and a comparator check it against the approved specification. The approved specification and Lean’s kernel therefore remain inside the trusted base.

The authors report about 6.5 million lines of machine-checked Lean proof code. That code rests on roughly 18,000 lines of trusted definitions and statements, plus about 8,000 lines of AArch64 semantics and trusted symbol names. The result also relies on cryptographic assumptions or idealizations and contracts for cryptographic primitives, two output functions and several library routines.

The released work has symbolic and computational components. Its symbolic proof includes handshake secrecy against a future quantum attacker, while the computational theorem is classical. The ratchet theorems do not establish SPQR’s intended post-quantum healing property.

Google DeepMind describes the project as the first machine-code-level verification to connect protocol security guarantees to an unmodified, widely deployed cryptographic protocol implementation. That comparative claim has not been independently established. Google DeepMind published the specifications and proofs and made the code repository available, but none of the reviewed sources documents an independent party rebuilding the target binary and rerunning the complete Lean checks.

The paper says a five-person team completed the proof work over four weeks, with agents running in parallel on symbolic and computational proofs. The researchers also reintroduced two previously fixed libsignal bugs and produced complete Lean proofs that the altered binaries violated the symbolic security theorem.