DeepMind Checks Signal Code with AI

Google DeepMind claims to have formally verified, using AI, elements of the encryption code of Signal. The team states that they conducted the operation in one month and presents it as the first formal verification of a widely deployed cryptographic protocol at the implementation level. The scope remains partial, with no plans for a consumer product, but researchers mention potential openings towards other critical systems.

DeepMind Claims a World First and Clarifies the Scope

Researchers at Google DeepMind assert that they have used AI to formally verify, for the first time, a widely deployed cryptographic protocol at this level. They specify that this is also the first formal verification of the implementation of such a protocol, regardless of the method used. The team indicates that they completed this work in one month, whereas experts would typically require several years. DeepMind emphasizes that only a portion of Signal's code has been verified and views this result as a step towards enhanced security infrastructure, in a context where AI is transforming cybersecurity. No consumer product launch is planned at this stage. The researchers express openness to publishing their code as open source to support other formal verification initiatives and believe that verifying the core cryptography of Signal could serve as a foundation for securing other essential systems, such as medical device firmware or electrical grid software.

A Hybrid Method with AlphaProof Code and Gemini Carbon

The researchers used AlphaProof Code and relied on previous verifications conducted by the Signal Foundation. The task was divided into two parts: humans collaborated with agents to define the properties to be demonstrated, and then several agents, based on Gemini Carbon, conducted the proofs. These agents also audited the results and flagged areas for human review, which concerned only 1% of the codebase, according to the researchers. To test the approach's ability to distinguish correct code from faulty code, two already fixed bugs in Signal were submitted to AlphaProof Code, which produced correct proofs.

What This Changes for Signal and Encrypted Messaging

Parts of Signal's encryption code have been formally verified, and mathematical proofs have established that certain components function as intended, without errors, according to the team. The researchers believe that this automatic proof applied to Signal's core protocol enhances their confidence in the code's privacy guarantees. WhatsApp and Google Messages use the same encryption, which extends the implications of these results to other encrypted messaging services.

Formal Verification Tested by AI and Cybersecurity

The development of formal proofs has historically been difficult and time-consuming, often limiting their application to production software. AlphaProof Code is presented as a breakthrough towards more robust security verifications, as the manual creation of these proofs remains very labor-intensive. AI is described as an ambivalent factor for cybersecurity: it poses both a significant risk and a powerful tool. The year 2026 was marked by numerous AI-related security incidents, often involving agents, while companies like Anthropic, Google, and OpenAI are developing models dedicated to cybersecurity, including Anthropic's Claude Mythos. More broadly, recent advances attributed to AI in mathematics and large-scale computing capabilities suggest an acceleration of tasks that were once very manual. This dynamic is seen as reassuring in light of vulnerabilities recently discovered by AI systems in software, as many communications rely on Signal's cryptography.