Google DeepMind researchers used AI agents to mathematically verify key security properties of the code behind the Signal Protocol, which protects billions of private conversations across apps like Signal, WhatsApp and Google Messages.
The researchers used AlphaProof Code, a multi-LLM agentic framework that divides the work of formal verification much like a research team: human experts work alongside AI to decide what needs to be proven, while a group of AI agents works to prove it.
In just four weeks, the AI agents generated and checked millions of lines of mathematical proofs, demonstrating that key security properties of the Signal Protocol hold.
To test its ability to detect vulnerabilities, researchers deliberately reintroduced two previously fixed bugs into an isolated version of Signal’s code. AlphaProof Code successfully identified both issues and generated machine-checked proofs showing that the modified code was insecure.
Signal’s Chief Technology Officer commented on the research:
“While prior formal verification focused on smaller portions of the code, Google DeepMind’s approach enables significant expansion. Using AI agents to translate live code into valid Lean theorems is a major breakthrough. As AI-driven security threats grow, rigorously verifying the Signal protocol implementation gives us even greater confidence in our code’s privacy guarantees”.
While the Signal Protocol already has been extensively assessed by security experts, AlphaProof Code adds another layer of assurance. This marks an important step towards making secure communication even more reliable and shows how AI can help strengthen the security of critical software.
Informiert bleiben
Möchtest du die neuesten Signal Neuigkeiten, Tipps und Updates erhalten? Folge uns auf Bluesky oder auf Mastodon.
