AI RESEARCH
AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms
arXiv CS.AI
•
ArXi:2602.09464v2 Announce Type: replace-cross Vericoding refers to the generation of formally verified code from rigorous specifications. Recent AI models show promise in vericoding, but a unified methodology for cross-paradigm evaluation is lacking. Existing benchmarks test only individual languages/tools (e.g., Dafny, Verus, and Lean) and each covers very different tasks, so the performance numbers are not directly comparable. We address this gap with AlgoVeri, a benchmark that evaluates vericoding of $77$ classical algorithms in Dafny, Verus, and Lean.