Google AI Verifies Key Security Properties in Signal Code

Google DeepMind says it has used AI to mathematically verify important security properties of the code behind the Signal messaging protocol. The work, announced on 10 November, targets a difficult question in software security: does the implementation actually behave as its designers intend, rather than merely looking sound on paper?

The project used AlphaProof Code, a framework that combines AI agents with human expertise. Researchers translated desired properties into formal specifications and used the system to construct machine-checkable proofs about core cryptographic code. Signal’s protocol protects conversations in Signal and is also used in other messaging products, making the result more consequential than an exercise on a small demonstration programme.

Formal verification is different from a conventional test suite. Tests check selected inputs and outputs. A mathematical proof aims to establish that a stated property holds across all cases covered by the model and its assumptions. In this project, humans still had to define the properties and review the specifications. The AI helped shoulder the enormous work of constructing and checking proofs against real implementation code.

DeepMind says its agents produced roughly six million lines of Lean proof over four weeks. To test whether the method could distinguish secure code from faulty code, the researchers reintroduced two real bugs that had previously been fixed in an isolated version of Signal’s code. The system identified both. That is a useful validation step, although two deliberately reintroduced faults are not a measure of how many unknown vulnerabilities might remain.

The company is releasing its formal verification artefacts so other researchers can inspect the work. That matters because a security claim is stronger when its proof obligations, code version and assumptions can be examined independently. DeepMind also credits Signal engineers for feedback on the methodology.

A proof of selected properties of core cryptographic implementation is not a guarantee that every part of Signal is immune to attack. Messaging security also depends on device operating systems, updates, account recovery, user behaviour and the correctness of components outside the verified scope. A compromised phone can still expose messages even if the protocol code satisfies its formal specification.

There is also a distinction between verifying that code matches a specification and proving that the specification captures every security threat. If an important behaviour is omitted from the model, the proof may still be valid within a narrower boundary. That is why DeepMind’s description of key properties, rather than a blanket claim that the entire app has been proved secure, is important.

The development fits a wider shift in AI security work. TechBooky recently examined an OpenAI pipeline that used models to find and help patch Linux privilege-escalation flaws. AlphaProof Code approaches the problem from another direction: instead of only searching for failures, it tries to establish mathematically that selected safeguards hold.

For organisations building payment, health or infrastructure software, the long-term promise is clear. Proof techniques that once demanded extraordinary specialist labour could become practical for more production systems. The immediate result is more modest but still notable: a research team has shown that AI-assisted formal verification can be applied to code at the heart of a widely used encrypted-messaging protocol, with its boundaries stated for others to test.