Technical Summary: FVSpec

Problem Statement

The paper addresses the critical gap in AI-assisted formal verification (FV) for real-world software. While AI safety proposals increasingly rely on autonomous agents to formally verify AI-generated code, current benchmarks fail to support this goal. Existing benchmarks (e.g., Minif2f, PutnamBench) focus on mathematical Olympiad problems or expert-written theorem prover code, which differs significantly from the "normal" software engineering landscape. Real-world software involves complex dependency trees, black-box external APIs, and components written in different languages, making it inherently harder to verify than monolithic, closed systems. Furthermore, there is a lack of high-quality, large-scale datasets derived from code written by engineers without formal verification intent, which is necessary to train agents that can operate "out-of-distribution" relative to their training data.

Methodology

The authors introduce FVSpec, a benchmark generation pipeline that transforms real-world Property-Based Tests (PBTs) into formal verification challenges in Lean 4. The process involves three main stages:

1. Data Collection (FVSpec:PBT):

   • The team scraped 11,039 unique PBTs from 333 open-source Python repositories using the Hypothesis framework.
   • Repositories were filtered for permissive licenses, and duplicates (including forks) were removed to ensure diversity.
   • The resulting corpus represents "ordinary" software engineering, with tests ranging from trivial assertions to complex multi-strategy tests.

2. Agentic Transpilation (FVSpec:FV):

   • A three-agent LLM pipeline translates the Python PBTs and their associated code into Lean 4.
   • Function Discovery: Uses tree-sitter to extract the Function Under Test (FUT) and its transitive closure of local dependencies.
   • Translation: A formalization agent generates two files: Impl.lean (a computable port of the function) and Spec.lean (theorem statements corresponding to the PBT assertions, with proofs left as sorry placeholders).
   • Iterative Repair: The pipeline employs a Language Server Protocol (LSP) loop. If the generated Lean code fails to compile (via lake build), the compiler diagnostics are fed back to the agent for revision. This loop runs for up to 16 iterations.
   • Handling Effects: For code involving side effects (e.g., Redis, file I/O), the agent axiomatizes these external systems as uninterpreted interfaces. Theorems are stated over these axioms, ensuring the proof obligation remains meaningful regarding the logic of the code, even if the concrete implementation details are abstracted.

3. Post-Production and Filtering:

   • Generated samples undergo rigorous validation. Failures are categorized (e.g., timeouts, type mismatches, unknown identifiers).
   • A "structural faithfulness" score is computed based on five sub-metrics: parameter coverage, type correspondence, strategy coverage, assertion coverage, and dependency coverage.
   • Samples are graded for difficulty (Easy/Hard) using a calibrated LLM judge (claude-haiku-4-5).
   • The final dataset retains multiple formalizations per PBT if no single attempt dominates on quality metrics, resulting in 9,415 challenges derived from 2,772 unique PBTs.

Key Contributions

1. FVSpec:PBT: A corpus of 11,039 deduplicated Python PBTs scraped from open-source repositories, representing the first large-scale, license-clean dataset of PBTs from ordinary software development (excluding competitive programming or curated ITP code).
2. FVSpec:FV: A dataset of 9,415 Lean 4 formal verification challenges. Each challenge includes the original Python code, the original PBT, a Lean implementation, and a Lean theorem statement with proof obligations. The dataset features a median structural faithfulness of 0.65, with 62% of challenges classified as "hard."
3. Baseline Evaluations: Performance metrics for frontier models (Claude Sonnet 4.6, Claude Opus 4.7, and GPT-5.4). The models achieved a mean success rate of 70% on "easy" problems and 49% on "hard" problems, indicating the benchmark is not yet saturated.
4. Open Source Release: The full pipeline (scraper, dependency extractor, formalization agent, and scripts) and datasets are released under an MIT/Apache dual license.

Results

• Pipeline Yield: The transpilation pipeline successfully converted 25% of the initial 11,039 PBTs into valid Lean challenges (9,415 samples).
• Quality Metrics: The median structural faithfulness score is 0.65. Type correspondence (1.00) and assertion coverage (0.97) are high, while parameter coverage (0.24) and dependency coverage (0.48) are lower, indicating areas where translation fidelity varies.
• Model Performance: Baseline models solved 70% of easy samples and 49% of hard samples. Refusal rates were low (4–8% for easy, 3–25% for hard), suggesting models generally attempt the tasks.
• Complexity: The median sample contains 6 theorems. The dataset includes a wide range of complexity, from simple sorting algorithms to complex workflow job schedulers involving time-outs and state transitions.

Significance and Claims

The paper claims that FVSpec provides a necessary foundation for advancing AI-assisted formal verification of real-world software. Unlike previous benchmarks that rely on expert-written proofs or mathematical problems, FVSpec derives specifications from engineers who had no formal verification intent. This ensures the problems are "out-of-distribution" relative to standard model training data, offering a more rigorous test of an agent's ability to generalize.

The authors position this work as a step toward "Guaranteed Safe AI" and "Scalable Formal Oversight," where autonomous agents must verify software as quickly and effectively as they write it. By providing a large-scale, realistic benchmark, FVSpec aims to drive progress in training agents capable of handling the complexities of modern software ecosystems, including external dependencies and side effects, which are often ignored in synthetic benchmarks. The paper modestly acknowledges limitations, such as the potential for axiomatization to miss specific side-effect semantics and the lack of human expert baselines for difficulty calibration.