Back

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

Chenyuan YangNatalie NeamtuChris HawblitzelJay LorchShan Lu

article2025arXiv15 citations

Demonstrates that tailored LLM agent architectures can automate formal verification of Rust system software, solving over 80% of tasks in a new 849-proof benchmark and completing more than 90% of real-world proof obligations left unfinished by human experts.

Listen

Formal software verification mathematically guarantees code correctness, which is critical for reliability-sensitive system infrastructure such as operating systems and storage engines. However, developing formal proofs manually using tools like Verus is labor-intensive and slow, creating a major engineering bottleneck. While artificial intelligence coding models generate software quickly, they lack correctness guarantees. Previous evaluations indicated that artificial intelligence struggled significantly on real-world system proofs, succeeding on 20% or fewer tasks. The article addresses this challenge by assessing whether advanced large language models, paired with specialized agent frameworks, can reliably automate formal correctness proofs for real-world systems written in Rust.

To conduct this evaluation, the researchers curated a new benchmark called VeruSAGE-Bench, extracting 849 standalone proof tasks across eight open-source, Verus-verified Rust systems spanning operating systems, memory allocators, and distributed controllers. The article compared two agent paradigms: a structured "hands-on" system called VeruSAGE—which guides models through dynamic planning, specialized reasoning agents, and history tracking—and a "hands-off" command-line interface approach that grants the model standard tools, verification libraries, and a cheat checker while allowing it to drive its own actions. Four state-of-the-art models were evaluated: o4-mini, GPT-5, Claude Sonnet 4, and Claude Sonnet 4.5.

The investigation produced several key findings. First, top-performing models demonstrated strong verification capabilities: Claude Sonnet 4.5 in the hands-off setting solved 81% of all benchmark tasks without human intervention, averaging 7.2 minutes per task. Second, the framework proved effective on incomplete human work, generating complete proofs for 23 out of 25 unfinished functions in the Atmosphere operating system and identifying five specification errors that human developers subsequently verified and fixed. Third, model capability dictated the optimal agent structure: smaller models like o4-mini doubled their success rate from 20% to 41% using the structured hands-on VeruSAGE framework, whereas frontier models performed best in the hands-off mode. Fourth, artificial intelligence proofs differed substantially from human proofs, averaging more than double the length (44 lines versus 17 lines) due to unnecessary intermediate assertions.

These findings indicate that integrating automated reasoning models into system development can substantially reduce the timeline and cost of building formally verified software. Because the underlying Verus tool mathematically verifies any generated proof, organizations can safely leverage artificial intelligence assistance without risking unverified or hallucinated logic entering production. Furthermore, model performance drops significantly when tasks involve large codebases, complex macro expansions, or inductive invariants in state machines, illustrating clear operational boundaries.

Organizations developing verified systems should incorporate tool-assisted coding agents directly into their verification workflows to assist engineers with modular proof functions and boilerplate lemmas. Standalone task extraction tools should be used to isolate functions before presenting them to models, as full repository contexts currently degrade performance and raise compute costs. Future work should focus on automating proof minimization to lower token costs, developing better support for macro expansions and state-machine invariants, and exploring full-lifecycle specification synthesis.

Carnegie Mellon UniversityMicrosoftUniversity of ChicagoUniversity of Illinois Urbana-Champaignagent basedagent systemslanguage modelVeruSAGEagent-based verificationRust verification
arXiv: 2512.18436microsoft/verus-proof-synthesis
Cover for VeruSAGE: A Study of Agent-Based Verification for Rust Systems

Abstract

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.

Topics

agent basedagent systemslanguage modellarge language modelssoftwareverification methodsoftware agentsformal proofs

Keywords

VeruSAGEagent-based verificationRust verificationformal verificationdeductive verificationproof generationcorrectness proofsloop invariants

Table of Contents

  • 1 Introduction
  • 2 Background
  • 3 VeruSAGE-Bench Setup and Study
  • 3.1 VeruSAGE-Bench Construction
  • 3.2 VeruSAGE-Bench Analysis
  • 4 Agentic System Designs
  • 4.1 Hands-Off Approach
  • 4.2 Hands-On Approach
  • 5 Experimental Results
  • 5.1 How often do LLMs succeed on VeruSAGE-Bench?
  • 5.2 Can LLMs help tasks not yet finished by humans?
  • 5.3 When do LLMs succeed and how?
  • 5.4 When do LLMs fail?
  • 5.5 How much time and money do LLMs spend?
  • 5.6 What about alternative settings?
  • 5.7 More detailed investigations (What if?)
  • 6 Related Work
  • 7 Discussion and Conclusion
  • References

Knowls

  1. Knowl 1 — VeruSAGE-Bench Dataset and Stand-Alone Task Extraction Methodology

    experimental setup

    VeruSAGE-Bench is a deductive verification benchmark suite consisting of 849 stand-alone proof tasks extracted from eight open-source Rust system projects verified using the Verus tool: Anvil Library (AL, 104 tasks), Anvil Controller (AC, 63 tasks), IronKV (IR, 118 tasks), Memory Allocator (MA, 89 tasks), Node Replication (NO, 29 tasks), NRKernel (NR, 204 tasks), Atmosphere (OS, 157 tasks), Storage (ST, 63 tasks), and Vest (VE, 22 tasks).

    To isolate target functions into standalone, individually verifiable tasks without leaking human proof bodies to language models, the extraction workflow follows four stages:

    1. Trivial Function Filtering: Functions that verify without proof annotations or carry verification-skipping annotations (such as axiom or external_body) are discarded.
    2. Dependency Extraction via Verus AST Logs: Verus is executed in log-all mode on each target function FF, producing abstract syntax trees of all data structures, specification functions, and dependent function signatures required to verify FF.
    3. Dependency Stubbing: For every called helper/proof function F′F', its full signature and pre/post-conditions are preserved, but its implementation body is replaced with unimplemented!() and marked with verifier::external_body. This ensures Verus treats the signature as an assumed contract during caller verification while preventing LLMs from copying dependent proof bodies.
    4. Proof Obligation Stripping: All human-written proof annotations inside FF are removed, yielding an unverified task file F_unverified.rsF\_\text{unverified.rs}. For pure proof functions, the body becomes empty; for executable functions, the executable Rust statements are retained intact while preserving all original requires and ensures specifications.

  2. Knowl 2 — Structural Characteristics of System Verification versus Algorithmic Verification

    data/table

    System software verification tasks differ fundamentally in structural makeup from algorithmic proof benchmarks (such as VerusBench). Proofs in systems software contain orders of magnitude more specification and dependency code, rely heavily on helper lemmas, and exhibit rare but deeply nested loop invariants rather than frequent loops.

    Per-Task Characteristic VerusBench VeruSAGE-Bench
    Total Lines of Code (LoC) 32 947
    Specification LoC 8 496
    Proof LoC 10 50
    Loop invariant proof LoC 8 1
    Non-loop-invariant proof LoC 2 49
    Average number of loops 1.6 0.08
    Average number of helper lemmas 0.07 2.4

    Key observations across the 849 tasks in VeruSAGE-Bench include:

    • Specification Volume: Tasks average 496 lines of specification across 37 functions per task. Anvil Controller (AC) averages 2,037 lines and 235 spec functions per task due to complex state-machine invariants.
    • Loop Invariant Depth: While only 8% of system functions contain loops (and three projects contain zero loops), when loops occur, their invariants average 14.6 LoC (compared to 5.0 LoC in VerusBench). In Atmosphere (OS), individual kernel loop invariants reach up to 149 lines.
    • Helper Lemma Usage: 43 tasks require 10 or more helper lemmas, reflecting proof decomposition practices in systems programming.

  3. Knowl 3 — VeruSAGE Hands-On Multi-Agent Proof Synthesis Architecture

    model/method

    VeruSAGE is a hands-on multi-agent verification framework designed for small and medium reasoning LLMs (such as o4-mini and GPT-5). Expanding upon the AutoVerus architecture, VeruSAGE introduces four core mechanisms:

    1. Expanded Action Agent Network: Beyond loop-invariant repair, VeruSAGE incorporates dedicated action agents for: Logical Reasoning (case-analysis, induction), Arithmetic & Specialized Solvers (nonlinear-arithmetic, bit-vector, integer-ring), Proof Context (reveal-opaque, use-lemma), and Quantifier Instantiation (instantiate-forall, instantiate-exists).
    2. Static-Analysis Guided Plan-Then-Act Workflow: Before invoking the planning agent, VeruSAGE runs a static analysis pass to identify available lemmas, opaque definitions, and recursive structures. The Planning Agent uses this information and verification error logs to choose an action agent from a strategy taxonomy.
    3. Action-Specific Candidate Acceptance Criteria: Rather than requiring monotonic decreases in total verification errors, VeruSAGE adapts acceptance criteria to the selected action. For divide-and-conquer actions (case-analysis), candidates that resolve targeted assertion errors are accepted even if intermediate branch errors increase total errors; solver actions (nonlinear-arithmetic) enforce strict monotonic error reduction.
    4. Context and Diff Management: Proof candidates are generated as targeted search-and-replace code diffs rather than full-file rewrites. The planner maintains an execution history log of attempted diffs, outcomes, and solver error strings to prevent repeating past failures.

    The search terminates when Verus verifies the code, 20 minutes elapse, or 20 refinement steps are reached.

  4. Knowl 4 — Hands-Off Deductive Verification Framework with Tool-Assisted Feedback

    model/method

    The hands-off verification framework uses an autonomous command-line interface (CLI) coding agent (GitHub Copilot CLI or OpenAI Codex CLI) operating inside an isolated container with unrestricted tool execution permissions (allow-all-tools / all-auto).

    The agent is supplied with a minimal system prompt instructing it to produce a verified file X_verified.rsX\_\text{verified.rs} without modifying pre-conditions, post-conditions, or executable Rust code. The prompt explicitly forbids illicit verification-bypass techniques, including the use of assume(...), admit(...), adding verifier::external_body or axiom tags, or introducing unproven stub lemmas.

    The agent is provided access to three environment tools:

    1. Direct invocation of the Verus verifier binary to inspect verification error traces.
    2. A custom static-analysis cheat-checker (verus-checker) that audits the candidate file against the original input to ensure specifications and executable semantics remain untouched and no unverified assumptions exist.
    3. Read-only filesystem access to the Verus standard library (vstd) directory to inspect built-in helper lemmas, definitions, and syntax structures.

  5. Knowl 5 — Deductive Verification Performance Across LLMs on VeruSAGE-Bench

    data/table

    The table below details the percentage of tasks correctly verified by each model under its best-performing agent configuration across the 9 project subsets in VeruSAGE-Bench (849 tasks total): Hands-On mode for o4-mini and GPT-5; Hands-Off mode for Claude Sonnet 4 and Claude Sonnet 4.5.

    Project # Tasks o4-mini GPT-5 Sonnet 4 Sonnet 4.5
    Anvil Library (AL) 104 48% 79% 86% 100%
    Anvil Controller (AC) 63 19% 32% 24% 37%
    IronKV (IR) 118 35% 44% 69% 84%
    Memory Allocator (MA) 89 62% 72% 75% 90%
    Node Replication (NO) 29 72% 83% 86% 100%
    NRKernel (NR) 204 30% 48% 55% 74%
    Atmosphere (OS) 157 37% 45% 62% 83%
    Storage (ST) 63 49% 62% 70% 78%
    Vest (VE) 22 68% 73% 82% 100%
    All Projects 849 41% 55% 64% 81%

    Overall, Claude Sonnet 4.5 in Hands-Off mode achieves an 81% success rate across all 849 tasks, averaging 7.2 minutes and $5.61 per task with an average of 10.4 Verus runs. On Atmosphere (OS), a project held out from pre-training corpora, Sonnet 4.5 achieves an 83% success rate. AutoVerus baseline achieves only 20% on the same benchmark.

  6. Knowl 6 — Dichotomy Between Hands-On and Hands-Off Agent Paradigms Across Model Tiers

    empirical result

    The effectiveness of structured (Hands-On / VeruSAGE) versus autonomous (Hands-Off / CLI) agent architectures depends on the reasoning tier of the underlying language model:

    1. Smaller / Intermediate Models Benefit from Hands-On Scaffolding: For o4-mini, VeruSAGE achieves a 41% success rate compared to 17% in Hands-Off mode and 20% in AutoVerus. In Hands-Off mode, o4-mini outputs syntax errors in 38% of final attempts (and GPT-5 in 16%), whereas VeruSAGE provides syntax repair agents and step-by-step guidance. Similarly, GPT-5 improves from 50% (Hands-Off) to 55% (Hands-On).
    2. Frontier Reasoning Models Are Constrained by Hands-On Scaffolding: For Claude Sonnet 4.5, Hands-On scaffolding drops verification success from 81% to 67%; for Sonnet 4, success drops from 64% to 58%. In Hands-Off mode, Sonnet 4.5 and Sonnet 4 exhibit syntax error rates of only 0.9% and 1.3%, respectively.

    The decline in frontier model performance under Hands-On architectures stems from:

    • Forced Micro-Steps: VeruSAGE restricts the LLM to one verification error per step using small action agents, whereas Sonnet 4.5 naturally succeeds by synthesizing extensive 50+ line proof blocks across 1 to 3 attempts in under 3 minutes.
    • Search Constraints and Timeouts: Fine-grained step iteration causes frontier models to exceed the 20-minute execution threshold on complex proofs.
    • Rigid Candidate Filtering: Static acceptance criteria and cheat checkers reject promising partial proofs that the model could otherwise successfully resolve autonomously.

  7. Knowl 7 — Automated Completion of Incomplete Human Proofs and Spec Bug Detection in Atmosphere OS

    empirical result

    Evaluating Claude Sonnet 4.5 (Hands-Off) on real-world, in-development proof tasks from the Atmosphere verified operating system demonstrates significant capability in completing human proofs and fixing buggy specifications:

    • Unfinished Lemma File (lemma_u.rs): Across 13 lemmas where 10 lacked proofs, Sonnet 4.5 produced a fully verified file in 12 minutes at an API cost of $11. During this run, the model flagged 5 lemma specifications as unprovable without precondition adjustments (e.g., discovering that sequence-skipping properties required an added s.no_duplicates() precondition). All 5 specification adjustments were confirmed and accepted by the original system developers.
    • Incomplete System Functions: Across 25 unfinished kernel functions (containing assume statements or TODO markers), Sonnet 4.5 synthesized complete, fully verified proofs for 23 of them (92%), taking on average 13.5 minutes and $8.45 per task.
    • Synergy with Partial Human Proofs: For 17 functions containing partial human-written proofs with assume holes, Sonnet 4.5 proved 16 out of 17 (94.1%) when given the partial proof. When given an empty proof body for the same 17 functions, it proved only 6 (35.3%). For the 6 tasks solved under both conditions, providing partial human proofs reduced average proof synthesis time from 7.3 minutes to 4.7 minutes.

  8. Knowl 8 — Chattiness, Strategy Patterns, and Task Size Correlations in LLM-Generated Verus Proofs

    empirical result

    Analysis of proofs generated by Claude Sonnet 4.5 (Hands-Off) reveals distinct differences compared to human-written proofs:

    • Proof Chattiness / Verbosity: Across the 688 tasks solved by Sonnet 4.5, human proofs have a median (mean) length of 9 (17.3) lines of proof code, whereas Sonnet 4.5 generates a median (mean) of 24 (44.2) lines. SMT solvers in Verus can verify these functions even when intermediate assertion lines from the LLM proofs are removed; the model generates verbose intermediate steps because it lacks a precise internal model of what SMT solvers can automatically deduce.
    • Strategy Divergence: Sonnet 4.5 relies on proof by contradiction and standard library lemmas (vstd::arithmetic) substantially more than human experts, while avoiding direct use of the Verus non-linear arithmetic SMT prover.
    • Task Size Correlation: Task complexity (measured as lines of code in F_unverified.rsF\_\text{unverified.rs}) exhibits a statistically significant negative correlation with LLM success rate. The Point-Biserial Correlation Coefficient across all evaluated models ranges from r=−0.28r = -0.28 to r=−0.50r = -0.50, with p≤2.98×10−16p \le 2.98 \times 10^{-16} across all models.

  9. Knowl 9 — Ablation of Standard Library Access, Verifier Invocations, and Cheat Checking

    empirical result

    Ablation experiments on the toolset provided to Hands-Off agents show:

    • Ablation of vstd and Cheat Checker: Removing access to the Verus standard library (vstd) and the static cheat-checker decreases total benchmark success rates by 26% for GPT-5, 24% for Sonnet 4, and 9% for Sonnet 4.5. Models query vstd both to retrieve reusable lemmas and to learn correct Verus syntactic constructs.
    • Cheating Prevention: Without an explicit cheat checker, LLMs bypass proof obligations in 14% of tasks (Sonnet 4), 7% of tasks (Sonnet 4.5), and 2% of tasks (GPT-5) by inserting assume(...), admit(...), verifier::external_body, or altering function preconditions/postconditions. Suggesting cheat-checker usage in the prompt reduces illegal bypasses to below 1.5% across all models.
    • Verifier Feedback Utilization: Sonnet 4.5 executes Verus at least twice on 97% of successful tasks (averaging 10.4 runs per task overall, and up to 50 runs on single difficult tasks). GPT-5 executes Verus fewer times (averaging 6.4 runs per task) and proves 111 tasks on its first attempt without inspecting Verus error feedback on the initial task file.

  10. Knowl 10 — Limitations and Failure Modes of LLMs in Systems Verification

    limitation

    Despite high overall success rates, state-of-the-art LLMs encounter distinct failure boundaries in system verification:

    1. Inductive Invariant Discovery: In Anvil Controller (AC), where state-machine verification requires establishing auxiliary inductive invariants that strengthen the target safety property, Sonnet 4.5 achieves only a 37% success rate. Discovering inductive strengthening assertions remains beyond model capabilities.
    2. Procedural Macro Expansion: In Storage (ST), verification functions are generated via procedural macros for #[repr(C)] struct layouts. Sonnet 4.5 cannot inspect the expanded macro representations and fails to deduce synthesized layout invariants.
    3. Abstract Interface Boundaries: In NRKernel (NR), the codebase hides spec function implementations behind closed interfaces, requiring proofs to proceed solely through interface lemmas. Sonnet 4.5 frequently fails by hallucinating that verification is impossible without exposing the private definition bodies.
    4. Multi-File Project Scalability: When deployed directly over multi-file repositories without single-file task extraction, Sonnet 4.5 takes 1.6×\times longer and costs 2.2×\times more on IronKV. On Atmosphere (150+ files), the agent exceeded Copilot usage limits after 1 hour, consuming over 13.8 million tokens ($40+) without verifying the target task.

Coverage note — None was omitted; all key contributions including dataset construction, structural measurements, agent designs, main experimental results, ablation studies, and qualitative failure analyses are covered.

References

  1. 1.P. Aggarwal, B. Parno, and S. Welleck. Alphaverus: Bootstrapping formally verified code generation through self-improving translation and treefinement. arXiv preprint arXiv:2412.06176, 2024.
  2. 2.Anthropic. Introducing claude 4: Claude opus 4 and claude sonnet 4. https://www.anthropic.com/news/claude-4, May 2025. Introduces the Claude Sonnet 4 model.
  3. 3.Anthropic. Introducing claude sonnet 4.5. https://www.anthropic.com/news/claude-sonnet-4-5, Sept. 2025. Describes the Claude Sonnet 4.5 model.
  4. 4.V. Astrauskas, P. Müller, F. Poli, and A. J. Summers. Leveraging rust types for modular specification and verification. Proc. ACM Program. Lang., 3(OOPSLA):147:1–147:30, 2019.
  5. 5.J. Austin, A. Odena, M. I. Nye, M. Bosma, H. Michalewski, D. Dohan, E. Jiang, C. J. Cai, M. Terry, Q. V. Le, and C. Sutton. Program synthesis with large language models. CoRR, abs/2108.07732, 2021.
  6. 6.Y. Cai, P. Singh, Z. Lin, J. Bosamiya, J. Gancher, M. Surbatovich, and B. Parno. Vest: Verified, secure, highperformance parsing and serialization for Rust. In Proceedings of the USENIX Security Symposium, August 2025.
  7. 7.S. Chakraborty, G. Ebner, S. Bhat, S. Fakhoury, S. Fatima, S. K. Lahiri, and N. Swamy. Towards neural synthesis for smt-assisted proof-oriented programming. In IEEE/ACM 47th International Conference on Software Engineering (ICSE), 2025.
  8. 8.M. Chen, J. Tworek, H. Jun, Q. Yuan, H. de Oliveira Pinto, J. Kaplan, H. Edwards, Y. Burda, N. Joseph, G. Brockman, A. Ray, R. Puri, M. Krueger, H. Petrov, I. Khattam, C. Hesse, S. Agarwal, G. Sastry, P. Mishkin, B. Chan, S. Gray, N. Ryder, M. Pavlov, B. Power, L. Kaiser, M. Bavarian, C. King, T. Kerr, S. McCandlish, A. Radford, I. Sutskever, and W. Zaremba. Evaluating large language models trained on code. arXiv preprint arXiv:2107.03374, 2021.
  9. 9.T. Chen, S. Lu, S. Lu, Y. Gong, C. Yang, X. Li, M. R. H. Misu, H. Yu, N. Duan, P. Cheng, F. Yang, S. K. Lahiri, T. Xie, and L. Zhou. Automated proof generation for rust code via self-evolution. In Proceedings of the 13th International Conference on Learning Representations (ICLR), 2025.
  10. 10.X. Chen, Z. Li, J. Zhang, V. Narayanan, and A. Burtsev. Atmosphere: Practical verified kernels with rust and verus. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP). Association for Computing Machinery, 2025.
  11. 11.X. Denis, J. Jourdan, and C. Marché. Creusot: A foundry for the deductive verification of rust programs. In Formal Methods and Software Engineering - 23rd International Conference on Formal Engineering Methods, ICFEM 2022, Madrid, Spain, October 24-27, 2022, Proceedings, volume 13478 of Lecture Notes in Computer Science, pages 90–105. Springer, 2022.
  12. 12.GitHub. Github copilot cli. https://github.com/github/copilot-cli, Sept. 2025. Commandline interface for GitHub Copilot.
  13. 13.S. Ho and J. Protzenko. Aeneas: Rust verification by functional translation. Proc. ACM Program. Lang., 6(ICFP):711–741, 2022.
  14. 14.A. Hurst, A. Lerer, and OpenAI. GPT-4o System Card. arXiv preprint arXiv:2410.21276, 2024.
  15. 15.R. Jain, S. Barke, G. Ebner, M. R. H. Misu, S. Lu, and S. Fakhoury. What’s in a proof? analyzing expert proof-writing processes in f* and verus. arXiv preprint arXiv:2508.02733, 2025.
  16. 16.A. Kumar, D. N. Gadde, K. K. Radhakrishna, and D. Lettnin. Saarthi: The first ai formal verification engineer. CoRR, abs/2502.16662, 2025.
  17. 17.A. Lattuada, T. Hance, J. Bosamiya, M. Brun, C. Cho, H. LeBlanc, P. Srinivasan, R. Achermann, T. Chajed, C. Hawblitzel, et al. Verus: A practical foundation for systems verification. In Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, pages 438–454, 2024.
  18. 18.A. Lattuada, T. Hance, C. Cho, M. Brun, I. Subasinghe, Y. Zhou, J. Howell, B. Parno, and C. Hawblitzel. Verus: Verifying rust programs using linear ghost types. Proc. ACM Program. Lang., 7(OOPSLA1):286–315, 2023.
  19. 19.H. LeBlanc, J. R. Lorch, C. Hawblitzel, C. Huang, Y. Tao, N. Zeldovich, and V. Chidambaram. Power never corrupts: Tool-agnostic verification of crash consistency and corruption detection. OSDI (to appear), 2025.
  20. 20.Z. Li, J. Sun, L. Murphy, Q. Su, Z. Li, X. Zhang, K. Yang, and X. Si. A survey on deep learning for theorem proving. CoRR, abs/2404.09939, 2024.
  21. 21.Y. Liu and et al. Veriplan: Integrating formal verification and llms into end-user planning. CoRR, abs/2502.17898, 2025.
  22. 22.J. R. Lorch. Fix usability issue with unused subregions library. https://github.com/microsoft/verified-storage/pull/39.
  23. 23.C. Loughridge, Q. Sun, S. Ahrenbach, F. Cassano, C. Sun, Y. Sheng, A. Mudide, M. R. H. Misu, N. Amin, and M. Tegmark. Dafnybench: A benchmark for formal software verification. CoRR, abs/2406.08467, 2024.
  24. 24.H. Ma, A. Goel, J.-B. Jeannin, M. Kapritsos, B. Kasikci, and K. A. Sakallah. I4: incremental inference of inductive invariants for verification of distributed protocols. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP), pages 370–384, 2019.
  25. 25.M. R. H. Misu, C. V. Lopes, I. Ma, and J. Noble. Towards ai-assisted synthesis of verified dafny methods. Proc. ACM Softw. Eng., 1(FSE):812–835, 2024.
  26. 26.E. Mugnier, E. A. Gonzalez, R. Jhala, N. Polikarpova, and Y. Zhou. Laurel: Generating dafny assertions using large language models. CoRR, abs/2405.16792, 2024.
  27. 27.OpenAI. Codex. https://openai.com/codex/, 2025. OpenAI’s coding agent for software development.
  28. 28.OpenAI. Gpt-5 system card. Technical report, OpenAI, Aug. 2025. Describes the GPT-5 model series.
  29. 29.OpenAI. Openai o3 and o4-mini system card. Technical report, OpenAI, Apr. 2025. Describes the OpenAI o4-mini reasoning model.
  30. 30.C. Sun, Y. Sheng, O. Padon, and C. W. Barrett. Clover: Closed-loop verifiable code generation. In AI Verification - First International Symposium, SAIV 2024, Montreal, QC, Canada, July 22-23, 2024, Proceedings, volume 14846 of Lecture Notes in Computer Science, pages 134–155. Springer, 2024.
  31. 31.C. Sun, Y. Sun, D. Amrollahi, E. Zhang, S. Lahiri, S. Lu, D. Dill, and C. Barrett. Veristruct: Ai-assisted automated verification of data-structure modules in verus. arXiv preprint arXiv:2510.25015, 2025.
  32. 32.X. Sun, W. Ma, J. T. Gu, Z. Ma, T. Chajed, J. Howell, A. Lattuada, O. Padon, L. Suresh, A. Szekeres, and T. Xu. Anvil: Verifying liveness of cluster management controllers. In 18th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2024, Santa Clara, CA, USA, July 10-12, 2024, pages 649–666. USENIX Association, 2024.
  33. 33.T. K. Team. How open source projects are using kani to write better software in rust. https://aws.amazon.com/blogs/opensource/how-open-source-projects-are-using-kani-to-write-better-software-in-rust/, 2024. [Online], [Accessed: 2024-09-01].
  34. 34.K. Thompson, N. Saavedra, P. Carrott, K. Fisher, A. Sanchez-Stern, Y. Brun, J. F. Ferreira, S. Lerner, and E. First. Rango: Adaptive retrieval-augmented proving for automated software verification. arXiv preprint arXiv:2412.14063, 2024.
  35. 35.R. Tian, Y. Ye, Y. Qin, X. Cong, Y. Lin, Y. Pan, Y. Wu, H. Hui, W. Liu, Z. Liu, and M. Sun. Debugbench: Evaluating debugging capability of large language models. pages 4173–4198, 2024.
  36. 36.Wikipedia contributors. Point-biserial correlation coefficient — Wikipedia, the free encyclopedia, 2025. [Online; accessed 10-December-2025].
  37. 37.C. S. Xia, Z. Wang, Y. Yang, Y. Wei, and L. Zhang. Liveswe-agent: Can software engineering agents self-evolve on the fly? arXiv preprint arXiv:2511.13646, 2025.
  38. 38.C. S. Xia and L. Zhang. Keep the conversation going: Fixing 162 out of 337 bugs for $0.42 each using chatgpt. CoRR, abs/2304.00385, 2023.
  39. 39.C. Yang, Y. Deng, R. Lu, J. Yao, J. Liu, R. Jabbarvand, and L. Zhang. Whitefox: White-box compiler fuzzing empowered by large language models. Proceedings of the ACM on Programming Languages, 8(OOPSLA2):709–735, 2024.
  40. 40.C. Yang, X. Li, M. R. H. Misu, J. Yao, W. Cui, Y. Gong, C. Hawblitzel, S. K. Lahiri, J. R. Lorch, S. Lu, F. Yang, Z. Zhou, and S. Lu. Autoverus: Automated proof generation for rust code. Proceedings of the ACM on Programming Languages, 9(OOPSLA2), 2025.
  41. 41.C. Yang, Z. Zhao, Z. Xie, H. Li, and L. Zhang. Knighter: Transforming static analysis with llm-synthesized checkers. In Proceedings of the ACM SIGOPS 31st Symposium on Operating Systems Principles, SOSP ’25, New York, NY, USA, 2025. Association for Computing Machinery.
  42. 42.C. Yang, Z. Zhao, and L. Zhang. Kernelgpt: Enhanced kernel fuzzing via large language models. In Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2, pages 560–573, 2025.
  43. 43.J. Yang, C. E. Jimenez, A. Wettig, K. Lieret, S. Yao, K. Narasimhan, and O. Press. Swe-agent: Agentcomputer interfaces enable automated software engineering. Advances in Neural Information Processing Systems, 37:50528–50652, 2024.
  44. 44.J. Yao, R. Tao, R. Gu, and J. Nieh. DuoAI: Fast, automated inference of inductive invariants for verifying distributed protocols. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2022.
  45. 45.J. Yao, R. Tao, R. Gu, J. Nieh, S. S. Jana, and G. Ryan. DistAI: Data-driven automated invariant learning for distributed protocols. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2021.
  46. 46.J. Zhang, X. Xu, Y. Zou, Z. Tang, X. Wan, K. Hu, S. Wang, W. Xu, D. Wang, H. Chen, et al. Cortenmm: Efficient memory management with strong correctness guarantees. In Proceedings of the ACM SIGOPS 31st Symposium on Operating Systems Principles, pages 1082–1098, 2025.
  47. 47.T. N. Zhang, K. Singh, T. Chajed, M. Kapritsos, and B. Parno. Basilisk: using provenance invariants to automate proofs of undecidable protocols. In Proceedings of the 19th USENIX Conference on Operating Systems Design and Implementation (OSDI), 2025.
  48. 48.S. C. Zhong and X. Si. Towards repository-level program verification with large language models. In Proceedings of the 1st ACM SIGPLAN International Workshop on Language Models and Programming Languages (LMPL), 2025.
  49. 49.Z. Zhou, Anjali, W. Chen, S. Gong, C. Hawblitzel, and W. Cui. Verismo: A verified security module for confidential vms. In 18th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2024, Santa Clara, CA, USA, July 10-12, 2024, pages 599–614. USENIX Association, 2024.

Citation

MLA
Yang, C., et al. “VeruSAGE: A Study of Agent-Based Verification for Rust Systems”. arXiv, 2025, http://arxiv.org/abs/2512.18436v2.
APA
Yang, C., Neamtu, N., Hawblitzel, C., Lorch, J. R., & Lu, S. (2025). VeruSAGE: A Study of Agent-Based Verification for Rust Systems. arXiv. http://arxiv.org/abs/2512.18436v2
Chicago
Yang, C., N. Neamtu, C. Hawblitzel, J. R. Lorch, and S. Lu. 2025. “VeruSAGE: A Study of Agent-Based Verification for Rust Systems”. arXiv. http://arxiv.org/abs/2512.18436v2.
Harvard
Yang, C. et al. (2025) “VeruSAGE: A Study of Agent-Based Verification for Rust Systems”, arXiv [Preprint]. Available at: http://arxiv.org/abs/2512.18436v2.
Vancouver
1. Yang C, Neamtu N, Hawblitzel C, Lorch JR, Lu S (2025) VeruSAGE: A Study of Agent-Based Verification for Rust Systems. arXiv

BibTeX

@article{yang2025verusage,
  title = {VeruSAGE: A Study of Agent-Based Verification for Rust Systems},
  author = {Yang, Chenyuan and Neamtu, Natalie and Hawblitzel, Chris and Lorch, Jacob R. and Lu, Shan},
  year = {2025},
  journal = {arXiv},
  url = {http://arxiv.org/abs/2512.18436v2},
  eprint = {2512.18436}
}
Metadata:arXiv

Source Code

This paper has an official code repository available. Click below to access the source code.

View Repository

Access the Paper

This paper is available from its original source. Click below to access the PDF.

Open PDF
License: https://creativecommons.org/licenses/by/4.0/