Source-linked AI summary
FVSpec: Real-World Property-Based Tests as Lean Challenges
Quinn Dougherty, Max von Hippel, Simon Henniger, Hazel Shackleton, Mike Dodds
TL;DR
AI-assisted formal verification lacks realistic benchmarks for software built without formal-verification intent. FVSpec scrapes real-world Python property-based tests and converts them into Lean 4 challenges through an agentic formalization pipeline. It produces a large, difficult benchmark whose baselines show substantial room for improvement, especially on hard problems.
Problem
Existing formal-verification benchmarks are small, focused on advanced mathematics, or derived from expert-driven projects, limiting evidence about verification of ordinary real-world software.
Method
FVSpec scrapes Python Hypothesis PBTs and lifts them into Lean 4 implementation/specification pairs through an agentic transpilation pipeline with iterative repair and post-production.
Results
Baseline evaluations show mean success of 70% on easy challenges and 49% on hard challenges.
Takeaways & Limitations
FVSpec provides an open benchmark for evaluating AI models and agents on formal verification tasks derived from ordinary software development.
Takeaways & Limitations
The scraper skips repositories with explicitly non-permissive licenses but accepts repositories whose licenses GitHub cannot detect.
Abstract
from arXiv · showhide
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.
1 Introduction
FVSpec addresses the need for realistic benchmarks for AI-assisted formal verification by deriving Lean challenges from property-based tests written for ordinary software. It contributes open datasets and pipeline infrastructure, with baseline results showing substantial remaining difficulty.
- Motivation: Formal verification can certify software mathematically, but existing benchmarks provide limited evidence for real-world software-verification capabilities.Prior benchmarks are small, focused on advanced mathematics, or based on expert-driven verification projects rather than ordinary software development.
- Benchmark idea: FVSpec derives verification challenges from publicly available Python property-based tests, whose logical properties resemble formal specifications.The benchmark contrasts proof-based formal verification with randomly generated property-based tests that check theorem-like rules.
- Contributions: 11,039 deduplicated Python PBTs from 333 open-source repositories form the FVSpec:PBT dataset.The corpus is described as the first large PBT dataset drawn from ordinary software development.
- Contributions: 9,415 Lean 4 FV challenge samples were lifted from 2,772 PBTs using an agentic transpilation pipeline.The resulting samples average eight theorems each and include detailed metadata.
- Evaluation: Baseline evaluations of Claude Sonnet 4.6, Claude Opus 4.7, and GPT 5.4 achieved mean success rates of 70% on easy challenges and 49% on hard challenges.These results indicate that the benchmark remains challenging, especially for hard problems.
- Release: The full scraper, dependency extractor, agent, and post-production pipeline was released under MIT/Apache dual licensing.The release includes the infrastructure used to construct the benchmark.
2 Methods
The methods collect and deduplicate real-world Python PBTs, then lift them into Lean challenges through dependency discovery, agentic transpilation, and post-production. The corpus emphasizes diverse software contexts, while the formalization abstracts effectful systems through uninterpreted interfaces.
- PBT collection: The scraper discovers repositories through the Hypothesis dependency graph, filters explicitly non-permissive licenses, and extracts PBTs with locally defined dependencies.Extraction uses shallow clones, ripgrep, and recovery of the transitive closure of locally defined functions.
- PBT collection: 11,039 PBTs across 333 repositories remained after deduplicating forks and tests with repeated whitespace-normalized SHA-256 hashes.The corpus spans 281 GitHub users and 303 distinct projects.
- Dataset characteristics: The corpus is distributed across repositories: no single repository contributes more than 8.7% of PBTs, while the top ten contribute 58.5%.The median PBT is 13 lines of code and exercises around three times its own length in production code.
- Dataset characteristics: The dataset spans source tests from trivial single assertions to multi-strategy tests exercising complex library APIs.This diversity is inherited from real-world engineering practice rather than curated difficulty.
- Lean lifting: Each PBT becomes a Lean Impl.lean and Spec.lean pair through function discovery, agentic transpilation, and post-production.The pipeline extends the FVAPPS process with an iterative LSP-repair loop.
- Lean lifting: The formalization agent type-checks generated Lean code after each step and receives compiler feedback for up to 16 tool iterations.Impl.lean contains a computable port without sorry, while Spec.lean contains one sorry-backed theorem per Hypothesis assertion.
- Side effects: Effectful code is modeled through uninterpreted interfaces, while property-relevant entities and operators become Lean structures and inductive types.The canonical workflow example abstracts Redis, queues, state transitions, and runner retrieval into axiomatized components.
- Dependency scope: Figure 3 analyzes 6,912 PBTs with recoverable local dependencies; the median PBT exercises code 3.3 times its own length.The remaining 4,127 tests form a subset excluded because they use only standard-library or external code, or dependency extraction failed.
3 Results
FVSpec produces Lean challenges from real-world PBTs while measuring translation faithfulness, implementation recovery, artifact complexity, and proof-generation difficulty. The resulting benchmark preserves substantial structural information but includes incomplete implementations, variable translation costs, and mixed proof difficulty.
- Dataset results: 9,415 samples were generated from 2,772 distinct PBTs, with 85% formalization success from 11,039 inputs.The mean sample contains 8 theorems, with median 6 and maximum 66.
- Dataset results: 65% of PBT groups with multiple formalizations had no single attempt dominating every faithfulness sub-metric.The corpus therefore retains all compiling formalizations and marks the highest-quality version with is_canonical.
- Translation quality: Structural faithfulness has a clear mode above 0.5, although a long tail of lower-quality translations remains.The score combines parameter, type, strategy, assertion, and dependency coverage.
- Translation quality: 59% of samples include complete computable Lean implementations, while 41% use signature-only stubs.Structural faithfulness remains comparable across these groups, with means of 0.67 and 0.68 respectively.
- Artifact complexity: Generated Lean artifacts vary widely in complexity, with sorry counts tracking theorem counts closely.The pipeline creates theorem statements with sorry placeholders, so larger theorem collections generally entail more residual placeholders.
- Proof-generation evaluation: 49% of hard samples and 70% of easy samples were solved on average by the evaluated models.Difficulty grading includes both easy and hard problems, while hard problems tend to produce longer Lean outputs.
4 Limitations
FVSpec has limitations in semantic faithfulness, side-effect modeling, implementation completeness, difficulty calibration, licensing coverage, and human-baseline assessment.
- Translated specifications may not faithfully represent the original PBT, and structural faithfulness is only a heuristic for semantic equivalence.A high score does not guarantee semantic equivalence, while a low score does not necessarily indicate a useless problem.
- Timing, memory, side-effect ordering, and wall-clock latency properties cannot be meaningfully witnessed by the uninterpreted axioms used for effectful interfaces.Pure signatures can also hide internal effects, causing the agent to inline code as if it were pure.
- Difficulty labels are model predictions from claude-haiku-4-5 and are imperfect and uncalibrated against human expert performance.The dataset does not measure human expert performance, so difficulty cannot be calibrated against skilled proof effort.
- 59% of samples have complete Lean implementations, while the remaining 41% constrain opaque stubs and therefore weaken the proof obligation.The residual samples are tagged for filtering.
- The scraper skips explicitly non-permissive licenses but accepts repositories whose licenses GitHub cannot detect.
5 Related Work
FVSpec builds on prior Lean and verification benchmarks while differing in source realism, training-data exposure, and scale. Existing benchmarks commonly use synthetic, pedagogical, expert-written, or mathematics-focused problems rather than properties from ordinary software development.
- FVSpec extends FVAPPS by applying AI-driven translation at scale to PBTs found in the wild rather than programming-puzzle sources.The pipeline infers specifications from natural language and source code.
- Prior Lean benchmarks include small program-specification sets, curated verified-code tasks, and benchmarks spanning code, specification, and proof generation.The cited examples contain 177, 161, and 189 tasks, respectively.
- Other verification benchmarks cover Dafny, Verus, SV-COMP, loop invariants, and SMT-assisted proof-oriented programming, often targeting automated verification or specific tools.
- Interactive theorem-proving corpora such as LeanDojo Benchmark 4 and CoqStoq are much larger but primarily mathematical and drawn from theorem repositories.Their theorems also exist in most frontier models’ training data.
- Mathematics benchmarks evaluate advanced mathematical reasoning, whereas software verification requires modeling program semantics, library APIs, and computational behavior.
- FVSpec differs by using practicing engineers’ real-world PBTs, keeping problems largely out of training data, and operating at thousands rather than hundreds of problems.This contrasts with benchmarks derived from synthetic coding problems or pedagogical exercises.
6 Conclusion
FVSpec is a large benchmark of Lean 4 challenges derived from real-world Python PBTs through an agentic formalization pipeline. Its scale, out-of-distribution origins, and baseline results indicate substantial room for progress in AI-assisted verification of ordinary software.
- The pipeline formalized 2,772 PBTs, producing a 25% lake-build success rate, median structural faithfulness of 0.65, and 62% hard challenges.
- FVSpec sources specifications from practicing engineers without formal-verification intent, making its problems genuinely out of distribution relative to model training data.
- Baseline evaluations of three frontier models show that the benchmark is far from saturated, especially on hard problems.
- The approach could extend to PBTs from other languages and to other interactive theorem provers.
A Comparison with the Hypothesis Corpus
FVSpec and HC-2026 are scraped Hypothesis corpora designed for different downstream uses. Their differing filtering requirements reflect runtime analysis versus Lean formalization goals.
- HC-2026 studies Hypothesis runtime behavior, while FVSpec feeds a Lean formalization pipeline.The design differences are summarized in Table 3.
- HC-2026 filters out repositories whose PBTs are not directly runnable without custom setup, including dependencies on services, API keys, environment variables, or live databases.
- FVSpec imposes no direct-runnability requirement because its pipeline only needs a PBT’s source and specification context.
- Table 3 compares FVSpec with HC-2026, while Table 2 reports PBT corpus statistics.