ExVerus: Verus Proof Repair via Counterexample Reasoning
This addresses the challenge of reliable formal verification for software developers, offering an incremental enhancement over existing LLM-based approaches.
The paper tackles the problem of automating formal verification with LLMs by introducing EXVERUS, a counterexample-guided framework that uses behavioral feedback to improve proof generation, resulting in significant improvements in proof accuracy, robustness, and token efficiency over state-of-the-art methods.
Large Language Models (LLMs) have shown promising results in automating formal verification. However, existing approaches treat proof generation as a static, end-to-end prediction over source code, relying on limited verifier feedback and lacking access to concrete program behaviors. We present EXVERUS, a counterexample-guided framework that enables LLMs to reason about proofs using behavioral feedback via counterexamples. When a proof fails, EXVERUS automatically generates and validates counterexamples, and then guides the LLM to generalize them into inductive invariants to block these failures. Our evaluation shows that EXVERUS significantly improves proof accuracy, robustness, and token efficiency over the state-of-the-art prompting-based Verus proof generator.