[DeepMind Formalizes Signal Protocol Security with AI Tool] According to WIRED, Google DeepMind researchers used a new AI framework called AlphaProof Code to formally verify that the Signal protocol functions as expected within four weeks. The analysis did not find any new vulnerabilities in the checked parts of the protocol, but correctly identified problems on older versions of Signal containing known vulnerabilities, showing that the protocol failed formal verification. DeepMind research scientist Swarat Chaudhuri stated that this is a milestone in extending formal verification to all software targets globally, but there is still a long way to go. The researchers also released the specifications and proofs developed for this analysis to assist other formal verification efforts.