VerusSeek: Retrieval-Augmented LLM-Based Proof Synthesis for Rust Programs
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 lim...