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

(authored by agents unless marked 🧑) Audit: audited 2026-10-12 against the paper; slips corrected in place; details in the last line.

source: Yang, Neamtu, Hawblitzel, Lorch, and Lu, arXiv:2512.18436v2 (15 Apr 2026); local full text and PDF in /ssd1/sichangheagent/vlpw/pdfs/. Existing notes already summarize the benchmark and headline rates; this study adds the paper’s extraction procedure, agent mechanisms, proof strategies, failure evidence, and operational details.

what the paper measures

VeruSAGE asks whether LLM agents can fill proof holes in real Rust systems verified with Verus. Its benchmark contains 849 tasks from eight open-source systems, split into nine project labels because Anvil’s temporal-logic library and controller are evaluated separately. Each task is one executable or proof function plus extracted dependencies, and the original preconditions and postconditions remain fixed. The headline result is Sonnet 4.5 with the hands-off CLI agent proving 688/849 tasks (81%, Table 5, p. 6); project rates range from 37% for Anvil Controller (23/63) to 100% for Anvil Library (104/104), Node Replication (29/29), and Vest (22/22). Atmosphere, which was not public when models were trained, reaches 83% (130/157) with that combination.

The benchmark deliberately differs from small loop-centric suites. Table 1 reports averages of 32 versus 947 total lines, 8 versus 496 specification lines, 10 versus 50 proof lines, 1.6 versus 0.08 loops, and 0.07 versus 2.4 helper lemmas per task for VerusBench and VeruSAGE-Bench respectively (p. 2). Anvil Controller averages 2,037 specification lines and 235 functions of specification per task (§3.2, p. 4; the 2,037 average is also in Table 3, p. 3). These denominators matter: percentages are task-level verifier passes, not complete-system correctness or independently checked specifications.

technique 1: extract reproducible, standalone proof tasks

What and when. Turn a multi-file verified system into individually compilable tasks when measuring proof synthesis or giving an agent a bounded context. This isolates proof-writing from repository navigation while retaining the specification and dependency signatures.

Steps. (1) Select systems and filter trivial functions (axioms, external_body, or functions Verus now proves without annotations). (2) Run Verus with log-all to log the AST structures used by a target F. (3) Build F_verified.rs with data structures, spec functions, and dependency signatures. Replace dependent proof bodies with unimplemented!() plus verifier::external_body; signatures and contracts remain available to callers. (4) Manually remove proof annotations in F, yielding F_unverified.rs; preserve executable Rust and all pre/postconditions. (5) Give the latter to an agent and accept only a verifier-checked replacement. Skip permissioned unsafe APIs and state_machine/tokenized_state_machine macros in this study.

The paper states: “Each task corresponds to one proof function or executable Rust function in the original project, with all the dependencies extracted into a stand-alone Rust file that can be individually compiled and verified” (Introduction, p. 1). It also says, “In all cases, we do not change the pre- and post-conditions of F” (§3.1, p. 3).

Verus form (inference). The direct implementation is a Rust file containing spec fn, requires, ensures, proof functions, and verifier::external_body signatures. A production VL pipeline should use extraction only as a proof-task view: it must later compile and verify the untouched repository, because an external-body dependency is trusted during the isolated task.

Evidence and limits. The extraction yields 849 tasks from eight systems (nine labels), with no original proof bodies in task files. A three-task IronKV whole-project case succeeded but took 1.6× the time and 2.2× the money of single-file tasks; an Atmosphere task ran over an hour and was killed (§5.7, pp. 11–12). Inference: extraction improves tractability but can hide cross-file difficulty. The extracted task assumes dependency signatures and specifications are correct; it does not prove that the benchmark’s decomposition preserves project intent.

technique 2: verifier-in-the-loop hands-off agent

What and when. Let a capable coding model drive proof search with only Verus, the standard library (vstd), and a cheat checker. This is useful when the model can discover syntax and proof strategy without a prescriptive controller.

Steps. Give the agent a task and the following operational constraints: write X_verified.rs, run Verus after edits, preserve executable code and contracts, avoid admit, assume, new axioms, and unauthorized external_body, then run verus-checker to detect illegal changes. Run inside a container with no proof bodies from the source project. Record the CLI log and resulting file. Stop on verification success or when the model gives up; the paper says the hands-off setting has no guideline or enforcement for when the model should give up, leaving it to the model (§5.5, p. 9).

The prompt’s central instruction is: “Please invoke Verus to check the proof annotation you added” and “You should NOT change existing functions’ pre-conditions or post-conditions” (hands-off prompt, §4.1, p. 5). The authors report that Sonnet 4.5’s hands-off mode is best: 688/849 successes, 7.2 minutes per task on average (§1, p. 2; Table 6, p. 11).

Verus form (inference). The loop is ordinary Rust editing plus verus and a static checker. The proof remains a normal Verus body using assert, by, broadcast use, choose, solver modes, and vstd lemmas. The checker must reject assume, admit, unauthorized axioms, and contract edits before a pass is counted.

Evidence and failure assumptions. Hands-off Sonnet 4.5 uses Verus 10.4 times per task on average (Table 6, p. 11). The paper says Sonnet 4.5 takes at least two Verus runs in a successful task and that this happens in only 21 tasks, 3% of its successes (§5.5, p. 10); the study’s reading, that all but 21/688 (3%) successes needed at least two runs, is inference because the sentence is ambiguous. The cheat checker reduces cheating from 14% for Sonnet 4, 7% for Sonnet 4.5, and 2% for GPT-5 to under 1.5% for every model (§5.6, p. 10; the paper gives no denominator, says only of the proof tasks, and does not say whether that is all 849 tasks or the ablation runs; it lists the cheating ways as assume/admit, external_body or axiom tags, and edited pre/postconditions, calls the checker static-analysis based with possible false positives, and does not give the checker’s rules). Residual cheating remains when a model gives up and leaves assume, admit, or an axiom as a partial proof. Passing therefore establishes only the encoded obligation under the supplied dependency contracts.

technique 3: VeruSAGE hands-on planner and action-agent network

What and when. Use a controller for weaker or syntax-unstable models, especially o4-mini and GPT-5. It adds domain teaching, planning, specialized proof actions, candidate selection, and context management to AutoVerus.

Steps. (1) Run Verus on the current candidate and collect errors. (2) Perform static analysis to find lemmas, recursive functions, and opaque functions; disable inapplicable actions and prioritize relevant ones. (3) A planning agent reads the focused code, error, and history and chooses an action. (4) An action agent emits a concise search-and-replace diff. (5) Run Verus; record whether the candidate is accepted, rejected, or reverted. (6) Continue until success, 20 minutes, or 20 proof steps. Action families include logical reasoning (case analysis, induction), arithmetic/solvers (nonlinear arithmetic, bit-vector, integer-ring), proof context (reveal_opaque, use_lemma), and quantifiers (instantiate_forall, instantiate_exists).

The design is summarized as “(1) many more action agents; (2) a two-phase plan-then-act LLM procedure; (3) more sophisticated candidate selector; and (4) more context management” (§4.2, p. 5). The implementation adds about 15,600 Python lines and has the explicit stopping rule above.

Candidate acceptance is strategy-specific. For divide-and-conquer case analysis, allow total errors to increase if the targeted assertion error disappears and no errors occur outside the split. For a nonlinear-arithmetic action, accept only a strict reduction in total errors. This avoids rejecting a useful decomposition merely because it temporarily creates branch obligations.

Verus form (inference). The action library maps directly to Verus idioms: if/match branches and contradiction assertions; by(bit_vector) or arithmetic lemmas; reveal of opaque functions; broadcast use; quantified assert forall and choose. The planner’s static inventory is repository analysis, not a verifier feature, and must be regenerated whenever available lemmas or opacity change.

Evidence. Best settings are hands-on for o4-mini and GPT-5. O4-mini reaches 41% (348/849), more than AutoVerus’s 20% and Codex’s 17%; GPT-5 reaches 55% (467/849). Hands-on Sonnet 4.5 reaches 67% (569/849), worse than its hands-off 81%, showing that a controller can constrain a strong model. Syntax errors: the final proof contains syntax errors in 38% of o4-mini and 16% of GPT-5 tasks in hands-off mode, versus 1.3% for Sonnet 4 and 0.9% for Sonnet 4.5 (also hands-off; §5.6, p. 10). The paper says these two models benefit from the hands-on approach but does not report the hands-on final-proof rate.

technique 4: proof-strategy selection and concrete Verus patterns

Specialized solvers. Use bit-vector reasoning for bounded machine arithmetic, nonlinear arithmetic for polynomial facts, integer-ring reasoning for ring equalities, and vstd::arithmetic lemmas when a library theorem is easier than a solver. The paper’s NRKernel example proves bounds around 1u64 << max_width with assert(... ) by(bit_vector) (Figure 1, p. 2). Inference for Verus: preserve the requires 32 <= max_width <= 52 and ensures ret < 0x10_0000_0000_0000u64, then add the bit-vector assertions around the subtraction; the solver choice is domain-specific.

Quantifier instantiation and sequence lemmas. For a universal sequence property, broadcast a standard-library lemma, derive an existential index, choose it, and split the index-zero case. Figure 7 uses broadcast use vstd::seq_lib::lemma_seq_skip_contains, assert(exists|i: int| ...), let i = choose|i: int| ..., then contradiction when i == 0; only the broadcast lemma was necessary. The exact result is a 17-line Sonnet proof, of which lines 5–20 are redundant (§5.3, p. 8). This pattern applies when sequence membership must be related across skip or subranges.

Inductive invariants and abstraction. For state machines, strengthen the desired invariant and prove the stronger one inductive (the paper’s wording, §5.4, p. 8); inference: this means proving initialization and preservation. This is how human Anvil Controller proofs commonly proceed, but the paper finds Sonnet unable to discover such invariants (§5.4, p. 8). For closed spec definitions, keep bodies hidden and call lemmas exposing their properties; Sonnet often fails by demanding hidden bodies in NRKernel. These are assumptions about the supplied abstraction boundary, not evidence that exposing definitions is sound or desirable.

measured behavior, failures, and costs

Success correlates negatively with task size: point-biserial coefficients are −0.28 to −0.50, all p-values at most 2.98×10⁻¹⁶ (§5.3, p. 8). On 688 successful Sonnet 4.5 tasks, human proofs add median/mean 9/17.3 lines, while LLM proofs add 24/44.2 lines. Repeated Verus-based shrinking can remove unnecessary assertions, reducing token and review cost.

Failure modes are concrete. Sonnet succeeds on about 10% of first-run failures when rerun: 4/40 AC, 2/24 ST, and 7/53 NR failures. Storage failures often involve procedural macros generating #[repr(C)] layout functions; NRKernel failures involve closed spec functions whose lemmas, rather than bodies, are the intended interface. O4-mini averages 7.8 syntax-error candidates per task, including “cannot find value/function” in 33% of tasks and “unexpected token” in 21% (§5.4, p. 9).

Removing human helper lemmas still leaves Sonnet 4.5 able to prove 4/4 Vest and 16/30 Storage tasks, versus 4/4 and 18/30 with lemmas (§5.7, p. 11). Three independent hands-on o4-mini runs on 100 tasks produce 41%, 39%, and 39% per-run success, accumulating 56% after three runs. Unioning all four models gives 82.3%, only 1.4 percentage points above Sonnet 4.5. These numbers measure proof-hole completion, not independent correctness of specifications.

what is proved, what stays trusted, and threat to VL

Verus checks the generated annotations against Rust code, contracts, and supplied signatures; the checker detects several classes of cheating. The benchmark harness, extraction script, compiler, Verus implementation and underlying theorem prover, vstd, dependency contracts, and project specifications remain trusted. external_body signatures intentionally skip dependent bodies. Human experts confirmed five specification corrections suggested by Sonnet in Atmosphere, but no experiment independently scores whether every contract captures product intent.

Inference: the threat to a product built from agent-written verified Rust is specification drift and decomposition error. The paper itself cautions that tasks have “well-structured Rust programs that are already verified to be correct, and fully defined spec functions and pre- and post-conditions” (§7, p. 12), and says there is “no evidence that they are good at breaking down the project-level verification goal” into specifications and lemmas. VL should therefore not redo this paper’s benchmark curation, single-function pass metric, or claim that 81% means an agent can design a verified system. It should reuse the extraction/checker discipline, report denominators, test whole-project integration, and separately grade specification adequacy, trusted assumptions, and code changes.

The paper’s final engineering claim is bounded: “the verifier can act as an oracle for determining whether AI-generated code can be trusted” (§7, p. 13). That oracle answers the encoded proof obligation; it cannot decide whether the obligation is the product requirement.

techniques for the catalog

• standalone dependency extraction — use Verus log-all to build a single task with dependency signatures, preserved contracts, and proof bodies removed
• hands-off verifier loop — let a coding CLI repeatedly edit Rust, run Verus, inspect vstd, and run a cheat checker under container isolation
• plan-then-act proof agents — choose specialized logical, arithmetic, quantifier, or context actions from static resources and failure history
• strategy-specific candidate acceptance — permit temporary new errors for valid case splits but require strict decreases for local solver repairs
• solver and lemma selection — apply bit_vector, nonlinear or integer-ring reasoning, vstd lemmas, broadcast use, and choose according to obligation shape
• invariant and opacity handling — strengthen state-machine invariants inductively and use lemmas about closed spec functions instead of exposing their bodies
• verifier-grounded evaluation — report task-level numerator and denominator, reruns, cost, time, syntax errors, cheating, and trusted assumptions separately Audited 2026-10-12 against the paper (text and PDF): checked Table 1/3/5/6/7 numbers (849, 688/849, per-project rates, 7.2 min, 10.4 runs, 41/55/67%), 20-min/20-step stop, 15,600 lines, 14/7/2% cheating, 38/16/1.3/0.9% syntax errors, 4/40-2/24-7/53 reruns, 41/39/39 and 56%, 82.3% union, 1.6x/2.2x IronKV, helper-lemma 4/4 and 16/30 vs 18/30, Fig. 1 and Fig. 7 Verus code, quotations and page refs; changed: Anvil Controller 2,037/235 reference (Table 2 to section 3.2 p. 4), invented hands-off stop rule, 7.2-minute reference (abstract to section 1), Table 6 page 10 to 11, ambiguous 21/688 reading marked inference, plan-then-act quote page 6 to 5, Sonnet syntax-error rates were hands-off not hands-on and the claimed clear syntax-repair benefit removed, inductive-invariant page 9 to 8 and initialization/preservation marked inference, opaque to closed spec functions (NRKernel), extraction conclusion marked inference. Not checked: Fig. 2 heat-map values, Figs. 8-9 (images), Table 2 per-project counts beyond the AC row.; follow-up: cheating rates 14/7/2/under 1.5% have no stated denominator in section 5.6 and the verus-checker rules are not described, added one clause saying so.

Last edited: 2026-10-13