# VERINA: Benchmarking Verifiable Code Generation

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

## Key facts

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

## Builds on (most cited first, 30 of 39)

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (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)
- [Qwen2.5-Coder Technical Report](https://mlsanity.com/paper/2409.12186/) (2024)
- [DSPy: Compiling Declarative Language Model Calls into Self-Improving Pipelines](https://mlsanity.com/paper/2310.03714/) (2023)
- [Asleep at the Keyboard? Assessing the Security of GitHub Copilot's Code Contributions](https://mlsanity.com/paper/2108.09293/) (2021)
- [The Stack: 3 TB of permissively licensed source code](https://mlsanity.com/paper/2211.15533/) (2022)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [Leveraging Automated Unit Tests for Unsupervised Code Translation](https://mlsanity.com/paper/2110.06773/) (2021)
- [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)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?](https://mlsanity.com/paper/2310.01831/) (2023)
- [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)
- [SpecGen: Automated Generation of Formal Program Specifications via Large Language Models](https://mlsanity.com/paper/2401.08807/) (2024)
- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement](https://mlsanity.com/paper/2412.06176/) (2024)
- [Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization (Extended Version)](https://mlsanity.com/paper/2403.04651/) (2024)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [Towards Understanding the Characteristics of Code Generation Errors Made by Large Language Models](https://mlsanity.com/paper/2406.08731/) (2024)
- [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)
- [Proof Automation with Large Language Models](https://mlsanity.com/paper/2409.14274/) (2024)

## Built on by (most cited first, 30 of 34)

- [Code as Agent Harness](https://mlsanity.com/paper/2605.18747/) (2026)
- [Large Language Model Reasoning Failures](https://mlsanity.com/paper/2602.06176/) (2026)
- [A benchmark for vericoding: formally verified program synthesis](https://mlsanity.com/paper/2509.22908/) (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)
- [SorryDB: Can AI Provers Complete Real-World Lean Theorems?](https://mlsanity.com/paper/2603.02668/) (2026)
- [VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code](https://mlsanity.com/paper/2510.06296/) (2025)
- [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)
- [Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems](https://mlsanity.com/paper/2605.23109/) (2026)
- [A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants](https://mlsanity.com/paper/2508.18587/) (2025)
- [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)
- [Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization](https://mlsanity.com/paper/2605.26457/) (2026)
- [SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems](https://mlsanity.com/paper/2509.23130/) (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)
- [Lacuna: A Research Map for Machine Learning](https://mlsanity.com/paper/2606.26246/) (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)
- [Making LLMs Reliable When It Matters Most: A Five-Layer Architecture for High-Stakes Decisions](https://mlsanity.com/paper/2511.07669/) (2025)
- [s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs](https://mlsanity.com/paper/2603.14628/) (2026)
- [Automating Formal Verification with Reinforcement Learning and Recursive Inference](https://mlsanity.com/paper/2605.30914/) (2026)
- [Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory](https://mlsanity.com/paper/2606.06523/) (2026)
- [Toward an Agentic Infused Software Ecosystem](https://mlsanity.com/paper/2602.20979/) (2026)
- [Automating Formal Verification with Agent-Guided Tree Search](https://mlsanity.com/paper/2605.27485/) (2026)
- [Projectional Decoding: Towards Semantic-Aware LLM Generation](https://mlsanity.com/paper/2605.30054/) (2026)
- [The Periodic Table of LLM Reasoning: A Structured Survey of Reasoning Paradigms, Methods, and Failure Modes](https://mlsanity.com/paper/2606.11470/) (2026)
- [An AI Approach to Verified Production Cryptographic Libraries](https://mlsanity.com/paper/2608.00965/) (2026)
- [MemoReason: Evaluating the Effect of Parametric Memory on Contextual Reasoning in LLMs](https://mlsanity.com/paper/2609.35312/) (2026)

## Abstract (arXiv)

Large language models (LLMs) are increasingly integrated in software development, but ensuring correctness in LLM-generated code remains challenging and often requires costly manual review. Verifiable code generation -- jointly generating code, specifications, and proofs of code-specification alignment -- offers a promising path to address this limitation and further unleash LLMs' benefits in coding. Yet, there exists a significant gap in evaluation: current benchmarks often focus on only individual components rather than providing a holistic evaluation framework of all tasks. In this paper, we introduce VERINA (Verifiable Code Generation Arena), a high-quality benchmark enabling a comprehensive and modular evaluation of code, specification, and proof generation as well as their compositions. VERINA consists of 189 manually curated coding tasks in Lean, with detailed problem descriptions, reference implementations, formal specifications, and extensive test suites. Our extensive evaluation of state-of-the-art LLMs reveals significant challenges in verifiable code generation, especially in proof generation, underscoring the need for improving LLM-based theorem provers in verification domains. The best model, OpenAI o3, achieves a 72.6% code correctness rate, 52.3% for specification soundness and completeness, and a mere 4.9% proof success rate (based on one trial per task). We hope VERINA will catalyze progress in verifiable code generation by providing a rigorous and comprehensive benchmark. We release our dataset on https://huggingface.co/datasets/sunblaze-ucb/verina and our evaluation code on https://github.com/sunblaze-ucb/verina.