VerusSeek: Retrieval-Augmented LLM-Based Proof Synthesis for Rust Programs

Abstract

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.