946 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 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 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 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 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 accuracy (%) across the four evaluation tasks.
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.
pass@1 accuracy (%) of ten state-of-the-art models. Click a column to sort; filter by provider or search. Bold marks the best per column.
| # | Model | SpecGen | CodeGen | ProofGen | End-to-End | ||
|---|---|---|---|---|---|---|---|
| nl→spec | nl→code | spec→code | nl+spec→code | spec+code→proof | nl→verified | ||
All values are pass@1 (%) as reported in the paper; bold marks the best in each column. Want to add a model? Open a pull request on GitHub.
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. Accuracy is pass@1 (%); k ranges from 1 to 20.
VeriContest spans 946 main problems (690 from LeetCode and 256 from Codeforces), plus an extended set of 61 verified problems held out of the main evaluation. Every problem ships with the same artifacts:
Seed problems
91 problems manually built with sound, complete specs, code, and proofs.
Semi-automated expansion
Scaled to 946 problems with human-in-the-loop review.
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}
}