# Agentic Proving for Program Verification

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use.
- Builds on 18 of its 35 references that are in the map.
- First posted on arXiv 22 May 2026.

## Placed in

- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

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

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://mlsanity.com/paper/2507.23726/) (2025)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [Winning Gold at IMO 2025 with a Model-Agnostic Verification-and-Refinement Pipeline](https://mlsanity.com/paper/2507.15855/) (2025)
- [Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics](https://mlsanity.com/paper/2601.14027/) (2026)
- [VERINA: Benchmarking Verifiable Code Generation](https://mlsanity.com/paper/2505.23135/) (2025)
- [CLEVER: A Curated Benchmark for Formally Verified Code Generation](https://mlsanity.com/paper/2505.13938/) (2025)
- [FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving](https://mlsanity.com/paper/2406.14408/) (2024)
- [Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification](https://mlsanity.com/paper/2603.19329/) (2026)
- [Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents](https://mlsanity.com/paper/2603.17150/) (2026)
- [MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study](https://mlsanity.com/paper/2503.04763/) (2025)
- [A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL](https://mlsanity.com/paper/2507.18885/) (2025)
- [A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants](https://mlsanity.com/paper/2508.18587/) (2025)
- [Canonical for Automated Theorem Proving in Lean](https://mlsanity.com/paper/2504.06239/) (2025)
- [Certified Program Synthesis with a Multi-Modal Verifier](https://mlsanity.com/paper/2604.16584/) (2026)

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

- [VGPT-RSI for RH-Adjacent Formal Progress: Boundary Certificates, Verified Finite Lagarias Inequalities, and Explicit Failure Localization](https://mlsanity.com/paper/2606.15096/) (2026)
- [FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification](https://mlsanity.com/paper/2610.00885/) (2026)
- [Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification](https://mlsanity.com/paper/2610.09681/) (2026)

## Abstract (arXiv)

Agentic systems have recently emerged as state-of-the-art approaches for automated theorem proving in formal mathematics. To assess how far these capabilities extend to program verification, we evaluate Claude Code in an agentic proving framework on CLEVER, a Lean 4 benchmark for verifiable code generation. Our results show that Claude generates arguably valid specifications for 98.8% of problems (with 81.3% also accepted by CLEVER's isomorphism-based scoring on the correct portion of the benchmark), certifies implementations against correct ground-truth specifications for 87.5% of problems, and reaches a 98.1% success rate on the end-to-end program generation and verification pipeline over entries with self-consistent premises. Across all stages, Claude further provides high-quality feedback on its own attempts (as confirmed under manual review), identifying underlying causes of failure and lingering bugs in the dataset. These findings highlight a growing mismatch between the difficulty of existing program verification benchmarks and the capabilities of modern agentic provers, and point to the need for more rigorous, bug-resilient evaluation methodologies, and in particular for alternatives to isomorphism-based scoring of generated specifications. More broadly, our results provide empirical evidence that tight compiler-in-the-loop agentic paradigms are currently the most effective approach for foundational program verification.