FVSpec: Real-World Property-Based Tests as Lean Challenges
2026-05-31 • Software Engineering
Software EngineeringArtificial Intelligence
AI summaryⓘ
The authors created a way to test how well AI can turn real-world Python code tests into formal software proofs using a system called Lean 4. They collected over 11,000 Python tests and translated about a quarter into formal Lean specifications, which is tricky because it needs understanding of Python behavior and complex programming logic. They used a group of AI models working together to do the translations and checked how good the results were. Their work provides tools and data for others to improve AI methods that help make sure software is correct and reliable.
property-based testsformal verificationLean 4dependently-typed programmingtranspilingPython semanticsproof generationautomated theorem provingAI-assisted verification
Authors
Quinn Dougherty, Max von Hippel, Hazel Shackleton, Mike Dodds
Abstract
We present a benchmark for evaluating AI models and agents on real-world formal software verification tasks. We first scrape 11,039 property-based tests (PBTs) from real-world Python repositories, then automatically translate 2,772 of them (25%) into 9,415 Lean 4 specifications with sorry placeholders (about 3 formalizations/PBT; we retain multiple attempts when none dominates on quality metrics). Translating PBTs into Lean specifications is challenging: it requires modeling Python semantics in Lean, inferring the logical property encoded in an imperative PBT, and handling the inherent difficulties of dependently-typed programming in a seldom-used language. We describe a three-agent LLM pipeline for transpiling PBTs into Lean specifications, evaluate coverage and quality metrics, and provide baselines for proof generation using several automated and model based approaches. All code (scraper and agents) and data (PBTs and Lean specifications) are open source. Our benchmark aims to drive progress on the underexplored problem of AI-assisted formal verification of real-world software, which is of increasing interest as AI produces more and more of the world's code.