Google DeepMind uses AI to mathematically verify key parts of Signal

Google DeepMind has formally verified several core components of the Signal encrypted messaging protocol using mathematical proof methods. The effort took about four weeks to complete. The project suggests that artificial intelligence could make formal verification, a rigorous method of proving software correct, much more practical to apply. Formal verification has traditionally been costly and labor-intensive, limiting its use to a small set of critical systems. The result points to a possible path for applying such checks to security-sensitive software more broadly.