VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation

• URL: http://arxiv.org/abs/2605.08553v1
• Date: Fri, 08 May 2026 23:25:05 GMT
• Title: VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation
• Abstract summary: Large language models can generate useful code from natural language, but their outputs come without correctness guarantees.<n>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.<n>We present VeriContest, a benchmark of 946 competitive-programming problems from LeetCode and Codeforces for verifiable code generation in Rust with Verus.
• Score: 2.2194977808724405
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Teaching Code LLMs to Reason with Intermediate Formal Specifications [9.552020178028576]
  SpecCoder is a training framework that learns from validated reference programs, behavior-changing mutants, and multi-turn specification-refinement traces.<n> SpecCoder selects specifications that hold on correct executions while rejecting faulty executions, turning specifications from passive annotations into executable evidence.
  arXiv  Detail & Related papers  (2026-07-05T11:09:30Z)
• WybeCoder: Verified Imperative Code Generation [22.401681809856896]
  WybeCoder is an agentic code verification framework.<n>It enables prove-as-you-generate development where code, invariants, and proofs co-evolve.
  arXiv  Detail & Related papers  (2026-03-31T00:06:44Z)
• AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
  Existing benchmarks test only individual languages/tools, so the performance numbers are not directly comparable.<n>We address this gap with AlgoVeri, a benchmark that evaluates vericoding of $77$ classical algorithms in Dafny, Verus, and Lean.
  arXiv  Detail & Related papers  (2026-02-10T06:58:26Z)
• VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code [25.916111156888235]
  We introduce a new benchmark for formal verification of Large Language Models (LLMs)<n>Our framework replaces ground-truth matching with a formally grounded metric, the equivalence score, and rigorously verifies the quality of generated specifications and code.<n>Our results show that generating formally verifiable code remains a profound challenge for state-of-the-art LLMs.
  arXiv  Detail & Related papers  (2025-10-07T13:19:05Z)
• IFEvalCode: Controlled Code Generation [69.28317223249358]
  The paper introduces forward and backward constraints generation to improve the instruction-following capabilities of Code LLMs.<n>The authors present IFEvalCode, a multilingual benchmark comprising 1.6K test samples across seven programming languages.
  arXiv  Detail & Related papers  (2025-07-30T08:08:48Z)
• VERINA: Benchmarking Verifiable Code Generation [46.582574591358735]
  Large language models (LLMs) are increasingly integrated in software development.<n> Ensuring correctness in LLM-generated code remains challenging.<n>Verifiable code generation offers a promising path to address this limitation.
  arXiv  Detail & Related papers  (2025-05-29T06:12:52Z)
• VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [9.383313869205628]
  We introduce a new benchmark that evaluates end-to-end program verification from natural language descriptions.<n>Our evaluation reveals that even state-of-the-art (SOTA) models, such as o3-mini, achieve a pass rate of less than 4%.
  arXiv  Detail & Related papers  (2025-05-25T19:00:52Z)
• ReCode: Robustness Evaluation of Code Generation Models [90.10436771217243]
  We propose ReCode, a comprehensive robustness evaluation benchmark for code generation models. We customize over 30 transformations specifically for code on docstrings, function and variable names, code syntax, and code format. With human annotators, we verified that over 90% of the perturbed prompts do not alter the semantic meaning of the original prompt.
  arXiv  Detail & Related papers  (2022-12-20T14:11:31Z)
• CodeT: Code Generation with Generated Tests [49.622590050797236]
  We explore the use of pre-trained language models to automatically generate test cases. CodeT executes the code solutions using the generated test cases, and then chooses the best solution. We evaluate CodeT on five different pre-trained models with both HumanEval and MBPP benchmarks.
  arXiv  Detail & Related papers  (2022-07-21T10:18:37Z)
• Measuring Coding Challenge Competence With APPS [54.22600767666257]
  We introduce APPS, a benchmark for code generation. Our benchmark includes 10,000 problems, which range from having simple one-line solutions to being substantial algorithmic challenges. Recent models such as GPT-Neo can pass approximately 15% of the test cases of introductory problems.
  arXiv  Detail & Related papers  (2021-05-20T17:58:42Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.