fvspec

FVSpec: Real-World Property-Based Tests as Lean Challenges

Galois, Inc.•Funded by ARIA (Advanced Research + Invention Agency)
arXivGitHub

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 them into Lean 4 specifications with sorryplaceholders. 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. 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.

Read on arXiv →

Figures

Pipeline cost breakdown across formalization stages
Figure 1. Compute cost of the PBT → FV pipeline, broken down by stage.
Distribution of structural faithfulness scores
Figure 2. Structural faithfulness of translations, with a clear mode above 0.5.
Distribution of easy/hard difficulty labels across the dataset
Figure 3. Easy/hard difficulty split assigned by the Claude Haiku grader.
Baseline pass@k curves for Sonnet, Opus, and GPT
Figure 4. Pass@k for Claude Sonnet 4.6, Claude Opus 4.7, and GPT 5.4 on easy vs. hard problems.

For the full paper — including methodology, dataset construction, baseline experiments, and threats to validity — see the arXiv version.