Google DeepMind formally verifies part of Signal protocol — Ars Technica

Google DeepMind has mathematically confirmed a number of key cryptographic guarantees of the Signal protocol using agentic artificial intelligence. The four-week research project was demonstrative in nature and used the new AlphaProof Code AI framework, Ars Technica reports.

Verification of cryptographic properties

Formal verification is a mathematical check of whether software meets specified properties and has no critical vulnerabilities. Before the advent of AI, this process took a great deal of time: specialists had to describe the program's properties, convert them into formulas, and construct a mathematical proof.

According to the publication, agentic AI can significantly reduce the time needed to create such a proof. At the same time, DeepMind's research was limited in scope: it did not cover the entire Signal mobile app, but concerned individual parts of the protocol.

During the analysis, the researchers found no new vulnerabilities in the verified parts of the Signal protocol. When AlphaProof Code was applied to older versions of Signal with known and long-fixed issues, the system correctly identified these vulnerabilities and showed that the protocol could not be formally verified while they were present.

More current news is available on the UA.News Telegram channel Telegram.

Limits of the research

DeepMind emphasized that the result is only one stage of broader work. Scaling AI-assisted formal verification to large volumes of program code and all software systems still requires further development.

The researchers also noted that earlier work by the Signal Foundation on formal verification of individual parts of the code contributed to faster analysis. DeepMind is publishing the specification and proof created for the Signal analysis so they can be used in other formal verification research.

The company conducted the project free of charge as a research project, without disclosing its cost. Google also did not say whether it plans to launch a commercial product or service for formal verification.

DeepMind described the approach as collaboration between humans and AI: agents can assist at various stages and correct their own work, but human input and review are provided at key stages.