DeepMind uses AI agents and humans to formally verify Signal's encryption

[Yasmin56]

AI has helped prove that one of the world's most widely used secure messaging systems does what it promises. The Register reports that Google DeepMind's AlphaProof Code multi agent framework has verified Signal's post quantum PQXDH handshake and Triple Ratchet in the libsignal library

The article calls it the first AI assisted proof linking protocol guarantees to a widely used cryptographic implementation. Gemini Carbon agents wrote 6.5 million lines of Lean, with an audit pass flagging sections for human review

The work took a team of five people four weeks. For comparison, verifying the seL4 microkernel took around 20 person years

The proof assumes perfect cryptography, so it checks the protocol logic rather than the underlying maths. DeepMind research scientist Swarat Chaudhuri said the next frontier is not proof but specification, and that the team does not have the last word by any means, with the work answering the Beneficial AI Foundation's April challenge to verify Signal in Lean

Cutting formal verification from years to weeks could make it practical for far more software, which would be great for security. Signal protects millions of conversations, so extra confidence in its code matters. Chaudhuri's point about specification is important, because a proof is only as good as the question it answers

Would you trust software more if it came with a formal proof? And which other software should be verified like this?

Google DeepMind melds humans and AI agents to vet Signalwww.theregister.com