Four weeks. That is how long a five-person Google DeepMind team, working with AI agents, took to produce machine-checked proofs of key security properties in the compiled code of Signal’s core chat library. The proofs run to about 6.5 million lines. Earlier landmark efforts on other systems took years of specialist labour, and usually needed code written to be proved.
The research post, dated 10 November 2026, sets out the method and its limits. The accompanying technical paper reports the numbers in more detail. The work is not a proof of the Signal app as a whole, and it is not a proof of other apps that use a related design. It is a proof of specified properties of libsignal, the reference library, for one-to-one sessions, taken down to the compiled machine code that actually runs.
What was proved
libsignal is the library that implements Signal’s encryption design. In plain terms, that design is meant to keep a message private even if a key is stolen later, and to recover after a device has been briefly compromised. Those two ideas are usually called forward secrecy and post-compromise security.
The team compiled the unmodified library — version 0.105.4, plus the related SPQR crate at version 1.6.0 — with the ordinary Rust compiler, into a small command-line tool running on 64-bit Arm Linux. The proofs are about that executable, not a cleaned-up rewrite. The verified library is about 560KB, or about 140,000 machine instructions.
They cover the PQXDH handshake, which is how two people start a private session, including a post-quantum step meant to stand up to a future quantum computer, and the Triple Ratchet, which issues a fresh key for each message. In the “symbolic” model, which treats the underlying cryptography as ideal, the paper also claims handshake secrecy against a later attacker with a quantum computer. Group chats, sealed sender and the server-side protocol are left as future work.
How the work was done
Formal verification means writing a precise mathematical statement of what the code must do, then proving that the code meets it. A single missed assumption can weaken the result, so people still have to choose what to prove and approve that statement.
The paper is blunt about the split. Humans selected the properties, resolved ambiguities and signed off the specification. Agents then wrote the proofs. Those proofs are accepted only if Lean, a proof-checking system, confirms them. The reliability of the result, the authors write, does not depend on the reliability of the proving agents, because Lean’s kernel checks the logic.
The research post says the proving agents were powered by Gemini Carbon. The proof work itself was done by five researchers over four weeks, each running agents on their own workstation. That is a short campaign by the standards of the field. The paper notes that the seL4 microkernel, a famous earlier verification, took twenty person-years, and that the CompCert C compiler took six. Both of those codebases were written with proof in mind. libsignal was not.
The proofs themselves can be long because they talk about machine code. About 6.5 million lines are proofs: 5.3 million about the binary, plus separate files for the two security models. A reader who wants to trust the headline claims still has to read the trusted parts: about 18,000 lines of specification in the repository, plus about 8,000 lines of the Arm machine-code model and the symbol names mapped onto the executable. The low-level cryptographic routines, two output functions and a few library calls are assumed by contract, not proved.
A check against old bugs
To test whether the statements were strong enough, the team reintroduced two bugs that researchers had previously found in libsignal, and that have since been fixed. In both cases they proved that the symbolic security theorem does not hold of the bugged binary. That is a useful check: a specification that still “succeeds” on known-broken code would be too weak.
One of those bugs stored a new session’s state, including a copy of a secret, after a prekey message had only decrypted under an older session. The other accepted a handshake whose base key had been mangled, creating a second session with the same shared secret.
What the result does not say
The authors are careful, and the limits matter. The proofs do not cover every part of Signal, every possible attack, or the cryptographic primitives themselves. Side channels are out of scope. The computational proof, which tries to bound a real attacker’s chance of success, gives no guarantee against a quantum adversary, and its bound becomes vacuous for multiple long sessions with many rounds.
Variants of the same protocol are used in WhatsApp, Meta’s Messenger and Google Messages, the paper notes. Those apps were not the artefact under proof. A proof about libsignal does not automatically transfer to every product that speaks a similar language.
Ehren Kret, Signal’s chief technology officer, is quoted in the research post as saying that rigorously verifying the protocol implementation “gives us even greater confidence in our code’s privacy guarantees”.
The proofs and specifications are published in an open repository.
Why it matters
Most people who send a private message never see the library that encrypts it. A method that can check the compiled code of that library, in weeks rather than person-years, is a practical change in how such software can be audited. It is not a certificate that Signal, or any other chat app, is free of flaws. It is a machine-checked argument about specified properties of one core library, produced quickly enough that other critical code might be next.
Most everyday chat products still have no such proof, and some popular tools do not encrypt messages end to end at all. An earlier report covered a consumer chat tool that sends texts without that protection.
The post A Five-Person Team and AI Proved Signal’s Code in Four Weeks appeared first on DailyAI.
