AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms
Introduction
We introduce AlgoVeri, a benchmark that evaluates vericoding of $77$ classical algorithms in Dafny, Verus, and Lean. By enforcing identical functional contracts, AlgoVeri reveals critical capability gaps in current models. While frontier models achieve tractable success in Dafny ($40.3$% for Gemini-3 Flash), where high-level abstractions and SMT automation simplify… See the full description on the dataset page: https://huggingface.co/datasets/zzzzzhy/algoveri.
