FVSpec benchmark tests AI on real-world formal verification

A team of researchers (Quinn Dougherty, Max von Hippel, Hazel Shackleton, Mike Dodds) has released FVSpec, a new benchmark that pushes AI models and agents to solve real-world formal software verification problems. The core idea: take existing Python property-based tests (PBTs) from actual open-source repositories — 11,039 in total — and automatically translate a subset (2,772 PBTs, roughly 25%) into Lean 4 specifications. Each PBT yields about 3 formalizations on average, resulting in 9,415 Lean 4 files with `sorry` placeholders (i.e., unproven theorems). The translation pipeline itself is notable: it uses a three-agent LLM system to model Python semantics in Lean, infer logical properties from imperative tests, and handle the complexities of dependently typed programming. The authors provide baselines using several automated and model-based proof generation approaches, making it a comprehensive testbed.

The challenge is significant. Translating imperative Python PBTs to Lean — a language vastly different from Python — requires deep understanding of both the code's runtime behavior and formal logic. This benchmark directly addresses an underexplored problem: as AI generates an increasing share of the world's code, verifying that code is safe and correct becomes crucial. FVSpec provides a standardized way to measure progress on AI-assisted formal verification. The entire scraper, agent pipeline, and dataset are open source, inviting the community to improve upon the baselines. By connecting real-world software engineering with formal methods, FVSpec could help bridge the gap between practical AI code generation and rigorous verification.