Google DeepMind just mathematically verified key parts of Signal

Google DeepMind researchers used agentic AI to mathematically verify key parts of the Signal protocol's cryptography in a four-week project, providing independent validation of the security of widely used platforms like Signal, Google Messages, and WhatsApp. The project demonstrated Google DeepMind's formal verification capabilities using the AlphaProof Code framework, a new AI tool that can significantly cut down the time required for software verification. The analysis did not find any new vulnerabilities in the Signal protocol, but it was limited in scope and the researchers emphasized the need for further work to scale up formal verification to all software. The project suggests that AI-aided formal verification could make the process more practical, but its effectiveness for widespread use remains unclear.