# VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 33 of its 46 references that are in the map.
- First posted on arXiv 8 May 2026.

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

- [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)
- [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)
- [DeepSeek-V4: Towards Highly Efficient Million-Token Context Intelligence](https://mlsanity.com/paper/2606.19348/) (2026)
- [Measuring Coding Challenge Competence With APPS](https://mlsanity.com/paper/2105.09938/) (2021)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024)
- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [CodeContests+: High-Quality Test Case Generation for Competitive Programming](https://mlsanity.com/paper/2506.05817/) (2025)
- [VERINA: Benchmarking Verifiable Code Generation](https://mlsanity.com/paper/2505.23135/) (2025)
- [Can Large Language Models Write Good Property-Based Tests?](https://mlsanity.com/paper/2307.04346/) (2023)
- [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)
- [Large Language Models for Code Generation: A Comprehensive Survey of Challenges, Techniques, Evaluation, and Applications](https://mlsanity.com/paper/2503.01245/) (2025)
- [KNighter: Transforming Static Analysis with LLM-Synthesized Checkers](https://mlsanity.com/paper/2503.09002/) (2025)
- [HardTests: Synthesizing High-Quality Test Cases for LLM Coding](https://mlsanity.com/paper/2505.24098/) (2025)
- [A benchmark for vericoding: formally verified program synthesis](https://mlsanity.com/paper/2509.22908/) (2025)
- [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)
- [Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference](https://mlsanity.com/paper/2503.04779/) (2025)
- [VeruSAGE: A Study of Agent-Based Verification for Rust Systems](https://mlsanity.com/paper/2512.18436/) (2025)
- [AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms](https://mlsanity.com/paper/2602.09464/) (2026)
- [AI IDEs or Autonomous Agents? Measuring the Impact of Coding Agents on Software Development](https://mlsanity.com/paper/2601.13597/) (2026)
- [VerifyThisBench: Generating Code, Specifications, and Proofs All at Once](https://mlsanity.com/paper/2505.19271/) (2025)
- [Can LLMs Generate Reliable Test Case Generators? A Study on Competition-Level Programming Problems](https://mlsanity.com/paper/2506.06821/) (2025)
- [VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus](https://mlsanity.com/paper/2510.25015/) (2025)
- [CodeHacker: Automated Test Case Generation for Detecting Vulnerabilities in Competitive Programming Solutions](https://mlsanity.com/paper/2602.20213/) (2026)
- [Beyond Static Pattern Matching? Rethinking Automatic Cryptographic API Misuse Detection in the Era of LLMs](https://mlsanity.com/paper/2407.16576/) (2024)
- [Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?](https://mlsanity.com/paper/2510.12702/) (2025)

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

- [Solving VeriContest with a Lean-Backed Rust Verifier](https://mlsanity.com/paper/2610.03994/) (2026)
- [Second-Order Problem Solving for Recursive Self-Improvement in Formal Verification](https://mlsanity.com/paper/2610.05701/) (2026)
- [Beyond Type-checking: Towards Holistic Evaluation of Formal Specification Generation](https://mlsanity.com/paper/2610.10604/) (2026)

## Abstract (arXiv)

Large language models can generate useful code from natural language, but their outputs come without correctness guarantees. Verifiable code generation offers a path beyond testing by requiring models to produce not only executable code, but also formal specifications and machine-checkable proofs. Progress in this direction, however, is difficult to measure: existing benchmarks are often small, focus on only one part of the pipeline, lack ground-truth proofs or rigorous specification validation, or target verification settings far from mainstream software development. We present VeriContest, a benchmark of 946 competitive-programming problems from LeetCode and Codeforces for verifiable code generation in Rust with Verus. Each problem pairs a natural language description with expert-validated formal specifications, judge-accepted Rust code, Verus-checked proofs, and positive and negative test suites. VeriContest is constructed through a three-phase pipeline that scales from manually verified seed problems to semi-automated expansion with human-in-the-loop review. To further strengthen benchmark quality, we use testing as an additional quality-assurance layer for validating postcondition completeness. VeriContest supports isolated and compositional evaluation of specification generation, code generation, proof generation, and end-to-end verified program synthesis. Evaluating ten state-of-the-art models reveals a sharp gap between coding ability and verifiable code generation: the strongest model reaches 92.18% on natural-language-to-code generation, but only 48.31% on specification generation, 13.95% on proof generation, and 5.29% end-to-end. These results identify proof and specification generation as the central bottlenecks for models and establish VeriContest as a rigorous platform for measuring and training future systems that generate code with machine-checkable correctness.