mlsanityData to 7 Oct 2026

AutoVerus: Automated Proof Generation for Rust Code

arXiv 2409.13082 ↗First posted 19 Sep 2024cs.SE cs.AI cs.FLcited by 46

Not on the map. Why?

Abstract (arXiv)

Generative AI has shown its values for many software engineering tasks. Still in its infancy, large language model (LLM)-based proof generation lags behind LLM-based code generation. In this paper, we present AutoVerus. AutoVerus uses LLMs to automatically generate correctness proof for Rust code. AutoVerus is designed to match the unique features of Verus, a verification tool that can prove the correctness of Rust code using proofs and specifications also written in Rust. AutoVerus consists of a network of LLM agents that are crafted and orchestrated to mimic human experts' three phases of proof construction: preliminary proof generation, proof refinement guided by generic tips, and proof debugging guided by verification errors. To thoroughly evaluate AutoVerus and help foster future research in this direction, we have built a benchmark suite of 150 non-trivial proof tasks, based on existing code-generation benchmarks and verification benchmarks. Our evaluation shows that AutoVerus can automatically generate correct proof for more than 90% of them, with more than half of them tackled in less than 30 seconds or 3 LLM calls.

Key facts. Cited by 46 papers in the map (data through 7 Oct 2026). Builds on 24 of its 56 references that are in the map. First posted on arXiv 19 Sep 2024.

Builds on

24 of 56 references.

References · 24

  1. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  2. 2021Program Synthesis with Large Language Modelscited by 3,509
  3. 2023Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generationcited by 1,332
  4. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  5. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  6. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
  7. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  8. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 107
  9. 2022Large Language Models are Zero-Shot Fuzzers: Fuzzing Deep-Learning Libraries via Large Language Modelscited by 102
  10. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 97
  11. 2024DebugBench: Evaluating Debugging Capability of Large Language Modelscited by 74
  12. 2023Clover: Closed-Loop Verifiable Code Generationcited by 62
12 more
  1. 2024Towards AI-Assisted Synthesis of Verified Dafny Methodscited by 58
  2. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  3. 2024DafnyBench: A Benchmark for Formal Software Verificationcited by 54
  4. 2023Verus: Verifying Rust Programs using Linear Ghost Types (extended version)cited by 50
  5. 2023Lemur: Integrating Large Language Models in Automated Program Verificationcited by 49
  6. 2023WhiteFox: White-Box Compiler Fuzzing Empowered by Large Language Modelscited by 37
  7. 2019Generating Correctness Proofs with Neural Networkscited by 36
  8. 2024Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programmingcited by 19
  9. 2023KernelGPT: Enhanced Kernel Fuzzing via Large Language Modelscited by 17
  10. 2022Aeneas: Rust Verification by Functional Translationcited by 7
  11. 20243DGen: AI-Assisted Generation of Provably Correct Binary Format Parserscited by 6
  12. 2021Diffy: Inductive Reasoning of Array Programs using Difference Invariantscited by 5

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2024: 3; 2025: 16; 2026: 27.

46 papers.

Sort:

By area:

  1. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  2. 2024AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinementcited by 33
  3. 2024Automated Proof Generation for Rust Code via Self-Evolutioncited by 31
  4. 2025VERINA: Benchmarking Verifiable Code Generationcited by 30
  5. 2025KNighter: Transforming Static Analysis with LLM-Synthesized Checkerscited by 22
  6. 2025Proving the Coding Interview: A Benchmark for Formally Verified Code Generationcited by 18
  7. 2025A benchmark for vericoding: formally verified program synthesiscited by 16
  8. 2025Propose, Solve, Verify: Self-Play Through Formal Verificationcited by 11
  9. 2025VeruSAGE: A Study of Agent-Based Verification for Rust Systemscited by 11
  10. 2025Locus: Agentic Predicate Synthesis for Directed Fuzzingcited by 8
  11. 2025VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Veruscited by 8
  12. 2025ProofWright: Towards Agentic Formal Verification of CUDAcited by 8
34 more
  1. 2026TraceCoder: A Trace-Driven Multi-Agent Framework for Automated Debugging of LLM-Generated Codecited by 6
  2. 2026FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoningcited by 6
  3. 2025Towards Repository-Level Program Verification with Large Language Modelscited by 4
  4. 2026Neural Theorem Proving for Verification Conditions: A Real-World Benchmarkcited by 4
  5. 2025RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generationcited by 3
  6. 2025Agentic Specification Generator for Move Programscited by 3
  7. 2025Designing LLM-based Multi-Agent Systems for Software Engineering Tasks: Quality Attributes, Design Patterns and Rationalecited by 3
  8. 2026Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systemscited by 3
  9. 2025SymGPT: Auditing Smart Contracts via Combining Symbolic Execution with Large Language Modelscited by 2
  10. 2025SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systemscited by 2
  11. 2025MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verificationcited by 2
  12. 2026Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Inductioncited by 2
  13. 2026Spec-Harness: Measuring and Improving Behavioral Adequacy of LLM-Synthesized Formal Specificationscited by 2
  14. 2026Certified Program Synthesis with a Multi-Modal Verifiercited by 2
  15. 2026Can LLM Aid in Solving Constraints with Inductive Definitions?cited by 1
  16. 2026VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generationcited by 1
  17. 2026Formal Disco: Scalable Open-Ended Generation of Formally Verified Programscited by 1
  18. 2026P3: Joint Program-and-Proof Planning for Verified Code Generationcited by 1
  19. 2026Vero: Can AI Agents Build Formally Verified Software Repositories?cited by 1
  20. 2026Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thoughtcited by 0
  21. 2026ANCORA: Learning to Question via Manifold-Anchored Self-Play for Verifiable Reasoningcited by 0
  22. 2026Combining Mechanical and Agentic Specification Inference for Movecited by 0
  23. 2026FVSpec: Real-World Property-Based Tests as Lean Challengescited by 0
  24. 2026An Empirical Study of LLM-Generated Specifications for VeriFastcited by 0
  25. 2026Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiabilitycited by 0
  26. 2026Specula: Scaling formal specifications for autonomous model checking of system codecited by 0
  27. 2026VeriSkill: A Self-Evolution Framework for Program Verification Skillscited by 0
  28. 2026An AI Approach to Verified Production Cryptographic Librariescited by 0
  29. 2026Schwarz: Solver-Aware Agentic Program Verificationcited by 0
  30. 2026SkillSpec: Intent-Masked Specification Reasoning for Agent Skill Correctnesscited by 0
  31. 2026MAGS: Multi-agent Auto-formalization Guarantees Safety for Agentic Outputscited by 0
  32. 2026Djinnlang: Higher-Level Programming by Unambiguous Specification with an LLM in the Compilercited by 0
  33. 2026OSFoundry: Building and Evolving Operating Systems with Specification-Guided Agentscited by 0
  34. 2026From Verification Failures to Reusable Guidance for Coding Agentscited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2026Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set
  2. 2026KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code
  3. 2026ExVerus: Verus Proof Repair via Counterexample Reasoning
  4. 2026WybeCoder: Verified Imperative Code Generation
  5. 2026Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization
  6. 2026SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs?
  7. 2026Harnessing Code Agents for Automatic Software Verification
  8. 2025APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning