Google DeepMind researchers have reported a major development in AI-powered cybersecurity. Their new framework, called AlphaProof Code, has been used to formally verify the Signal cryptographic protocol down to the machine-code level.
The development matters because the Signal protocol is used to protect private communications across messaging services, including Signal and WhatsApp. By mathematically checking the software implementation, researchers aim to identify errors that could otherwise leave critical security systems vulnerable.
The project also highlights how AI could change the way developers test and secure software.
How Google's AI generated six million lines of proof
According to Google DeepMind research scientist Swarat Chaudhuri, AlphaProof Code agents worked on the project over four weeks in October 2026. The system generated more than six million lines of mathematical Lean proof, using Gemini Carbon models to support the verification process. Formal verification is different from ordinary software testing. Instead of checking whether a programme works in selected situations, it uses mathematical proofs to establish that code meets specified properties. The AI agents worked alongside human experts, helping generate and audit the proofs. The supplied account says researchers needed to review around one per cent of the codebase manually.
AI system tested against previously fixed bugs
Trending Stories
Researchers also tested the framework by deliberately reintroducing two bugs that had previously been fixed in the Signal code. According to the account, AlphaProof Code successfully detected both errors. This test is important because it demonstrates whether the system can identify known weaknesses rather than simply produce large amounts of mathematical output. However, finding two reintroduced bugs does not prove that every possible vulnerability has been eliminated.
What does this mean for WhatsApp and Signal users?
The Signal protocol is a foundation of end-to-end encryption, which is designed to ensure that only the communicating users can read their messages. Verifying its implementation mathematically could help developers identify certain coding errors before attackers exploit them.
However, this does not mean WhatsApp or Signal has become completely hack-proof. Messaging security also depends on device protection, account security, software updates and how encryption is implemented across different services. The research should therefore be seen as a step towards stronger software assurance, not a guarantee of perfect security.
Google DeepMind's bigger cybersecurity ambition
DeepMind's longer-term goal, as described by Chaudhuri, is to use AI-assisted verification across critical software infrastructure. The researchers have also made specifications and proofs available online for the wider research community to examine. From messaging applications to medical devices and power grids, software verification could become an important part of protecting digital infrastructure. The challenge now is whether AI can extend this approach to larger and more complex systems while keeping the mathematical guarantees reliable.


&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)

&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)

&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)
&imwidth=160&imheight=90&format=webp&quality=medium)