DeepMind’s AlphaProof Code Formally Verifies Signal Protocol in Four Weeks

Cointime update: Google DeepMind researchers used a new AI framework called AlphaProof Code to formally verify that the Signal protocol operates as intended, completing the analysis in four weeks. The work found no new vulnerabilities in the checked portions of the protocol, but correctly identified known issues in an older Signal version and showed that version fails formal verification. DeepMind research scientist Swarat Chaudhuri called it a milestone toward scaling formal verification to all software worldwide, while noting much work remains.