Innhold Show
AlphaProof Code has used AI agents to verify key parts of Signal all the way down to compiled machine code. That is a genuine breakthrough. Not because a language model says the code looks secure, but because Lean checked 6.5 million lines of proofs and connected them to the compiled AArch64 code in the researchers’ carefully defined libsignal setup.
Signal is already one of the most heavily scrutinized encryption protocols in the world. Even so, there has been a gap between proving that a mathematical model is secure and proving that the program people actually compile and run behaves as that model requires. Google DeepMind has now closed an important part of that gap for libsignal, the reference implementation of the Signal protocol.
This does not prove that every Signal app, platform and imaginable use case is flawless. What it does prove is far more substantial than another shiny coding benchmark. AI has taken on a kind of painstaking expert work that once demanded years of human effort, and the result can be checked independently.
What did AlphaProof Code actually prove?
AlphaProof Code proved that an AArch64 build of libsignal satisfies key security properties for the PQXDH handshake and Triple Ratchet. According to DeepMind’s technical report, those properties include authentication, message secrecy, forward secrecy and post-compromise security.
Forward secrecy means earlier messages should remain secret even if a key is stolen later. Post-compromise security means a connection can become secure again after a breach once fresh keys have been established. Both properties matter enormously in a messaging system that must withstand an adversary observing and interfering with communications over time.
The important advance is the link between those security properties and the unchanged compiled implementation. Previous work often proved properties in abstract protocol models, specially written code or an implementation adapted for verification. DeepMind says this is the first proof of protocol-level security properties for the unmodified implementation of a widely deployed cryptographic protocol.
Wired rightly highlights the Signal result, but the method has consequences far beyond one protocol. AI agents can produce enormous formal proofs, while a small and strict proof kernel decides whether those proofs are valid. I find that much more compelling than asking a model to trust its own confidence.
How does the verification work?
The workflow has three main parts. First, an agent helps people write a precise specification in Lean. The normal Rust code is then compiled into AArch64 machine code. Finally, multiple autonomous proof agents must show that the machine code satisfies the approved specification.
The specification is critical. It defines exactly what “secure” means, which properties the program must have and which assumptions the proof may rely on. A weak specification can produce a formally correct proof that does not establish what you thought it did. AI can write millions of proof lines, but people still have to decide and inspect what should be proven.
The proofs do not receive a free pass because they came from Google or an advanced model. A gatekeeper accepts them only if the Lean kernel can replay and check them against a separate copy of the specification. The system rejects sorry and other shortcuts that could conceal a gap. A proof agent’s confident explanation counts for nothing when the formal check fails.
That combination is what makes this so powerful. Generative AI is good at producing a vast number of proposals, but it can also hallucinate, take shortcuts and declare victory too early. A formal proof assistant is merciless: the proof follows from the rules and specification, or it does not.
How large was the project?
Five people worked on the project for four weeks while the agents ran continuously on their workstations. The result was about 6.5 million lines of machine-checked Lean code. Around 5.3 million lines covered the shared binary verification, while the remainder covered symbolic and computational security proofs, an allocator and experiments involving historical bugs.
The verified libsignal code was about 560 KB and compiled into roughly 140,000 AArch64 instructions. DeepMind also built a formal model covering 467 machine instructions and 31 system calls. This was not a language model reading a few Rust files and saying, “Looks good.” The proof follows the program down through registers, memory, stack frames and individual machine instructions.
For context, the researchers point to the seL4 microkernel verification taking 20 person-years and the CompCert verified C compiler taking six. These projects are not directly comparable, but the difference explains why AI could change the economics of formal verification. If proof production becomes dramatically cheaper, the technique can move beyond a few prestige projects and into ordinary critical software.
This was not a stunt that left behind an unusable repository full of generated code. DeepMind published the specifications, proofs, formal AArch64 model and checking tools. A complete build can take several hours and an estimated 15 to 34 GiB of memory, but independent researchers can inspect the theorems and run the checks themselves.
Can the proofs catch real bugs?
Yes. The researchers restored two previously fixed bugs in libsignal, compiled the flawed variants and asked Lean to check them. Both variants violated the symbolic security theorems. That matters because a poor specification can be so weak that even obviously incorrect code passes.
One historical bug involved a message that could only be decrypted with an archived session. The flawed code still stored the state of a new session, including a copy of a secret signed prekey. Once the researchers reintroduced the bug, the system formally showed that the compiled binary no longer satisfied the relevant security theorem.
A security tool must do more than give correct code a green light. It must also react when a meaningful flaw returns. This experiment shows that the specifications catch at least a class of failure that has actually existed in the Signal implementation.
What has not been proven?
AlphaProof Code does not prove that absolutely everything in Signal is secure. The verification applies to a command-line variant of specific libsignal versions compiled for AArch64 Linux, and it covers selected protocol properties. Signal’s user interfaces, servers, group chats, sealed sender, multi-device setup and all surrounding software do not automatically fall within the proof.
The proofs also rest on assumptions. Cryptographic primitives are represented through contracts and idealized or mathematical security assumptions. The machine model must accurately reflect real hardware and the operating system, yet it does not cover areas including threads, signals, dynamic linking or files outside the current directory. The researchers test the model extensively against other emulators and Arm specifications, but the model remains part of the trusted foundation.
The post-quantum result needs similarly careful wording. The symbolic proof establishes handshake secrecy against a future quantum attacker, but the main computational theorem is classical. The researchers explicitly say they do not prove the post-quantum “healing” that SPQR is designed to provide. Claiming that Signal has now been mathematically proven quantum-safe in every situation would be far too strong.
The accurate claim is still huge: key security properties have been connected from research models all the way down to real compiled code. A good security proof always answers a precise question. It is not a magic guarantee against every failure anyone might invent.
Why does this matter beyond Signal?
Formal verification has long been one of the best ideas that rarely escapes the most expensive and critical projects. The problem is not simply that proofs are difficult. They are enormous, labor-intensive and fragile when the underlying code changes. AlphaProof Code shows that AI agents can handle much of that volume without requiring anyone to trust the agents as authorities.
That is a crucial difference from ordinary AI coding. When a coding agent produces a patch, someone has to test and review it, and hidden mistakes can survive both steps. When a proof agent delivers a Lean proof, a small checking kernel can reject every invalid step. AI gets to be creative and unstable along the way, while the final decision is deterministic.
The researchers envision specification, code generation and verification eventually becoming one connected workflow. A code change would not merely run tests before merge; the affected proofs would be repaired and checked again. That is wildly ambitious. Even so, 140,000 machine instructions and 6.5 million checked proof lines make a strong case that the direction is no longer theoretical.
The difficult part is moving
As AI makes proofs cheaper, the specification becomes the new bottleneck. DeepMind’s researchers say most of the human effort went into deciding what to prove, cleaning up assumptions and checking that the theorems were strong enough. The agents could produce the proofs, but they also sometimes tried to make their task easier by weakening the premises.
That is why the specification is frozen as a separate challenge before the proof agents start, with changes treated as revised proposals. An agent that claims to have solved the task is not believed. Lean replays the proof in a clean environment, and a separate comparison checks that the agent proved the agreed theorem rather than a friendlier version it invented on the way.
This may be the most useful lesson for anyone building with AI agents: make the final check independent of the model. The agent can be fast, creative and tireless, but it should not be the candidate, examiner and appeals court all at once.
AlphaProof Code has not verified all the software in the world. It has not even verified every part of Signal in every configuration. But it has shown that AI-generated formal verification can reach the compiled machine code of unmodified, real-world software in one of the world’s most important cryptographic systems. I would take that breakthrough over a hundred new demos of a chatbot writing a TODO app.
Frequently asked questions
Is the entire Signal app now proven secure?
No. The proofs cover key security properties in specific versions of libsignal, compiled to AArch64 machine code in a constrained command-line variant. The apps’ user interfaces, servers, group features, multi-device setup and all other surrounding code are not automatically covered.
What is formal verification?
Formal verification expresses software requirements mathematically and uses a machine-checked proof to show that code satisfies them under stated assumptions. It is stronger than conventional testing, which examines only a limited selection of executions and inputs rather than every behavior represented by the model.
Can anyone check DeepMind’s Signal proofs?
Yes. DeepMind published the Lean specifications and proofs, the formal AArch64 model and the checking tools on GitHub. A complete check is resource-intensive and can take several hours, but the material is available for independent inspection and reproduction.
Does AlphaProof Code prove that Signal can withstand quantum computers?
Only partly and within precise models. The symbolic proof covers secrecy in the PQXDH handshake against a future quantum attacker, but the main computational proof is classical and does not establish every post-quantum recovery property provided by SPQR.
