FVSpec

Real-World Property-Based Tests as Lean Challenges

A benchmark for evaluating AI models and agents on real-world formal software verification.

About FVSpec

We scrape 11,039 property-based tests (PBTs) from real-world Python repositories, then automatically translate them into Lean 4 specifications with sorry placeholders. The result is a corpus of 9,415 Lean 4 verification challenges authored, in effect, by practicing engineers who had no formal verification goal in mind — putting our problems out of distribution relative to anything an AI is likely to have memorized.

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 transpilation, evaluate coverage and quality metrics, and provide baselines for proof generation using several automated and model-based approaches.

11,039

Property-Based Tests

Deduplicated Hypothesis PBTs scraped from public GitHub

9,415

Lean 4 Challenges

Samples lifted from 2,772 PBTs (~8 theorems each, 75,005 total)

333

Source Repositories

Permissively-licensed Python projects from 281 distinct GitHub owners

62%

Hard Problems

Classified as hard by a calibrated difficulty predictor — far from saturated

Baselines

We evaluate frontier models on 100 randomly sampled easy problems and 100 hard problems. Each model has access to the Lean LSP via MCP tools and is scored on a binary proved flag (zero sorry remaining and lake build succeeds) and partial credit (fraction of sorry placeholders removed).

pass@k curves for Claude Sonnet 4.6, Claude Opus 4.7, and GPT 5.4, overall and split by easy vs. hard difficulty — pass@k (unbiased estimator) for Claude Sonnet 4.6, Claude Opus 4.7, and GPT 5.4, overall and split by difficulty.

Across Claude Sonnet 4.6, Claude Opus 4.7, and GPT 5.4, models average 70% on easy problems and 49% on hard problems — the benchmark is far from saturated.

See full results

Research Paper

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

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.