DeepMind AI formally verifies key security features of signal protocol

Researchers at Google DeepMind utilized agentic AI to mathematically confirm several critical cryptographic assurances within the Signal protocol, marking a significant achievement for both cryptography and artificial intelligence. This proof-of-concept project was completed in just four weeks and validates the security underpinning communications on platforms like Signal, Google Messages, and WhatsApp, demonstrating DeepMind's capabilities with its AlphaProof Code framework. While the analysis found no new weaknesses in the examined parts of the protocol, the tool successfully flagged known vulnerabilities in older Signal versions. Ehren Kret, Signal's chief technology officer, noted that DeepMind's approach allows for significant expansion beyond prior verification efforts. Pushmeet Kohli, chief scientist at Google Cloud and DeepMind's vice president of research, suggested that such verification could allow critical services, like banks, to prove their code's correctness. Swarat Chaudhuri, a DeepMind research scientist, emphasized that scaling this to all global software is a long-term goal, stressing a preference for a human-AI collaboration process rather than fully autonomous AI generation. The researchers are making their specification and proof public to assist the broader field of formal verification.