Google DeepMind said Tuesday that researchers using a new agentic system, AlphaProof Code, formally verified key security properties of the code behind the Signal protocol, the lab announced. WIRED and The Register also reported the work.
Why it matters: DeepMind called it the first time AI has formally verified 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. The work does not formally verify the entire Signal app, the researchers and WIRED both stressed.
Human experts worked with models to write mathematical specifications, which people then reviewed. Agents powered by Gemini Carbon generated more than six million lines of Lean, a proof language, in a process DeepMind said took four weeks, a task that has historically taken expert teams years. Agents then flagged about 1% of the work for a second human look; the Lean kernel checks the rest. The Register said the proofs covered Signal’s post-quantum PQXDH handshake and Triple Ratchet in libsignal, including forward secrecy, authentication, post-compromise security and handshake secrecy, while assuming perfect cryptography.
To test whether the system could distinguish good code from bad, researchers reintroduced two previously fixed bugs into an isolated copy of the code; in both cases it produced a machine-checked proof that the buggy version was insecure. Signal CTO Ehren Kret said in a statement to WIRED that the approach “enables significant expansion” on earlier verification work and “gives us even greater confidence in our code’s privacy guarantees.” DeepMind research scientist Swarat Chaudhuri told WIRED there is “a long distance to go before we are able to scale this to all the software of the world.”