// ZDNET — INTELLIGENZA ARTIFICIALE
Google’s new AI tool just proved Signal encryption really works – here’s how
With the aim of securing other vital systems, Google DeepMind plans to open-source its AlphaProof Code.
Researchers at Google DeepMind used AI to formally verify portions of Signal‘s underlying code — meaning they’ve mathematically proven that at least parts of the encrypted messaging app’s code do what they say, without errors. That’s reassuring given how many vulnerabilities AI systems have discovered in software lately, and how many people’s communications are protected by Signal’s cryptography. WhatsApp and Google Messages use the same encryption.
Also: How AI security failures are endangering your supply chain
DeepMind used AlphaProof Code, “a novel agentic framework for formal verification at unprecedented depth that combines human expertise with AI agents,” the researchers said. They added that formal verification “is the highest standard of security assurance,” but, without automation at scale like AI systems, difficult and time-consuming.
AI companies like OpenAI have been on a math-breakthrough tear as of late, in some cases solving nearly century-old math problems with AI. By computing at such vast scale, AI models can rapidly accelerate much of the manual work mathematicians do.
(Disclosure: Ziff Davis, ZDNET’s parent company, filed an April 2025 lawsuit against OpenAI, alleging it infringed Ziff Davis copyrights in training and operating its AI systems.)
Using AlphaProof Code and building on earlier verification work by the Signal Foundation, DeepMind researchers divided the verification task into two camps. Humans worked with agents to identify what they needed to prove, and multiple agents running Gemini Carbon, the company’s latest model, then executed it. The agents also audited the proof and “highlighted areas that needed a second look by a human — just 1% of the codebase, a massive time savings,” the researchers wrote.
Also: After the vibe-coding rush comes the debugging hangover
For good measure, researchers tested AlphaProof Code’s ability to distinguish correct from flawed code by showing it two previously fixed Signal bugs, for which it produced correct proofs.
“Our work marks the first time AI has been used to formally verify a widely deployed cryptographic protocol at this depth,” the researchers wrote. “It’s also the first time the implementation of a widely deployed protocol like this has been formally verified by any method, with or without AI.”