形式验证是 AI 生成代码质量保障的关键，做 AI 安全或软件验证的开发者可以直接用这个基准测试自己的模型，看看能否补全 Lean 证明。
FVSpec 是一个新基准，用于评估 AI 模型和智能体在真实软件形式验证任务上的能力。研究团队从真实 Python 仓库中抓取 11,039 个属性测试（PBT），并自动将其中 2,772 个（25%）翻译成 9,415 个 Lean 4 规范（含占位符）。翻译过程需模拟 Python 语义、推断逻辑属性并处理依赖类型编程的复杂性。团队设计了一个三智能体 LLM 流水线完成翻译，并提供了多种自动化与基于模型的证明生成基线。所有代码和数据已开源，旨在推动 AI 辅助真实软件形式验证这一未充分探索的领域。
FVSpec: Real-World Property-Based Tests as Lean Challenges
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.