DeepMind Uses AI Tools to Formally Verify the Security of the Signal Protocol

According to WIRED, Google DeepMind researchers used a new AI framework called AlphaProof Code to formally verify that the Signal protocol operates as intended within four weeks. The analysis did not uncover new vulnerabilities in the reviewed sections of the protocol, but it correctly identified issues on an older version of Signal containing known legacy vulnerabilities, demonstrating that the protocol fails formal verification.

DeepMind research scientist Swarat Chaudhuri noted that this represents a milestone toward extending formal verification to all software targets globally, though there is still a long way to go. The researchers also published the specifications and proofs developed for this analysis to support other formal verification initiatives.