Verus

Verus is a benchmark dataset containing 6.9 million verified Rust programs, each accompanied by a formal specification and a correctness proof, used to evaluate the performance of large language models in generating code and formal proofs.

Papers using Verus (3)

AutoVerus: Automated Proof Generation for Rust Code2024 · 1 citesReducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set2026AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms2026