“Code is cheap, show me the specification”: Training LLMs for End-to-End Verified Code Generation

Formal verification offers strong correctness guarantees for software, but writing precise specifications is often as difficult as proving them. Moreover, weak specifications can satisfy a verifier without capturing meaningful behavior, yielding formally verified yet empty guarantees. Contemporary LLMs lack the ability to generate verified code based on just natural language descriptions. Existing benchmarks majorly focus on evaluating specifications only indirectly, typically through testing or one-sided implication checks over simple pre-/post-conditions. We take a step toward closing both gaps for Rust paired with Verus, a verifier that checks Rust code against developer-written specifications. In this work, we develop techniques for end-to-end training and evaluation of verified code generation in Rust. We introduce SpecBench, a specification-evaluation benchmark with SMT-based equivalence checking that definitively judges generated Verus specifications; develop the first end-to-end training pipeline Verus prover to learn end-to-end verified code generation; and release VerusLM-4B-Codex, a 4B-parameter model trained from Qwen3-4B (Instruct) that significantly outperforms models of comparable size and even some larger ones.