AI Did Not Prove Signal Secure. It Proved a Carefully Chosen Slice.
A mathematical proof can sound like the end of a security argument. In software, it is usually the start of a more precise one: exactly which property was proved, of which program, under which assumptions? That is the u
A mathematical proof can sound like the end of a security argument. In software, it is usually the start of a more precise one: exactly which property was proved, of which program, under which assumptions?
That is the useful way to read Google DeepMind's November 10 announcement about using AI agents to verify parts of Signal's cryptographic implementation. The research is a major technical achievement. But the headline version, βAI proved Signal secure,β is wider than the actual result.
DeepMind's paper describes machine-checked proofs about selected security properties of compiled libsignal code. It does not claim to prove every part of the Signal service, every client, or every possible security property. That distinction is not a gotcha. It is how formal verification works, and it is the part developers should understand before applying the same idea to their own systems.
What the team actually checked
The work centers on libsignal, Signal's reference protocol implementation. The researchers used version 0.105.4 with the Sparse Post-Quantum Ratchet library, then built an AArch64 Linux command-line executable from the unmodified Rust crates. Their theorems are about runs of that compiled executable, rather than only a clean mathematical sketch of the protocol. The paper says it covers the PQXDH handshake and Triple Ratchet messaging in one-to-one sessions. It reports properties including authentication, confidentiality, forward secrecy, and post-compromise security. DeepMind's paper gives the setup and definitions.
This is an important connection between two layers that are often discussed separately. Protocol analysis asks whether a design has a security property. Implementation analysis asks whether real code preserves that property while parsing messages, updating state, handling keys, and processing errors. A correct design can still be implemented incorrectly.
The paper describes wrapping the existing library in a small command-line harness and reasoning about the compiled program's inputs, outputs, files, and possible runs. For example, the harness can initialize a session, send a message, or receive one. The researchers model an attacker who controls network traffic and can compromise certain keys or state, then prove claims within that model. The technical paper explains that boundary in detail.
DeepMind reports about 6.5 million lines of Lean proof code, resting on about 26,000 lines of specifications and AArch64 semantics. That number is striking, but line count is not the guarantee. The valuable feature is that Lean's kernel checks whether the generated proof follows from the approved formal statements. The proof-generating agents are not trusted to simply announce success. The checker can reject an invalid proof. The much smaller trusted base is easier for experts to review, but it still needs review.
Why a proof still depends on human judgment
A theorem only proves what its statement says. Before a prover can establish βthis program preserves confidentiality,β people must define confidentiality, state which executions count, describe the attacker, and specify how the program is modeled.
Those choices create the proof boundary. DeepMind's paper says human experts reviewed the specifications, and the approved specification was kept separate from the agents' proof work. Its gatekeeping process checks that the final proof matches the approved statements and that Lean accepts it. The researchers also describe reviewing proposed specification changes rather than letting proof agents quietly weaken the goal. The paper's method section is unusually clear about this division of responsibility.
This is why βthe proof checker is trustworthyβ does not mean βthe whole system is proven secure.β The checker can verify a theorem perfectly while the theorem omits a behavior that matters. A strong proof of a narrow claim is still a narrow proof.
There are other assumptions too. The paper models AArch64 Linux execution and relies on contracts for selected cryptographic primitives and routines. A contract says how a component is treated by the proof, instead of proving that component's internal implementation from first principles. The formal model, the specification, and those contracts all matter to the result. The published paper lists these parts of the trusted base.
That is not a weakness unique to this project. Every verification effort has a boundary. The engineering task is to make the boundary explicit, keep it small enough to review, and ensure it covers the risks the system actually faces.
The headline needs a scope check
The title of this article is deliberately narrower than many headlines. DeepMind says it formally verified key properties of code underlying the Signal protocol. That is substantial. It does not follow that the entire Signal product was proven secure.
The paper limits the result to selected one-to-one protocol behavior in a command-line harness. The researchers do not claim to have verified Signal's mobile apps, group messaging, server software, or every operation in the library. The proof also treats some cryptographic primitives through assumptions and contracts. WIRED's report likewise notes that the project did not formally verify the entire Signal mobile app and that scaling the approach remains an open question.
The guarantee also depends on the attacker model. The paper has symbolic and computational analyses with different assumptions and limits. In particular, it does not claim that every stated guarantee holds against every conceivable attacker, in every setting. The specification tells readers which attackers and events were considered. The paper's summary of guarantees and exclusions is more informative than the single phrase βproved secure.β
DeepMind says the project took four weeks. That is an impressive reported timeline, but the paper does not provide a matched cost study showing what the same scope would take a human team today. WIRED also reports that earlier Signal verification work gave the researchers a head start. So the careful conclusion is that AI agents helped complete a difficult verification campaign quickly, not that formal verification has become a one-click task. WIRED's coverage provides that additional context.
The result has a useful adversarial test
The researchers did more than ask the system to prove the unmodified program. They reintroduced two previously fixed bugs and checked whether the verification process could detect that the security claims no longer held. DeepMind reports that the altered versions failed the relevant properties. The paper describes those results as machine-checked counterexamples to the claims for the buggy binaries. DeepMind's announcement and its paper describe this validation step.
That matters because a proof workflow can fail in two directions. It can fail to prove correct code, wasting time. More seriously, it can prove a weak or irrelevant statement and create false confidence. Reintroducing known defects tests whether the chosen specifications are sensitive to at least some meaningful mistakes.
It does not show that every possible bug would be caught. Nor does it replace independent review of the assumptions or the code surrounding the verified component. It is evidence that the process caught those two known issues under this setup, no more and no less.
What developers can take from this
Most teams will not start by proving millions of lines of security-critical code. The more practical lesson is to borrow the structure of the verification effort, even when the proof method is lighter.
1. State the property before choosing the tool. βMake the payment service safeβ is not a testable requirement. βA request with an already-processed idempotency key must not create a second chargeβ is a start. Name the behavior and the conditions under which it must hold.
2. Define the system boundary. Is the claim about a method, a library, a compiled binary, a service, or an end-to-end workflow? List what is outside the boundary: databases, message brokers, identity providers, operating systems, and external APIs can all affect the outcome.
3. Write down assumptions. What must be true about inputs, callers, stored data, clocks, cryptographic libraries, and infrastructure? If a component is trusted rather than verified, say so. Hidden assumptions are where a narrow result gets misread as a broad one.
4. Keep the checker independent from the generator. If an AI writes code or proofs, have a separate deterministic tool check the result. The generator can suggest; the checker should decide whether the artifact satisfies the declared rules.
5. Test the specification with deliberate failures. Remove a permission check, skip a validation step, or introduce a known bug in an isolated test case. Does the property fail? If the answer is always βproof passed,β the statement may not express the guarantee you intended.
6. Report exclusions next to the result. Put the verified version, relevant configuration, threat model, unverified components, and known assumptions beside the green check. A bare βformally verifiedβ label is not enough for a maintainer deciding what can safely change.
This checklist is useful even if the team uses property-based tests, static analysis, model checking, or code review rather than Lean. The point is to make claims precise and checks independent. Formal proof is one end of that spectrum, not a replacement for every other engineering control.
The real shift is in who can afford to ask for proof
Formal verification has long required specialists and significant effort. DeepMind's result suggests that AI agents may reduce the cost of drafting specifications and constructing proofs for some systems. The hard human work does not disappear: experts still choose what matters, review what the theorem means, and decide whether the assumptions match reality.
That is a more useful promise than βAI makes software unhackable.β The likely change is that teams may be able to prove selected properties of more code than before. Whether that becomes routine depends on the quality of the specifications, the cost of review and compute, the ease of reproducing the proofs, and the fit between the verified boundary and the production system.
For now, treat the Signal result as an important demonstration with a carefully defined scope. The proof deserves attention because it reaches compiled implementation code and uses a machine-checking kernel. Its limitations deserve equal attention because they show what a proof does not cover.
The enduring lesson is simple: do not ask only whether a system has a proof. Ask what the proof says, what it assumes, and what it leaves outside.
I write about AI engineering and practical software assurance. Subscribe for more evidence-led guides. Have you used formal methods, property-based testing, or another way to make software guarantees more precise? What would you want a proof to cover in your own code?
Sources
Originally published by Dev.to Security. Aggregated on AIWithGhost for educational purposes β full credit and traffic to the original publisher.