VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean

TL;DR

VeriSoftBench is a new benchmark of 500 Lean 4 proof obligations from software verification, highlighting challenges in proof automation transferability and the importance of repository context in proof success.

Contribution

Introduces VeriSoftBench, a repository-scale benchmark for Lean proofs in software verification, with insights on proof automation transferability and dependency context importance.

Findings

Provers tuned for Mathlib-style mathematics transfer poorly to repository-centric proofs.

Proof success correlates with the size of dependency closures.

Providing curated dependency context improves proof automation performance.

Abstract

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.