Google DeepMind announced on November 10 that it had formally verified, with the help of artificial intelligence agents, key security properties of the Signal encryption protocol, the same one that protects WhatsApp and Google Messages. The work, carried out by five people in four weeks with a tool called AlphaProof Code, would have taken human experts years. But it does not guarantee that the Signal app is flawless, and its cost remains unknown.
What DeepMind demonstrated
Formal verification does not mean testing software on thousands of cases: it establishes, through a machine-checked mathematical proof, that a property holds in every situation covered by the model. According to The Register, the team focused on two building blocks of the protocol: PQXDH, the handshake designed to withstand future quantum computers, and the Triple Ratchet, which renews keys as messages are exchanged.
The proven properties go to the heart of Signal’s promise: forward secrecy (an old message stays protected even if a key leaks later), authentication of the parties, recovery after a device is temporarily compromised, and the secrecy of the initial exchange. The researchers claim a first: an AI reportedly helped build a proof that links these theoretical guarantees to a cryptographic implementation actually in use, down to the machine-code level.
How AlphaProof Code works
The tool is a multi-agent system. Cryptography experts define what needs to be proven; several models translate these goals into a specification that the experts review, then agents based on Gemini Carbon, Google’s model, write the proofs in Lean, a proof assistant whose kernel checks every step. The Register mentions around 6.5 million lines of generated Lean, followed by an automated audit flagging the passages to be reviewed by a human. According to DeepMind’s blog, which speaks of more than six million lines, this human review covered only about 1% of the code.
To make sure the tool does not validate just anything, the team ran a backward test. According to 9to5Mac, older versions of Signal carrying known vulnerabilities were indeed flagged as failing verification. DeepMind says two real bugs, since fixed, were reintroduced into an isolated copy of the code: in both cases, the system produced a machine-checked proof that the faulty version was not secure.
Researcher Swarat Chaudhuri, of DeepMind and the University of Texas at Austin, stresses the role of humans. Quoted by The Register, he believes the next challenge will no longer be the proof but the specification, that is, the exact definition of what the software must guarantee. On Signal’s side, its chief technology officer Ehren Kret, quoted by DeepMind, calls it a “major breakthrough” that agents can translate production code into valid Lean theorems, as earlier formal verifications had focused on smaller portions of the code.
What this work does not prove
9to5Mac’s headline, which speaks of encryption “proven secure”, goes further than the substance. The proof covers the protocol and some of its guarantees, not the entire Signal app, nor the way WhatsApp or Google Messages have integrated it. The Register also points out that the result assumes perfect cryptography: it says nothing about the mathematical strength of the algorithms themselves.
Then there is the question of scale. Neither the computing cost nor the exact volume of resources consumed has been published. Swarat Chaudhuri himself acknowledges, according to 9to5Mac, that there is still “a long distance to go” before the method can be applied to all software. DeepMind, however, says it is releasing its verification artifacts openly, along with a technical paper. According to The Register, this work also brings closer a challenge set in April by the Beneficial AI Foundation: formally verifying the Signal protocol and app in Lean.
Why it matters
Famous verification projects have required years of work: The Register cites the seL4 microkernel, which took some twenty person-years. If agents can cut that time to a few weeks, formal verification could move out of the lab to cover critical components such as encryption libraries, messaging protocols or embedded systems. For businesses, the immediate lesson is more modest: a proof is only as good as its specification, and human expertise remains the decisive link.
Frequently asked questions
Is Signal now impossible to hack?
No. DeepMind’s work proves specific properties of the protocol, under the assumption of perfect cryptography. The app, the phone and user errors remain possible points of attack.
Is WhatsApp affected?
WhatsApp and Google Messages use the Signal protocol, so the guarantees demonstrated for the protocol apply to them. Their own implementations, however, were not verified in this work.
What is Lean?
Lean is a proof assistant: software that mechanically checks every step of a proof. A proof accepted by its kernel does not depend on trusting the AI that wrote it.
Sources
- Google DeepMind melds humans and AI agents to vet Signal's secure messaging techniques — The Register, 2026-11-10
- Google DeepMind analysis proves Signal and WhatsApp encryption is secure — 9to5Mac, 2026-11-10
- Introducing AlphaProof Code — Google DeepMind (official blog), 2026-11-10