Google DeepMind's AlphaProof Code Verifies Signal's Security

How the process worked

The researchers first worked with various models to turn Signal's security goals into a human-reviewed mathematical specification. Gemini Carbon agents then generated Lean code proving the libsignal implementation correct. The agents produced 6.5 million lines of Lean, after which an auditing pass flagged parts that needed human review.

The result is theoretical: it assumes perfect cryptography and does not guarantee the computational secrecy of bytes. Still, it is a meaningful assertion of correctness, and a step toward a challenge the Beneficial AI Foundation issued in April to formally verify the Signal protocol and app with Lean.

Why it matters

Formal verification has historically demanded heroic effort: verifying the seL4 microkernel took 20 person-years, and building the verified CompCert C compiler took six years. The Signal work took four weeks for a team of five, plus "quite a few tokens", according to the researchers' paper.

Swarat Chaudhuri, a research scientist at Google DeepMind, said the hard part has shifted. Verification itself now scales, so the question becomes what to verify, a process that remains human-in-the-loop. He pointed to the rise of offensive AI capabilities and the many insecure systems that will be exploited.

The next step, he said, is applying the approach during software design, for code in general and not only cryptographic protocols, alongside the related AlphaProof Nexus project focused on mathematics. "The next frontier is not going to be proof but specification," he said.