Google DeepMind researchers said they have used AI agents to produce a machine-checked mathematical proof that the encryption code behind Signal's messaging protocol behaves as designed, a result the lab frames as an early step toward software whose security can be demonstrated rather than merely tested.
The project, completed in about four weeks by a five-person team, applied a new multi-agent framework called AlphaProof Code to libsignal, the implementation of the Signal protocol used by the Signal app, Google Messages and WhatsApp. The framework relies on a human-guided agent that writes a Lean specification, interprets machine-code semantics and drafts proofs that the Lean kernel then checks against that specification. In this case the proof covered Signal's post-quantum PQXDH handshake and Triple Ratchet, validating the design's forward secrecy, authentication, post-compromise security and handshake secrecy.
"It's a system that is fundamentally built for human AI collaboration," Swarat Chaudhuri, a research scientist at Google DeepMind and a professor at the University of Texas at Austin, said in an interview.
The work is significant on two fronts. It adds independent validation of cryptography that protects a large share of the world's private communications, and it shows how agentic AI can compress one of the most labor-intensive tasks in software security. Earlier formal-verification efforts were measured in person-years: proving the seL4 microkernel correct took roughly 20, while building the verified CompCert C compiler took six years.
According to the researchers, the agents generated millions of lines of Lean code, followed by an auditing pass that flagged sections needing human review. In a test of the system, the team reintroduced two bugs that had previously been found and fixed in Signal's code. In both cases the framework produced proofs showing the altered software was insecure, and it likewise failed to verify older Signal versions containing known vulnerabilities. The DeepMind analysis did not turn up any new flaws in the portions of the protocol it examined.
"While prior formal verification focused on smaller portions of the code, Google DeepMind's approach enables significant expansion," Signal chief technology officer Ehren Kret said in a statement. "As AI-driven security threats grow, rigorously verifying the Signal protocol implementation gives us even greater confidence in our code's privacy guarantees."
The effort is also a step toward a challenge issued in April by the Beneficial AI Foundation to formally verify the Signal protocol and app using Lean. The researchers are releasing the specification and proof they developed to support further verification work.
The limits are worth stating plainly. The proof assumes perfect cryptography and does not establish the computational secrecy of individual bytes, and it does not cover the entire Signal mobile app. The Signal Foundation had already done formal-verification work on smaller portions of the code, giving the DeepMind team a head start.
"We are very excited by this result, but there is a long distance to go before we are able to scale this to all the software of the world, and we want to do that," Chaudhuri said.
DeepMind's broader argument is that security flaws usually arise because code on a device does not behave the way its authors intended. Formal verification attacks that gap directly by proving properties about the actual machine code rather than relying on testing to surface failures. Chaudhuri said the same approach could eventually help developers show that software resists common classes of weakness, including the memory-safety bugs attackers exploit routinely.
"If you can now verify the correctness of these implementations, then you can rest easy," said Pushmeet Kohli, chief scientist at Google Cloud and DeepMind's vice president of research. "You can imagine banks, imagine all those other companies who rely on assurances and who worry about bugs who could now say, 'I can prove these properties.'"
The team describes its central methodological advance as a human-in-the-loop process in which agents contribute and self-correct at nearly every stage while people define what must be proven and review key outputs. Chaudhuri said the hard part in formal methods has shifted: verification itself is becoming tractable, and the open question is now specification, or deciding which properties matter and how to write them down.
"We don't want this sort of vibe world where AI is generating the goals and AI is generating the proofs and basically taking tests that are self-written," he said. "There's a middle ground."
Google has not said whether it will sell a formal-verification product or service, and it declined to disclose what the Signal analysis cost. For now the work remains a research project. The company is weighing how to fold the technology into AI coding agents and development workflows, and how to combine it with existing vulnerability-hunting and patching efforts such as Project Zero and CodeMender. A related DeepMind project, AlphaProof Nexus, is focused on mathematics.
The result lands as AI-assisted formal verification draws growing attention from security teams, though its practicality and cost at the scale of large codebases remain unresolved. For the cryptography community, the immediate takeaway is narrower: a widely deployed protocol has now been checked against its stated security goals at the machine-code level, with the proof open for others to inspect.
