DeepMind AI Agents Verify Signal's Encryption Code

Google’s artificial intelligence (AI) division, DeepMind, claims to have proven mathematically using AI that the heart of the encryption code used in the encrypted messaging service Signal is secure. This was done by training AI agents to convert the code into around six million lines of Lean, a formal verification programming language that ensures correctness of software. Only approximately one percent of these lines were validated manually by human experts, while the remainder was done automatically. This process took just four weeks, compared to the years it would take a team of experts to carry out such a task. As a proof of concept, the researchers introduced two real-world bugs that had previously been removed from the code of a version of Signal, and the AI agents were able to identify both instances as being insecure.

In the past, formal verification has been time consuming and costly, meaning that it has not been practical for most companies to use on real, deployed software. However, if AI agents are able to replicate years of work in just a few weeks, while requiring little manual input, then it may be possible to apply this technique to other important pieces of code, such as those used in medical equipment or power grids, where a single mistake can impact large numbers of people.