AI helps check the code that keeps private messages private

A private message can hold something ordinary and irreplaceable: a family conversation, a plan with a friend, a difficult question. Most of us cannot inspect the code carrying it. We depend on other people finding ways to check that the protection works.

On November 10, Google DeepMind announced AlphaProof Code, a system that combines researchers’ judgment with AI agents to verify security properties of Signal’s core cryptographic code. The company says the work took four weeks. Its announcement includes support from Signal’s chief technology officer, Ehren Kret, who describes the approach as an expansion of earlier verification work. DeepMind’s announcement

Checking the promise against the implementation

Signal’s published design explains why messaging security involves more than encrypting a single note. Its Double Ratchet changes the keys used as a conversation proceeds, aiming to protect earlier messages if current keys are stolen and to regain protection after a compromise under the required conditions. Handling delayed messages adds another practical complication. Signal’s specification

A sound design still has to survive implementation. An analogy is a building plan and the building itself: checking the plan does not settle whether the finished structure follows it. Software verification asks a similarly concrete question, though its answers are mathematical and depend on precisely stated assumptions.

DeepMind’s researchers worked with AI to define the requirements; agents then wrote proofs that the Lean proof checker had to accept. The technical report describes about 6.5 million lines of proof and roughly 26,000 lines of trusted specifications and processor semantics. The target was libsignal v0.105.4’s one-to-one session code, run in a small command-line harness compiled for AArch64 processors. Technical report

What the result covers

The report establishes specified confidentiality, authentication and compromise-recovery properties under its models. Reintroducing two previously fixed bugs produced proofs that the altered code violated the symbolic security theorem. The scope excludes the complete Signal applications, group messaging, multi-device state and side channels. Cryptographic and execution-environment assumptions remain. The computational proof offers no quantum-adversary guarantee. A separate symbolic proof covers handshake secrecy if an attacker later breaks Diffie–Hellman key exchange, but not the added post-quantum ratchet’s recovery after compromise. Results and limitations

For someone reading the headline, those boundaries are part of the result. A proof about one component cannot promise that a stolen unlocked phone, a deceptive message or every other part of an application is safe. This is a reason to understand the work, not a reason to change everyday security habits.

The opportunity is broader access to careful checking

The practical question is whether more software teams could afford this depth of scrutiny. WIRED reports that Google did not disclose the project’s cost or plans for a commercial verification service. A fast research demonstration alone cannot settle the economics of routine use. WIRED’s reporting

The released specifications and proofs give specialists something concrete to examine. Bright has reviewed the sources, not rerun the proofs or independently audited their assumptions. Public research artifacts

Bright’s reading is that the most useful possibility lies in changing who can obtain rigorous assurance. If the approach becomes affordable and repeatable, maintainers of everyday software could spend more effort deciding what people need protected, then test whether the implementation meets that requirement. Independent scrutiny, broader coverage and maintainable proofs will determine how far that opportunity travels.