1,006 verified problems
Competitive-programming tasks, each paired with a ground-truth specification, code, and Verus proof.
Algorithm-level verification
Real contest algorithms proved correct in Verus, going well beyond the usual toy examples.
Verifiable code generation
The full pipeline, evaluated on each task in isolation and composed together end-to-end.
Rigorous quality validation
Every problem is validated by automated testing and reviewed by at least two human experts.
Large language models can now generate useful code from natural language, but their outputs still 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 1,006 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 both 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 ordinary coding ability and verifiable code generation: the strongest model reaches 97.51% on natural-language-to-code generation, but only 57.16% on specification generation, 13.82% on proof generation, and 6.76% end-to-end. These results identify proof and specification generation as the central bottlenecks for current models and establish VeriContest as a rigorous platform for measuring and training future systems that generate code with machine-checkable correctness.
Models that write excellent code stumble when asked to prove it correct. Pick a model to see how its accuracy collapses across the pipeline.
Pass@1 on the 1,006 problems of release v2026.10.1, the same results as the leaderboard.
A sample of real problems. Each couples a natural-language statement with a ground-truth specification, judge-accepted code, and a Verus-checked proof.
Select a problem to view its artifacts.
Proof generation is the hardest task, but it is not a hard ceiling. Two test-time strategies steadily lift proof accuracy as we spend more compute: drawing more independent samples (pass@k) and iteratively repairing failed proofs (repair@k).
Task: spec + code → proof; k ranges from 1 to 20.
The current VeriContest release contains 1,006 problems (722 LeetCode and 284 Codeforces). Problems with multiple valid outputs use problem-specific checkers. Every problem ships with the same artifacts:
Seed problems
91 problems manually built with sound, complete specs, code, and proofs.
Semi-automated expansion
Expanded through generation and human review; the current collection has 1,006 problems.
Testcase validation
Positive/negative tests validate postcondition completeness.
Completeness is further checked by Post2Exe, which translates Verus postconditions into executable Rust and runs them on negative test cases.
@article{xie2026vericontest,
title = {{VeriContest}: A Competitive-Programming Benchmark for Verifiable Code Generation},
author = {Xie, Zichen and Pawagi, Mrigank and Liu, Yuxin and Rai, Aaditi and
Shao, Lize and Berberian, Jr., John and Che, Sicong and Wang, Wenxi},
journal = {arXiv preprint arXiv:2605.08553},
year = {2026}
}