SeVerus: Context-Aware, Gamified Benchmarking for Rust Verification
Coding agents achieve high success rates on existing benchmarks for Verus, a verifier for Rust programs. These benchmarks typically provide the auxiliary lemmas needed to complete a proof. In practice, however, such lemmas must be discovered and proved. To capture this challenge, we present SEVERUS, a context-aware tec...
Álvaro F. Silva, Martim Afonso, Nuno Saavedra et al.
· 0 citations