Google DeepMind researchers have completed a formal verification of Signal’s messaging security, marking what they claim is the first time AI has helped devise a proof that links protocol-level security guarantees to a widely used cryptographic implementation. They did so using AlphaProof Code, a multi-agent framework for formal software specification and verification. AlphaProof Code relies on a human-guided agent that writes a Lean specification, assesses machine code semantics, and crafts an agent-authored proof that the Lean kernel checks against the specification. In this instance, AlphaProof Code verified Signal’s post-quantum PQXDH handshake and Triple Ratchet , thereby validating the design of libsignal ‘s forward secrecy, authentication, post-compromise security, and handshake secrecy. In so doing, the Google/DeepMind team – Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, Charles Sutton, and Pushmeet Kohli – has taken a step toward a challenge the Beneficial AI Foundation issued in April to formally verify the Signal protocol and Signal app with Lean. The AlphaProof Code process involves working with various models to turn Signal’s security goals into a human-reviewed mathematical specification. Based on this spec, the researchers assigned Gemini Carbon agents to generate Lean code proving the correctness of the libsignal implementation. After the agents generated 6. 5 million lines of Lean code, they undertook an auditing pass and flagged bits that required human review. The result is theoretical in that it assumes perfect cryptography and doesn’t guarantee the computational secrecy of bytes. But it’s still a meaningful assertion of correctness. "It’s a system that is fundamentally built for human AI collaboration," said Swarat Chaudhuri, research scientist at Google DeepMind and a professor at the University of Texas at Austin, in an interview with The Register …