AI checked the code behind Signal. What does that mean for quantum-safe messages?

Google DeepMind has used AI-assisted mathematical proofs to check parts of the code behind Signal’s encryption, including the handshake designed to protect messages from future quantum computers. The November 10 result addresses a practical privacy problem: a sound encryption design can still be implemented incorrectly.^[1][2]

The important limit is that the researchers verified a particular command-line build of Signal’s cryptographic library, not the complete Signal phone apps. Their numerical bounds on an attacker’s chances of success do not cover quantum attackers. This is evidence about specified parts of the implementation, not a guarantee that every Signal conversation is immune to every attack.^[1][2]

Why the code matters

Encryption is often explained as a mathematical lock. But a messaging app also needs software to create keys, accept messages in the right order and update its secrets. A mistake in those instructions can undermine a good design.^[1][2]

DeepMind’s AlphaProof Code framework connects security statements to compiled machine code: the instructions a processor executes. Human researchers decide what the software must guarantee and review the assumptions. AI agents construct proofs, which a separate mathematical checker called Lean accepts or rejects. The proof assumes that some underlying cryptographic routines behave as specified, rather than checking every part of their implementation.^[1][2]

That division matters. A plausible AI answer is not the evidence here. The evidence is a machine-checked argument about the specified program, within the boundaries of the model the researchers chose.^[1][2]

The quantum connection

Signal announced its PQXDH handshake in September 2023. A handshake is the initial exchange that lets two parties establish shared secrets. PQXDH was designed to help protect conversations against an attacker who records encrypted traffic now and gains a sufficiently capable quantum computer later.^[4]

In October 2025, Signal announced its Triple Ratchet, combining its existing key-updating mechanism with a post-quantum component called the Sparse Post-Quantum Ratchet, or SPQR. A ratchet repeatedly changes encryption secrets so a single compromised key need not expose an entire conversation indefinitely. These protections are ordinary software running on ordinary devices, not quantum computers inside phones.^[5]

Today’s research studies code implementing both components. That is a new verification result, not a new Signal encryption rollout.^[1][2]

Two proofs, two different boundaries

The paper uses two approaches. A symbolic proof treats cryptographic operations as ideal building blocks. Within its stated scenario, it covers handshake secrecy even when the attacker can break the traditional Diffie–Hellman method for agreeing on a shared secret. But it assumes the parties already have the correct cryptographic identity keys for each other, and it does not establish the post-quantum recovery properties of the added ratchet.^[1][2]

The computational proof instead relates an attacker’s success to assumptions about the cryptographic building blocks. The authors explicitly say its bounds provide no guarantee against a quantum adversary. It also simplifies the setting, including fixed-length messages and no multi-device state.^[1][2]

For a reader assessing the headline, three separate questions help: Is the encryption design suitable for the threat? Does the checked code implement the promised properties? Does the actual app, device and operating environment satisfy the proof’s assumptions? Progress on the second question does not automatically settle the other two.

What the result adds

The authors report about 6.5 million lines of checked proof code, resting on roughly 26,000 lines of trusted specifications and processor semantics. A large proof is not automatically a broad guarantee: the smaller trusted layer still needs expert judgment. As a test, the team reintroduced two previously fixed bugs into isolated versions and proved that those versions violated its symbolic security statements. That was a controlled experiment, not the discovery of two new flaws in today’s Signal app.^[1][2]

Signal already described formal verification as part of its development process in 2025. The new work’s claimed advance is the depth of the connection to unmodified, compiled library code. DeepMind has published the proofs and specifications for outside scrutiny; the report is research from the team that built the system, not an independent certification of every deployment.^[1][2][3][5]

For everyday users, the news is another way to check the software protecting private messages. It does not call for a new setting or establish a date when quantum computers will threaten current encryption. The useful next evidence will be independent review of the assumptions, broader coverage of real app behavior and a demonstrated process for keeping proofs aligned with changing code.^[1][2]