Beyond Benchmarks: A Case Study of LLM-Generated Verus Specification Failures on Asterinas Vostd

Abstract

Large language models (LLMs) have recently shown promise in automating formal specification generation, but their effectiveness has mainly been demonstrated on self-contained benchmark tasks. This paper examines the changes that occur when LLM-generated specifications are applied to an industrial verification project. To answer this question, we conducted experiments on Asterinas OSTD's Vostd repository, a Rust-based OS-kernel verification codebase built around cross-file dependencies and Entity--Model proof abstractions. We analyze six formal verification targets spanning 156 function-level tasks, 50 Rust source files, and 7,149 lines of code; the failure corpus contains 1,587 reviewed failure episodes nested within 270 model-specific repair traces produced by DeepSeek-V4-Flash, GPT-4o, and Qwen-Coder. Our results show that existing methods effective on benchmarks face significant challenges on Vostd, and that framework customization for industrial validation is necessary and has considerable potential. LLM-generated specifications break in systematic rather than random ways: they cluster across four verification stages (i.e., repository integration, Verus legality, semantic modeling, and proof construction), and their distributions vary across models and targets. We further show that verifier diagnostics do not always identify the true source of failure, and that verifier-guided repair can regress or stall rather than converge. These findings indicate that LLM-generated specifications fail not merely because industrial code is harder, but because failures are structured, stage-dependent, and often repaired in the wrong direction. Future evaluation and tooling should therefore move beyond final pass/fail outcomes and account for where specifications break, whether diagnostics identify the real cause, and whether repair makes progress or simply cycles through new errors.