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 encoding (full) Rust semantics into an interactive theorem prover... not that it's possible to keep up with the news these days anyway, especially if it's not your full time job. Another question that I don't know the answer to is how full-program optimization changes the picture with that, wonder if someone has any insights there.