NL2VBench: A Benchmark for End-to-End Natural-Language to Verifiable Rust Generation

Abstract

Large language models (LLMs) have shown promise in code generation, but generating formally verifiable Rust programs from natural-language descriptions remains highly challenging. We present a benchmark called NL2VBench for generating verifiable Rust programs from natural-language descriptions using Verus.NL2VBench contains 762 verifier-checked tasks derived from five public sources and curated through filtering, deduplication, canonicalization, LLM-assisted drafting, and human revision. Each task provides a natural-language description, task-defining interface information, and a verifier-checked reference solution. To demonstrate its utility, we evaluate five representative LLMs on a direct NL-to-Verus baseline. The results show that current LLMs achieve low verification success and even lower strict semantic correctness, demonstrating that NL2VBench is a challenging and reusable benchmark for future research on LLM-based verified code generation. A demonstration video of NL2VBench is available at https://youtu.be/CNOXHejni1c.