mlsanityData to 7 Oct 2026

VeruSAGE: A Study of Agent-Based Verification for Rust Systems

arXiv 2512.18436 ↗First posted 20 Dec 2025cs.OS cs.AI cs.FLcited by 11

On the map: LLM agents and tool use → Software engineering coding agents

Abstract (arXiv)

Large language models (LLMs) have shown impressive capability to understand and develop code. However, their capability to rigorously reason about and prove code correctness remains in question. This paper offers a comprehensive study of LLMs' capability to develop correctness proofs for system software written in Rust. We curate a new system-verification benchmark suite, VeruSAGE-Bench, which consists of 849 proof tasks extracted from eight open-source Verus-verified Rust systems. Furthermore, we design different agent systems to match the strengths and weaknesses of different LLMs (o4-mini, GPT-5, Sonnet 4, and Sonnet 4.5). Our study shows that different tools and agent settings are needed to stimulate the system-verification capability of different types of LLMs. The best LLM-agent combination in our study completes over 80% of system-verification tasks in VeruSAGE-Bench. It also completes over 90% of a set of system proof tasks not part of VeruSAGE-Bench because they had not yet been finished by human experts. This result shows the great potential for LLM-assisted development of verified system software.

Key facts. Cited by 11 papers in the map (data through 7 Oct 2026). Placed in Software engineering coding agents, one of 16 directions in LLM agents and tool use. Builds on 24 of its 44 references that are in the map. First posted on arXiv 20 Dec 2025.

Builds on

24 of 44 references.

Closest ancestors · 2

Same direction, newest first

  1. 2025Live-SWE-agent: Can Software Engineering Agents Self-Evolve on the Fly?17 Nov
  2. 2024SWE-agent: Agent-Computer Interfaces Enable Automated Software Engineering6 May

Other references · 22

  1. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  2. 2024GPT-4o System Cardcited by 4,467
  3. 2021Program Synthesis with Large Language Modelscited by 3,509
  4. 2023Clover: Closed-Loop Verifiable Code Generationcited by 62
  5. 2024Towards AI-Assisted Synthesis of Verified Dafny Methodscited by 58
  6. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  7. 2024DafnyBench: A Benchmark for Formal Software Verificationcited by 54
  8. 2023Verus: Verifying Rust Programs using Linear Ghost Types (extended version)cited by 50
  9. 2024AutoVerus: Automated Proof Generation for Rust Codecited by 46
  10. 2023WhiteFox: White-Box Compiler Fuzzing Empowered by Large Language Modelscited by 37
  11. 2024AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinementcited by 33
  12. 2024Automated Proof Generation for Rust Code via Self-Evolutioncited by 31
10 more
  1. 2024Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verificationcited by 25
  2. 2025KNighter: Transforming Static Analysis with LLM-Synthesized Checkerscited by 22
  3. 2024Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programmingcited by 19
  4. 2025VeriPlan: Integrating Formal Verification and LLMs into End-User Planningcited by 19
  5. 2023KernelGPT: Enhanced Kernel Fuzzing via Large Language Modelscited by 17
  6. 2025VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Veruscited by 8
  7. 2022Aeneas: Rust Verification by Functional Translationcited by 7
  8. 2025Saarthi: The First AI Formal Verification Engineercited by 7
  9. 2025Towards Repository-Level Program Verification with Large Language Modelscited by 4
  10. 2025What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Veruscited by 1

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2026: 11.

11 papers.

  1. 2026AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithmscited by 11
  2. 2026interwhen: A Generalizable Framework for Steering Reasoning Models with Test-time Verificationcited by 2
  3. 2026Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalizationcited by 2
  4. 2026ExVerus: Verus Proof Repair via Counterexample Reasoningcited by 1
  5. 2026VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generationcited by 1
  6. 2026From Noisy Traces to Root Causes: Structural Trajectory Analysis and Causal Extraction for Agent Optimizationcited by 1
  7. 2026P3: Joint Program-and-Proof Planning for Verified Code Generationcited by 1
  8. 2026Vero: Can AI Agents Build Formally Verified Software Repositories?cited by 1
  9. 2026Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thoughtcited by 0
  10. 2026An AI Approach to Verified Production Cryptographic Librariescited by 0
  11. 2026Fewer Assumptions by Design: A Reusable Skill for LLM-Assisted Verus Verificationcited 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. 2026Automating Formal Verification with Agent-Guided Tree Search
  3. 2026KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code
  4. 2026Evaluating and Improving Automated Repository-Level Rust Issue Resolution with LLM-based Agents
  5. 2026Harnessing Code Agents for Automatic Software Verification
  6. 2026SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs?
  7. 2026Verification as an Architectural Layer for LLM Agents: A V-Model Design, and a Pilot Study of Its Deterministic Core
  8. 2025TypePilot: Leveraging the Scala Type System for Secure LLM-generated Code