# Google DeepMind uses AI agents to formally verify Signal's libsignal code

> Original title: Banger report from Google DeepMind.

- Source: Elvis Saravia
- Published: 2026-11-11T14:14:58.000Z
- Bad Influence: https://badinfluence.news/items/u4svnmfjjc464pcjmzjttc7ux
- Original: https://x.com/omarsar0/status/2120520666319647096

## Summary

Google DeepMind says AI agents wrote about 6.5 million lines of Lean proofs showing key security properties of Signal's libsignal code, down to compiled machine code. A five-person team finished the proof work in four weeks, while verifying the seL4 microkernel took twenty person-years. When two old Signal bugs were reintroduced, the system proved the buggy versions insecure.

## Post

Banger report from Google DeepMind.

This is also a good example of the type of ambitious work you can now do with frontier models.

(bookmark it)

They used AI agents to prove key security properties of Signal's code, down to the compiled machine code.

Agents powered by Gemini 4 Carbon wrote about 6.5 million lines of Lean proofs on the unmodified libsignal code. A team of five finished the proof work in four weeks. Verifying the seL4 microkernel took twenty person-years.

In this work, humans and agents write the security specs, prover agents write the proofs, and Lean checks every proof before it is accepted.

When they reintroduced two old Signal bugs, the system proved the buggy versions were insecure.

Paper: https://deepmind.google/documents/36/Formal_Verification_of_Signal_4.pdf

![](https://badinfluence.news/api/img-proxy?u=https%3A%2F%2Fpbs.twimg.com%2Fmedia%2FHW2aTvkbwAAoFxP.jpg&mode=thumb&exp=1794700800&sig=07043b3ab98bb487)