Google DeepMind researchers have used artificial intelligence to mathematically prove the security of key components in the Signal messaging protocol. The four-week project serves as a proof of concept for a new AI framework called AlphaProof Code, which aims to make formal verification more practical for software developers.
Formal verification uses mathematical logic to check that software functions exactly as intended. Before the current wave of AI tools, this process required experts to manually write complex formulas and proofs, a task that took months or years. The DeepMind team demonstrated that agentic AI can significantly reduce the time needed to build these mathematical arguments.
AlphaProof Code and Signal Validation
The analysis focused on specific cryptographic guarantees within the Signal protocol, which protects communications on platforms like Signal, Google Messages, and WhatsApp. The AI system did not find any new vulnerabilities in the code it reviewed. However, when the researchers tested the system on older versions of the protocol that contained known and fixed flaws, the AI correctly identified the weaknesses and proved that those versions could not be formally verified.
Swarat Chaudhuri, a research scientist at DeepMind, noted that the team is excited by the results but emphasized that the work is just one step in a larger process. He stated that there is still a long way to go before this technology can scale to verify all software in the world.
The researchers are releasing the specification and proofs they developed for the Signal analysis. This open release is intended to help other teams conduct formal verification work on different systems.
Human-AI Collaboration in Security
Ehren Kret, the chief technology officer at the Signal Foundation, highlighted that the project built upon prior formal verification work done by his organization. He noted that while previous efforts focused on smaller code segments, the DeepMind approach allows for significant expansion. Kret added that rigorously verifying the implementation gives the Signal team greater confidence in their privacy guarantees as AI-driven security threats grow.
Pushmeet Kohli, chief scientist at Google Cloud and DeepMind, suggested that this capability could benefit industries that rely on strict security assurances, such as banking. He said that if companies can verify the correctness of their implementations, they can rest easy about bugs and vulnerabilities.
Despite the success of the project, questions remain about the cost and scalability of AI-automated formal verification. DeepMind conducted the Signal analysis as a research project without charging fees. Google declined to share the specific costs of the analysis or comment on plans to release a commercial product based on the technology.
Chaudhuri described the project as a “human-AI collaboration process.” He explained that the agents contribute and self-correct at almost every phase, but the team still seeks human input and review at key points. He warned against a scenario where AI generates both the goals and the proofs without oversight, calling for a middle ground that ensures rigorous human validation.
Source: Ars Technica
