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