一句话：VerusSeek 通过检索可复用的 Verus 证明构件并合成循环不变式提示，显著提升 Rust 程序证明合成的成功率。
用 Verus 对 Rust 程序做形式验证能提供强正确性保证，但辅助规范与证明的编写仍需大量人工。现有基于 LLM 的证明合成代理因缺少与验证直接相关的可复用证明模式，在非平凡任务上效果受限。本文提出 VerusSeek：它不检索整文件或函数，而是把已验证的 Verus 代码索引为语义证明构件，包括契约、断言、循环不变式、引理与证明块；对每个验证任务执行类型感知检索，选出匹配当前证明义务的构件，并用有界层次上下文展开，同时为索引边界、frame 条件与终止性论证合成轻量结构化循环不变式提示。Verus 检查每个候选证明，其诊断信息指导下一轮修复。在 VerusBench 的 150 个任务上，VerusSeek 成功验证 122 个，而 AutoVerus 与 RagVerus 分别只有 69 个和 85 个。
Formal verification of Rust programs with Verus provides strong correctness guarantees, but developing the auxiliary specifications and proofs still requires considerable manual effort. Existing LLM-based proof-synthesis agents can automate part of this process, yet their effectiveness on non-trivial tasks is often limited by the lack of reusable proof patterns that are directly relevant to verification. This paper presents VerusSeek, a retrieval-augmented tool for LLM-assisted Verus proof synthesis for Rust programs. Instead of retrieving entire files or functions, VerusSeek indexes previously verified Verus code as semantic proof constructs, including contracts, assertions, loop invariants, lemmas, and proof blocks. For each verification task, the tool performs type-aware retrieval to select constructs that match the current proof obligation, expands them with bounded hierarchical context, and synthesizes lightweight structural loop-invariant hints for index bounds, frame conditions, and termination arguments. Verus checks each candidate proof, and the resulting diagnostics guide the next repair attempt. On 150 tasks from VerusBench, VerusSeek verifies 122 tasks, compared with 69 for AutoVerus and 85 for RagVerus. A demonstration video of VerusSeek is available at https://youtu.be/p2mb61gj95A.
@inproceedings{paperbot12527,
title = {VerusSeek: Retrieval-Augmented LLM-Based Proof Synthesis for Rust Programs},
author = {Yuchen Zhang and Cheng Wen and Jialun Cao and Dugang Liu and Zhiwu Xu and Yuwei Liu and Shengchao Qin},
booktitle = {ASE},
year = {2026},
doi = {10.1145/3832783.3834603}
}