ExVerus: Verus Proof Repair via Counterexample Reasoning

TL;DR

EXVERUS is a counterexample-guided framework that enhances LLM-based formal proof generation by using behavioral feedback to improve accuracy and robustness.

Contribution

It introduces a novel counterexample reasoning approach for LLMs in formal verification, enabling automatic generation and validation of counterexamples to guide proof improvement.

Findings

Significantly improves proof accuracy over state-of-the-art methods.

Enhances robustness and token efficiency in proof generation.

Effectively uses counterexamples to guide inductive invariant learning.

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.