[2603.25810] ExVerus: Verus Proof Repair via Counterexample Reasoning

Computer Science > Programming Languages arXiv:2603.25810 (cs) [Submitted on 26 Mar 2026] Title:ExVerus: Verus Proof Repair via Counterexample Reasoning Authors:Jun Yang, Yuechun Sun, Yi Wu, Rodrigo Caridad, Yongwei Yuan, Jianan Yao, Shan Lu, Kexin Pei View a PDF of the paper titled ExVerus: Verus Proof Repair via Counterexample Reasoning, by Jun Yang and 7 other authors View PDF Abstract: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. Comments: Subjects: Programming Languages (cs.PL); Machine Learning (cs.LG) ACM classes: D.2.4 Cite as: arXiv:2603.25810 [cs.PL]   (or arXiv:2603.25810v1 [cs.PL] for this version)   https://doi.org/10.48550/arXiv.2603.25810 Focus to learn more arXiv-issued DOI via DataCite (pending registration) Submission history From: Jun Yang...