一句话：通过工业内核验证项目案例研究，揭示 LLM 生成的 Verus 规约呈四阶段系统性失败，诊断与修复常失效。
LLM 自动生成形式规约在自包含基准上表现良好，但在工业验证项目中的有效性未知。本文在 Rust 内核验证仓库 Asterinas Vostd 上开展实证研究，分析 6 个验证目标、156 个函数级任务、50 个源文件与 7149 行代码，并考察 270 条 LLM 修复轨迹及 1587 条经审阅失败片段。结果表明，现有方法在 Vostd 上遭遇显著挑战，需面向工业验证定制框架；失败呈系统性，聚集于仓库集成、Verus 合法性、语义建模与证明构造四个阶段，分布随模型与目标而异。验证器诊断未必定位真因，修复可能回退或停滞。评估应超越最终通过/失败，关注失败位置、诊断真因与修复进展。
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.
@inproceedings{paperbot12269,
title = {Beyond Benchmarks: A Case Study of LLM-Generated Verus Specification Failures on Asterinas Vostd},
author = {Dugang Liu and Ding Wang and Chao Jiang and Cheng Wen and Zhiwu Xu and Zhong Ming and Yuwei Liu and Xinyi Wan and Lin Huang},
booktitle = {ASE},
year = {2026},
doi = {10.1145/3832783.3834504}
}