According to WIRED, Google DeepMind researchers used a new AI framework called AlphaProof Code to formally verify, in four weeks, that the Signal protocol works as expected. The analysis found no new vulnerabilities in the parts of the protocol examined, but correctly identified an issue in an older version of Signal containing a known, longstanding vulnerability, showing that the protocol could not pass formal verification. DeepMind research scientist Swarat Chaudhuri said this is a milestone in scaling formal verification to software targets around the world, but there is still a long way to go. The researchers also published the specifications and proofs developed for the analysis to help with other formal verification efforts.