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. By enforcing identical functional contracts, AlgoVeri reveals critical capability gaps in verification systems. While frontier models achieve tractable success in Dafny ($40.3$% for Gemini-3 Flash), where high-level abstractions and SMT automation simplify the workflow, performance collapses under the systems-level memory constraints of Verus ($24.7$%) and the explicit proof construction required by Lean (7.8%). Beyond aggregate metrics, we uncover a sharp divergence in test-time compute dynamics: Gemini-3 effectively utilizes iterative repair to boost performance (e.g., tripling pass rates in Dafny), whereas GPT-OSS saturates early. Finally, our error analysis shows that language design affects the refinement trajectory: while Dafny allows models to focus on logical correctness, Verus and Lean trap models in persistent syntactic and semantic barriers. All data and evaluation code can be found at https://github.com/haoyuzhao123/algoveri.

翻译：Vericoding指从严格规范生成形式化验证代码。最近的AI模型在验证编码方面展现出潜力，但缺乏跨范式评估的统一方法论。现有基准仅测试单个语言/工具（例如Dafny、Verus和Lean），且各自覆盖差异显著的任务，因此性能数据无法直接比较。我们通过AlgoVeri填补这一空白，该基准在Dafny、Verus和Lean中评估77个经典算法的验证编码。通过强制实施相同的功能契约，AlgoVeri揭示了验证系统中的关键能力差距。虽然前沿模型在Dafny中取得了可处理的成功（Gemini-3 Flash为40.3%），其中高级抽象和SMT自动化简化了工作流程，但在Verus的系统级内存约束（24.7%）和Lean所需的显式证明构造（7.8%）下性能急剧下降。除总体指标外，我们发现了测试时计算动态的显著差异：Gemini-3有效利用迭代修复提升性能（例如在Dafny中通过率提升三倍），而GPT-OSS则过早饱和。最后，我们的错误分析表明语言设计影响精化轨迹：Dafny使模型能够聚焦于逻辑正确性，而Verus和Lean将模型困于持续的语法和语义障碍。所有数据和评估代码可在https://github.com/haoyuzhao123/algoveri获取。