# VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean

arXiv: https://arxiv.org/abs/2602.18307 · HTML: https://mlsanity.com/paper/2602.18307/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 25 of its 61 references that are in the map.
- First posted on arXiv 20 Feb 2026.

## Builds on (most cited first, 25 of 25)

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024)
- [Verus: Verifying Rust Programs using Linear Ghost Types (extended version)](https://mlsanity.com/paper/2303.05491/) (2023)
- [miniCTX: Neural Theorem Proving with (Long-)Contexts](https://mlsanity.com/paper/2408.03350/) (2024)
- [Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics](https://mlsanity.com/paper/2510.12787/) (2025)
- [CLEVER: A Curated Benchmark for Formally Verified Code Generation](https://mlsanity.com/paper/2505.13938/) (2025)
- [Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification](https://mlsanity.com/paper/2412.14063/) (2024)
- [Proving the Coding Interview: A Benchmark for Formally Verified Code Generation](https://mlsanity.com/paper/2502.05714/) (2025)
- [miniCodeProps: a Minimal Benchmark for Proving Code Properties](https://mlsanity.com/paper/2406.11915/) (2024)
- [Lean-SMT: An SMT tactic for discharging proof goals in Lean](https://mlsanity.com/paper/2505.15796/) (2025)
- [Small Scale Reflection for the Working Lean User](https://mlsanity.com/paper/2403.12733/) (2024)

## Built on by (most cited first, 8 of 8)

- [Vero: Can AI Agents Build Formally Verified Software Repositories?](https://mlsanity.com/paper/2608.13522/) (2026)
- [s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs](https://mlsanity.com/paper/2603.14628/) (2026)
- [AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language](https://mlsanity.com/paper/2607.16372/) (2026)
- [AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics](https://mlsanity.com/paper/2609.05157/) (2026)
- [Lean Pool: An AI-Maintained Archive of Formalized Mathematics](https://mlsanity.com/paper/2609.25199/) (2026)
- [FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification](https://mlsanity.com/paper/2610.00885/) (2026)
- [Second-Order Problem Solving for Recursive Self-Improvement in Formal Verification](https://mlsanity.com/paper/2610.05701/) (2026)
- [Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification](https://mlsanity.com/paper/2610.09681/) (2026)

## Abstract (arXiv)

Large language models have achieved striking results in interactive theorem proving, particularly in Lean. However, most benchmarks for LLM-based proof automation are drawn from mathematics in the Mathlib ecosystem, whereas proofs in software verification are developed inside definition-rich codebases with substantial project-specific libraries. We introduce VeriSoftBench, a benchmark of 500 Lean 4 proof obligations drawn from open-source formal-methods developments and packaged to preserve realistic repository context and cross-file dependencies. Our evaluation of frontier LLMs and specialized provers yields three observations. First, provers tuned for Mathlib-style mathematics transfer poorly to this repository-centric setting. Second, success is strongly correlated with transitive repository dependence: tasks whose proofs draw on large, multi-hop dependency closures are less likely to be solved. Third, providing curated context restricted to a proof's dependency closure improves performance relative to exposing the full repository, but nevertheless leaves substantial room for improvement. Our benchmark and evaluation suite are released at https://github.com/utopia-group/VeriSoftBench.