Its new AlphaProof Code framework combines autonomous AI agents, human-reviewed specifications and mathematical proof checking to examine the actual machine code behind Signal’s cryptographic implementation.
AI-assisted formal verification workflow examining the cryptographic code behind the Signal messaging protocol.Google DeepMind has announced a significant development in AI-assisted cybersecurity research: an agentic AI framework that formally verified key security properties of the code implementing the Signal messaging protocol.
The system, called AlphaProof Code, was used to examine libsignal, the reference implementation of Signal’s cryptographic protocol. According to the research paper published on 10 November, the framework generated approximately 6.5 million lines of machine-checked Lean proof code.
The research focuses on a particularly important distinction in software security: proving that the code actually running on a device satisfies specified security properties, rather than simply testing whether the software appears to behave correctly. Google DeepMind+1
How the technology works
Traditional software testing searches for bugs by running programs under selected conditions. Formal verification takes a different approach: researchers define properties mathematically and attempt to prove that an implementation satisfies them.
AlphaProof Code combines three elements:
- Human-guided AI agents that translate security requirements into formal specifications.
- A mathematical model of AArch64 machine-code execution.
- Autonomous AI agents that generate proofs, which are subsequently checked by Lean’s trusted proof kernel.
The researchers used Gemini-powered agents to generate the proofs. Human researchers remained involved in defining and reviewing the properties that the system was required to establish.
This division of responsibility matters. The AI does not independently decide what constitutes a secure messaging protocol and then certify its own conclusions. The security requirements are specified and reviewed by people, while the generated mathematical proofs must pass independent machine checking. google-deepmind.github.io+1
What was actually verified?
AI-assisted formal verification workflow examining the cryptographic code behind the Signal messaging protocol.The work examined two important components of Signal’s security architecture:
- The PQXDH handshake, which establishes secure communication sessions.
- The Triple Ratchet mechanism, which supports ongoing message-key security.
The researchers report formal proofs covering forward secrecy, authentication, post-compromise security and handshake secrecy.
The paper describes the work as connecting protocol-level security guarantees to the unmodified implementation’s compiled machine code.
It also reports that the framework detected two previously fixed vulnerabilities when researchers deliberately reintroduced them into an isolated version of the code. google-deepmind.github.io+1
Why this matters beyond Signal
Formal verification has historically required substantial specialist effort. Its application has often been limited by the cost of translating complex software into mathematical specifications and constructing proofs.
AI agents could help reduce that workload.
The potential applications extend beyond encrypted messaging:
- Banking and financial infrastructure.
- Medical devices and healthcare software.
- Operating systems and critical applications.
- Telecommunications infrastructure.
- Industrial control systems.
For organisations operating critical software, the ability to prove particular security properties could become an additional layer of assurance alongside conventional security audits and penetration testing.
Important limitations
This result should not be interpreted as proof that the entire Signal application is invulnerable.
The research covers specified properties and a defined implementation and execution model. It does not establish that every component of the Signal application, every device configuration or every possible attack has been formally verified.
The researchers themselves identify opportunities to strengthen the mathematical models and extend the proofs.
What happens next?
AI-assisted formal verification workflow examining the cryptographic code behind the Signal messaging protocol.Google DeepMind has published the research and made the verification materials available through its open-source repository.
The next challenge is whether similar techniques can be applied economically to much larger software systems and production development workflows.
Google has also discussed the possibility of integrating formal verification into AI-assisted software development, allowing developers to prove selected security properties while building and updating applications. Google DeepMind+1
TheTechSpot Take
This is one of the more meaningful applications of AI in cybersecurity because it moves beyond detecting suspicious code or suggesting patches.
The important development is the possibility of using AI to help construct mathematical evidence that specific security properties hold in real implementations.
However, formal verification is only as meaningful as its specifications and assumptions. A proof can be mathematically correct while the chosen security model fails to represent an important real-world threat.
The combination of human expertise, AI-generated proofs and independently checked mathematical results is therefore more promising than the idea of allowing an AI model to certify its own security.
If the approach scales, it could change how developers build and maintain software that millions of people depend on.
