mlsanityData to 14 Oct 2026

ExVerus: Verus Proof Repair via Counterexample Reasoning

arXiv 2603.25810 ↗First posted 26 Mar 2026cs.PL cs.LGcited by 3

On the map: LLM reasoning → Mathematical reasoning

Abstract (arXiv)

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.

Key facts. Cited by 3 papers in the map (data through 14 Oct 2026). Placed in Mathematical reasoning, one of 17 directions in LLM reasoning. Builds on 17 of its 47 references that are in the map. First posted on arXiv 26 Mar 2026.

Builds on

17 of 47 references.

Closest ancestors · 1

Same direction, newest first

  1. 2026Learning to Disprove: Formal Counterexample Generation with Large Language Models19 Mar

Other references · 16

  1. 2021Evaluating Large Language Models Trained on Codecited by 8,320
  2. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
  3. 2025The Illusion of Thinking: Understanding the Strengths and Limitations of Reasoning Models via the Lens of Problem Complexitycited by 302
  4. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 58
  5. 2023Lemur: Integrating Large Language Models in Automated Program Verificationcited by 49
  6. 2023Finding Inductive Loop Invariants using Large Language Modelscited by 36
  7. 2024Inductive or Deductive? Rethinking the Fundamental Reasoning Abilities of LLMscited by 29
  8. 2024Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programmingcited by 20
  9. 2025VeruSAGE: A Study of Agent-Based Verification for Rust Systemscited by 12
  10. 2023Leveraging Large Language Models for Automated Proof Synthesis in Rustcited by 11
  11. 2026DafnyPro: LLM-Assisted Automated Verification for Dafny Programscited by 11
  12. 2025Re:Form -- Reducing Human Annotations in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafnycited by 10
4 more
  1. 2024Assessing the Reasoning Capabilities of LLMs in the context of Evidence-based Claim Verificationcited by 9
  2. 2025Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verificationcited by 6
  3. 2025RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generationcited by 4
  4. 2025Can LLMs Enable Verification in Mainstream Programming?cited by 3

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2026: 3.

3 papers.

  1. 2026P3: Joint Program-and-Proof Planning for Verified Code Generationcited by 2
  2. 2026Automating Formal Verification with Reinforcement Learning and Recursive Inferencecited by 1
  3. 2026Second-Order Problem Solving for Recursive Self-Improvement in Formal Verificationcited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2024AutoVerus: Automated Proof Generation for Rust Code
  2. 2026Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs
  3. 2025VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code
  4. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoning
  5. 2025Understanding Formal Reasoning Failures in LLMs as Abstract Interpreters
  6. 2025Towards Repository-Level Program Verification with Large Language Models
  7. 2025ProofCompass: Enhancing Specialized Provers with LLM Guidance
  8. 2026Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs