# CLEVER: A Curated Benchmark for Formally Verified Code Generation

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

## Key facts

- Cited by 29 papers in the map (data through 14 Oct 2026).
- Builds on 21 of its 51 references that are in the map.
- First posted on arXiv 20 May 2025.

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

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [LiveCodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Code](https://mlsanity.com/paper/2403.07974/) (2024)
- [Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation](https://mlsanity.com/paper/2305.01210/) (2023)
- [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)
- [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)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [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)
- [AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement](https://mlsanity.com/paper/2412.06176/) (2024)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving](https://mlsanity.com/paper/2406.14408/) (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)

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

- [VERINA: Benchmarking Verifiable Code Generation](https://mlsanity.com/paper/2505.23135/) (2025)
- [A benchmark for vericoding: formally verified program synthesis](https://mlsanity.com/paper/2509.22908/) (2025)
- [StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion](https://mlsanity.com/paper/2508.04440/) (2025)
- [A Comprehensive Survey on Benchmarks and Solutions in Software Engineering of LLM-Empowered Agentic System](https://mlsanity.com/paper/2510.09721/) (2025)
- [AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms](https://mlsanity.com/paper/2602.09464/) (2026)
- [Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification](https://mlsanity.com/paper/2603.19329/) (2026)
- [VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean](https://mlsanity.com/paper/2602.18307/) (2026)
- [VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code](https://mlsanity.com/paper/2510.06296/) (2025)
- [Towards Verified Code Reasoning by LLMs](https://mlsanity.com/paper/2509.26546/) (2025)
- [Neural Theorem Proving for Verification Conditions: A Real-World Benchmark](https://mlsanity.com/paper/2601.18944/) (2026)
- [Agentic Code Reasoning](https://mlsanity.com/paper/2603.01896/) (2026)
- [CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation](https://mlsanity.com/paper/2604.12268/) (2026)
- [VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation](https://mlsanity.com/paper/2605.08553/) (2026)
- [Agentic Proving for Program Verification](https://mlsanity.com/paper/2605.23772/) (2026)
- [SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems](https://mlsanity.com/paper/2509.23130/) (2025)
- [MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification](https://mlsanity.com/paper/2512.10187/) (2025)
- [Intent-aligned Formal Specification Synthesis via Traceable Refinement](https://mlsanity.com/paper/2604.10392/) (2026)
- [Certified Program Synthesis with a Multi-Modal Verifier](https://mlsanity.com/paper/2604.16584/) (2026)
- [P3: Joint Program-and-Proof Planning for Verified Code Generation](https://mlsanity.com/paper/2608.09277/) (2026)
- [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)
- [BRIDGE: Building Representations In Domain Guided Program Synthesis](https://mlsanity.com/paper/2511.21104/) (2025)
- [CangjieBench: Benchmarking LLMs on a Low-Resource General-Purpose Programming Language](https://mlsanity.com/paper/2603.14501/) (2026)
- [Teaching LLMs Program Semantics via Symbolic Execution Traces](https://mlsanity.com/paper/2605.06184/) (2026)
- [VeriScale: Adversarial Test-Suite Scaling for Verifiable Code Generation](https://mlsanity.com/paper/2605.22368/) (2026)
- [FVSpec: Real-World Property-Based Tests as Lean Challenges](https://mlsanity.com/paper/2606.01008/) (2026)
- [Self-Spec Verifiable Code Generation](https://mlsanity.com/paper/2609.39568/) (2026)
- [SpecGuardBench: Can Coding Agents Construct Reliable Validation Harnesses from Natural Language Specifications?](https://mlsanity.com/paper/2610.16870/) (2026)
- [claimcheck: Measuring and Improving Specification Faithfulness](https://mlsanity.com/paper/2610.17358/) (2026)

## Abstract (arXiv)

We introduce rm Csmall LEVER, a high-quality, curated benchmark of 161 problems for end-to-end verified code generation in Lean. Each problem consists of (1) the task of generating a specification that matches a held-out ground-truth specification, and (2) the task of generating a Lean implementation that provably satisfies this specification. Unlike prior benchmarks, rm Csmall LEVER avoids test-case supervision, LLM-generated annotations, and specifications that leak implementation logic or allow vacuous solutions. All outputs are verified post-hoc using Lean's type checker to ensure machine-checkable correctness. We use rm Csmall LEVER to evaluate several few-shot and agentic approaches based on state-of-the-art language models. These methods all struggle to achieve full verification, establishing it as a challenging frontier benchmark for program synthesis and formal reasoning. Our benchmark can be found on GitHub(https://github.com/trishullab/clever) as well as HuggingFace(https://huggingface.co/datasets/amitayusht/clever). All our evaluation code is also available online(https://github.com/trishullab/clever-prover).