Test, Don't (Just) Verify

AI is making formal verification go mainstream. AI-assisted mechnical proving companies are raising funds on billion dollar valuations , new people are trying proof assistants, overwhelmingly Lean, at unprecedented rates. Models achieve fascinating results in competitions previously considered to contain some of the hardest problems in the world, such as IMO, ICPC, Putnam; as well as open problems in mathematics such as Erdös Problems. It's not just the hobbyists that are excited about AI-assisted proofs, from Terry Tao , to Martin Kleppman , to Ilya Sergey , prominent researchers around the world are excited and hopeful about the effects. Formal Verification: The Goods Let me quickly give you a run down of the argument: There are multiple complex challenges in formal verification. The first one, and the one that is very hard to solve technically, is that most software in the world does not have a formal specification. A formal specification is a simpler mathematical description of the system we build. Algorithms have formal specifications. Data structures, protocols, data formats, safety-critical systems typically have formal specifications. The majority of the programs in the world doesn't have a formal specification, hell, most of them don't even have informal specifications. At the limit, which is where we actually are, the specification of a program is itself, the implementation is the specification. The lack of a formal specification makes it very hard to formally verify some piece of software, because what would you even verify? The second issue is, proof engineering, the practice of writing proofs for theorems about your systems, is very hard. The proofs have many domain specific elements to them, a proof of a mathematical theorem will be very different from a proof about a programming language, and a proof about the programming language will highly depend on the underlying constructs of its theoretical framework. The widest taught proof engineering book is Software Foundations , and every chapter has a different style of proofs. Someone that went through Volume 2: Programming Language Foundations will not find the problems in Volume 6: Separation Logic Foundations intuitive or obvious. There are other problems such as the tooling for proof automation, brittleness of proofs, reusability of proofs etc. but I don't find them particularly fundamental to proof engineering itself but rather problems of the current generation, so we can leave those aside for now. The rise of LLMs in programming vastly affects both of these points. It affects point number 1 because AI-assisted programming is a very natural fit fot specification-driven development. AI-assisted programming pushes the limits of programming from what you can implement to what you can specify and what you can verify . This is a great incentive for writing executable specifications, because then you can put the LLM inside a loop until it achieves the said objective, irrespective of the means of the achievement. I predict that this will give rise to program optimizers and translators that will be transformative of our work in those domains. However, tests are, as...

Preview: ~500 words