Google DeepMind Uses AI to Prove Signal's Encryption Secure Down to Machine Code

Google DeepMind says it has used artificial intelligence to formally prove key security properties of Signal's encryption — not just in the source code, but in the compiled program that actually runs on a phone's processor. The company announced the result on November 10, 2026, after roughly four weeks of work in which AI agents produced the bulk of the mathematical proofs.

What was verified

The system is called AlphaProof Code. It was pointed at libsignal, the reference library behind Signal's end-to-end encryption. According to CyberInsider, the researchers analysed an executable built from libsignal version 0.105.4 for 64-bit Arm processors and modelled how its machine instructions behave, so that claims about the binary itself could be checked.

The work covered the two pillars of the protocol:

• PQXDH, the opening handshake in which two parties establish a shared secret;
• the Triple Ratchet, which keeps refreshing encryption keys as a conversation goes on;
• properties such as forward secrecy and the recovery of protection for future messages once fresh key material is exchanged;
• handshake secrecy in a model where an attacker can later break classical Diffie–Hellman, a stand-in for a future quantum threat.

Machines write the proofs, humans check the goals

The proofs are written in Lean, a proof assistant that only accepts an argument if every single step checks out. CyberInsider reports that agents powered by Gemini models generated around 6.5 million lines of Lean code; Axios likewise describes millions of lines of machine-checked proof.

Humans still set the target. AI helped turn each security goal into a formal specification, but experts reviewed those specifications. To make sure the tool was not simply rubber-stamping code, the team reintroduced two previously fixed bugs into isolated copies of the library. In both cases the framework produced a machine-checked proof that the altered code broke a security property.

Signal's chief technology officer, Ehren Kret, said the effort extends the scope of earlier verification work and gives the project more confidence in its privacy guarantees, CyberInsider reported. DeepMind has published the verification artifacts on GitHub.

What the proof does not cover

The result is not a certificate that the entire Signal app is free of bugs. The guarantees rest on the attacker models the researchers chose and on the assumption that the underlying cryptographic primitives are sound. Side-channel attacks and the rest of the messenger — its interface, storage and networking code — were outside the scope. No new vulnerabilities in the current protocol were reported.

Why it matters

Formal verification has long been the gold standard for high-assurance software, but it is painfully slow and expensive, which is why it has mostly been reserved for chips, avionics and a handful of cryptographic libraries. If AI agents can produce checkable proofs about real compiled code in weeks rather than years, that level of scrutiny could reach far more software.

There is also a subtler point. Unlike AI-written code, which still has to be trusted or reviewed line by line, a Lean proof can be re-checked independently by anyone. The model's output is only accepted if a small, well-understood checker agrees with it. For a messaging protocol used by millions of people, that is a meaningful extra layer of assurance — and an early sign of how AI could be used to verify software, not just to write it.