Can AI Write Rust Programs That Can Be Formally Verified?

What is it about?

AI can write code, but can it also produce programs whose behavior can be formally checked? NL2VBench is a collection of 762 tasks designed to test this. Each task gives an AI system a natural-language description and a programming interface, then asks it to produce a Rust program together with the specifications and proof information needed for verification. We use these tasks to assess how well current AI models handle the complete process.

Featured Image

Why is it important?

Code that looks correct can still contain errors. Formal verification offers a way to check whether a program meets its stated requirements, but generating the code, requirements, and proofs together is difficult. NL2VBench measures this full challenge rather than just whether AI can produce code that compiles. Our results show that even the strongest model we tested succeeds on fewer than half of the tasks under our stricter correctness measure, leaving substantial room for improvement.