ExVerus: Verus Proof Repair via Counterexample Reasoning

Jun Yang, Yuechun Sun, Yi Wu +5

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…