Google DeepMind's AI agents formally verified Signal's code in four weeks

Great, what a great use case for AI. I feel like Google has been the cleanest of the big players in terms of useful contributions and control of their AI systems. This new proof agent doesn't seem to challenge the spec though, just the implementation, if I've understood correctly.

I wonder how this agent is different than a classic coding agent, in the end it seems to work the same way, iterating over a codebase while writing Lean or Rocq code and running it.

I'm expecting that very soon, perhaps in the next two or three years, it will seem mad that we ever ran _any_ unverified software on our systems, like how it now seems mad we used Telnet or plaintext HTTP.

Earlier this year I was doing some major refactors of an old project. At the time coding agents were really taking off where you could increasingly trust them for more autonomous work, so I was excited to give it a go.

It did the refactor, running for several hours, and ended up volunteering an extensive test suite as well. All tests green!

I was very impressed, until I squinted a little. It had implemented the whole thing backwards, in a way which was not only pointless (didn't achieve any of the stated goals) but actually made things worse than before!

Until that moment I'd been quite bullish about the potential of formal verification in the AI age. But upon seeing that mess, I realized, it might as well have written me a mathematical proof for the code it wrote, and the proof would have passed, and the code would still be wrong!

Very cool. A couple of years back I was toying with the thought of developing a specialized model for formal verification using something like the AlphaZero approach. Given the news from the past few months now I'm glad that I didn't, it really seems that general purpose LLMs are eating everything.

Interesting that they end up with 26k lines of specifications (including Arm semantics). That's quite a large trusted computing base. I guess they need to develop the symbolic/computational models from the ground up. It'll be interesting to see if we can develop reusable libraries of these, a la mathlib, and how the incentives work out there. The AI labs are probably not particularly interested in this, and it's also likely to be thankless work for the researchers. But perhaps if companies doing verification or selling verified products do sprout out, maybe there will have an incentive to share the work and have a standardized TCB. That might, for better or worse, also put a practical end to the "interactive theorem prover wars".

It's also interesting how this will play work for code under development. ChatGPT claims that the day after this was released, libsibnal changed substantially :D Perhaps an intermediate-level, untrusted model in Rust could help (where most of the proof relates the Rust model to the spec, and then a more mechanical proof relates the Rust model to the binary); seL4 did this a long time ago. But I've no idea if this is practical, I haven't heard of anything e […]

I have been experimenting with utilizing how easy it is for AI to code lean (

https://metamagic.substack.com/p/beyond-the-proof-dump-lean-...) and a few lessons

1. AI Lean is not perfect and AI can easily cheat given it is writing the lean. For anyone playing around with AI Lean code at minimum you need another adversarial prompt to review the ai generated lean.

2. In the paper poking around I see they did re-introduce some bugs to verify it would catch them, but they didn't find any bugs it looks like. Maybe signal is just amazing with many eyes reviewing it, but the real story for the rest of us is that if you start AI converting to Lean the value will be in what assumptions it finds. Even for stuff I thought was really logically tight, Lean found a few minor things I had to fix. Similar to fuzzing where I have never not found bugs when I introduced fuzzing into a codebase I expect the same for converting specs to lean.

3. Having the ability to generate Lean (cheaply) via AI is a very interesting unlock for coding. Potentially being able to go from spec to lean to code, using the lean as a logic gatekeeper has the potential to be a real capability that is used more everyday and not just in research.

Noob Question: Apart from these cryptographic systems would it be useful to build these proofs for general pieces of software? Specifically:

1. Has someone applied it to software systems where an AI agent is in the critical path in production i.e. non-deterministic action may occur(albeit with recovery)?

2. What scenarios does it make sense to have a lean proof from the start? Like i imagine if you wanted to make a database system with some guarantees around ACID then it might be better having this from the get go. But probably not that useful for building an API backed service.

Awesome. I remember thinking last year that software is about to get a lot more buggy now that people are offloading more to AI, but tools like this give me hope that perhaps the future of software actually looks a lot more safe.