DeepMind agents formally verify Signal protocol properties in Lean

DeepMind’s AlphaProof Code checked Signal’s PQXDH and Triple Ratchet, found no new flaws, and flagged known bugs.

Google DeepMind used AlphaProof Code, a multi-agent framework, to formally verify security properties of Signal’s libsignal implementation, including the post-quantum PQXDH handshake and Triple Ratchet. Human experts set a Lean specification; Gemini Carbon agents generated proofs that the Lean kernel checked, covering forward secrecy, authentication, post-compromise security, and handshake secrecy. The four-week effort by five people produced about 6.5 million lines of Lean; researchers reviewed roughly one percent and say the result assumes perfect cryptography and is not a byte-level secrecy guarantee. WIRED reports no new vulnerabilities in the portions examined and that known bugs in older versions were flagged; DeepMind says reintroduced copies of two previously fixed bugs were proved insecure. Artifacts and a paper are being released. The work did not cover the entire Signal app.