SeVerus: Context-Aware, Gamified Benchmarking for Rust Verification

S E V ERUS: Context-Aware, Gamified Benchmarking for Rust Verification Álvaro F. Silva1,† , Martim Afonso2,† , Nuno Saavedra2 , Emily First3 , Alexandra Mendes1 , João F. Ferreira4

arXiv:2611.07194v1 [cs.SE] 4 Nov 2026

1

Faculty of Engineering, University of Porto, Porto, Portugal {up201603524@up.pt, alexandra@archimendes.com} 2 INESC-ID & IST, University of Lisbon, Lisbon, Portugal {martim.afonso, nuno.saavedra}@tecnico.ulisboa.pt 3 Rutgers University, New Jersey, USA emily.first@rutgers.edu 4 INESC-ID and Faculty of Engineering, University of Porto, Porto, Portugal joao@joaoff.com

has emerged as an increasingly popular language [13], due in part to its emphasis on memory safety and performance. However, memory safety alone does not guarantee that a program satisfies its intended functional requirements [14]. Verus addresses this challenge by extending Rust [15] with deductive verification, allowing developers to specify and prove functional properties of their programs [16]. Although Verus uses SMT solvers [17] to automatically discharge verification conditions, complex proofs often require additional guidance, including loop invariants, intermediate assertions, and auxiliary lemmas. These proof artifacts may depend on other lemmas, giving rise to intricate proof dependencies that must be resolved to verify a program. Existing studies have evaluated the ability of coding agents to generate proofs for Verus programs. In particular, VeruSAGEBench [18] introduces a system-verification benchmark comprising 849 proof tasks extracted from eight open-source Verus repositories. The benchmark’s results demonstrate the strong capabilities of modern coding agents, with the best configuration in the original study solving more than 80% of the tasks. More recent models have reportedly achieved even higher success rates, with Claude Opus 4.5 solving 93.9% of tasks at an average cost of $13.65 per task [19]. While these results demonstrate substantial progress in automated proof generation, they leave open an important question: to what extent do existing benchmarks capture the challenges that verification agents face when auxiliary proof artifacts have not I. I NTRODUCTION Coding agents generate complex software with limited yet been developed? VeruSAGE-Bench does not fully capture the development human intervention [1], but establishing that their programs environment in which proof-generation agents would operate satisfy the intended requirements remains challenging [2], [3]. in real-world projects. First, each task is self-contained in a Formal verification offers strong correctness guarantees, but single file that includes the target lemma, the auxiliary lemmas constructing proofs often requires substantial human effort [4]– declarations it uses, and the specification functions and type [10]. Automating proof construction is therefore an important definitions they refer to. This setup effectively assumes that step towards enabling coding agents to produce verified agents already know which lemmas are relevant and can retrieve software [11], [12]. This challenge is relevant in systems all necessary context trivially, abstracting away the challenges programming, where correctness is critical and where Rust of navigating a repository and identifying relevant proof † These authors contributed equally. artifacts. Second, and more importantly, existing tasks assume

Abstract—Coding agents achieve high success rates on existing benchmarks for Verus, a verifier for Rust programs. These benchmarks typically provide the auxiliary lemmas needed to complete a proof. In practice, however, such lemmas must be discovered and proved. To capture this challenge, we present S E V ERUS, a context-aware technique to generate Verus benchmarks that organizes verification tasks into quests, each divided into levels in a gamified manner. Using the original proof dependencies in verified projects, S E V ERUS constructs one quest per verification target and progressively removes proof context to create individual levels. These levels range from the easiest, requiring completion of a single missing lemma, to the hardest, requiring a proof of the target without any supporting lemmas. An independent checker rejects changes to executable code, weakened specifications, and unsound proof constructs. A noisy binary search estimates the highest level that an agent can solve reliably. Applied to six open-source Verus projects, S E V ERUS generates 819 quests comprising 10,095 levels. Experiments with Codex using GPT-6 Sol and GPT-6 Luna, and with Claude Code using Sonnet 4.6, show that success decreases and cost increases as proof context is withdrawn. The strongest agent solves the final level of 52 of 60 sampled quests, yet can only reliably solve 35% of their levels, with failures concentrated in longer quests. Successful GPT6 Sol proofs rarely reproduce the withheld lemmas, using instead alternative proof decompositions. By systematically varying proof context, S E V ERUS provides a foundation for constructing verification benchmarks that can continue to challenge increasingly capable coding agents. Index Terms—formal verification, Verus, Rust, benchmarks, LLM agents, proof generation

that supporting lemmas have already been established. However, in practice, verifying a program may require developing multiple auxiliary lemmas that can themselves depend on further lemmas. Consequently, proving a target property may involve constructing an entire network of supporting proofs rather than completing a single isolated proof. We introduce S E V ERUS, a context-aware technique for gamified benchmarking of Rust verification agents. We define severification as the process of transforming an existing verified project into progressively harder verification tasks by systematically withdrawing its original proof context. An existing verified Rust project is severified by extracting dependencies among proof artifacts to frame evaluation as a game of proof construction. Each verification target defines a quest, organized into successive levels that progressively remove parts of the original proofs. Levels range from completing a single missing lemma to proving the target without its original supporting lemmas. Beyond completing a proof, the higher levels of a quest test whether an agent can decompose a target into intermediate lemmas, discharge the resulting proof obligations, and retrieve the relevant definitions and facts from a large repository. Applied to six open-source Verus projects, S E V ERUS produces S E V ERUS B ENCH -S TRIX, an initial benchmark of 819 quests and 10,095 levels. We evaluate Codex with GPT-6 Sol and GPT-6 Luna. One experiment also includes Claude Code with Sonnet 4.6. For all three models, success decreases and cost increases as proof context is withdrawn. Under a $5 budget per attempt, the strongest configuration solves the final level of 52 of 60 sampled quests, but reliably solves only 35% of their levels, with failures concentrated in longer quests. Successful GPT-6 Sol proofs rarely reproduce the withheld lemmas, instead using alternative proof decompositions. Research Questions. We address four research questions: RQ1: How does the availability of proof context affect agents’ verification success and cost? RQ2: To what extent can S E V ERUS generate challenging verification tasks? RQ3: How do agent-generated proofs differ from the original proofs? RQ4: How does agent behavior vary with the availability of proof context? Contributions. The main contributions of this paper are: S E V ERUS, a new context-aware technique for gamified benchmarking that constructs verification quests with systematically varied proof support. • S E V ERUS B ENCH -S TRIX , a benchmark constructed from six real-world repositories, comprising 819 quests and 10,095 levels (tasks). • A cost-bounded evaluation method based on noisy binary search that estimates reliable progress through quests without exhaustively evaluating all their levels. • An empirical evaluation using two state-of-the-art coding agents to investigate how proof context affects verification success, cost, generated proofs, and agent behavior. •

II. A N I LLUSTRATIVE E XAMPLE As a running example, we consider the function is_sorted, the reference solution to HumanEval/126 from the secure-foundations1 repository (Fig. 1, R box). Given a vector of integers, the function determines whether its elements are sorted in ascending order and no value occurs more than twice. Its Verus specification expresses these requirements through two universally quantified properties. Although the implementation is simple, its verification relies on 17 auxiliary lemmas, some depending on further lemmas. Without them, an agent must discover, state, and prove the lemmas itself. We show three of them. A. Proof dependencies Consider two lemmas directly used by is_sorted. The first, lemma_3eq_row_count_eq_greater_3 (L1 box in Fig. 1), states that three consecutive equal elements imply that the corresponding value occurs at least three times. The second, lemma_repeated_eq_imply_count (L2 box in Fig. 1), states that, in a sorted sequence without three consecutive equal elements, each value occurs at most twice. Both lemmas depend, directly or indirectly, on lemma_count_concat (L3 box in Fig. 1), which establishes that counting the occurrences of an element distributes over sequence concatenation. Thus, removing L3 affects multiple proof obligations, illustrating how the difficulty of verifying a function depends on the number of missing lemmas and also on their relationships. The second lemma additionally relies on a larger subgraph of supporting lemmas. The dependency graph in Fig. 1 illustrates these relationships. An edge from one symbol to another indicates that the former invokes the latter. B. A quest of verification tasks S E V ERUS introduces the idea of gamified benchmarking for Rust verification. For each verification target, it constructs a quest: a sequence of verification challenges called levels, each providing progressively less of the original proof context. This allows us to evaluate not only whether an agent can verify a target, but also how much proof support it requires. At each level, the verification target and its supporting lemmas can be in one of three states, illustrated in Fig. 2: proved (green), meaning the original proof is retained; admitted (orange), meaning the statement is retained but its proof is removed to be reconstructed; or hidden (dashed), meaning the lemma is removed entirely, requiring the agent to discover its own auxiliary reasoning. Fig. 2 illustrates six of the 24 levels generated for the is_sorted function from Fig. 1. At Level 1, nearly all the original proof context is available, leaving only a single lemma for the agent to prove. As levels increase, more proof support is withdrawn. By Level 22, both lemmas directly supporting the executable function are admitted, while their shared supporting 1 https://github.com/secure-foundations/human-eval-verus/blob/main/tasks/ human eval 126.rs

R: executable function is_sorted fn is_sorted(v: Vec<i32>) -> (ret: bool) ensures /* sorted && each value occurs at most twice */ { if v[i-2] == v[i-1] && v[i-1] == v[i] { proof { lemma_3eq_row_count_eq_greater_3(...); L1 } return false; } // ... assert forall|i: int| ... count(...) <= 2 by { lemma_repeated_eq_imply_count(...); L2 } true }

L1 : three consecutive equal values

L2 : no value occurs more than twice

proof fn lemma_3eq_row_count_eq_greater_3(...) requires /* three consecutive equal elements */ ensures count(v, v[i]) >= 3

proof fn lemma_repeated_eq_imply_count(...) requires /* sorted, with no three consecutive equal elements */ ensures count(v, v[w]) <= 2

L3 : shared supporting lemma

Dependency graph

proof fn lemma_count_concat(a, b, k) ensures count(a + b, k) == count(a, k) + count(b, k)

L1 L3

R L2

13 lemmas

Fig. 1: Simplified proof structure of is_sorted. The executable root R uses L1 and L2 , which both depend, directly or indirectly, on the shared lemma L3 . Ellipses mark omitted code, and contracts are shown schematically (complete file). SeVerus · QUEST human_eval_126 · root R = is_sorted

20 symbols · 21 edges · 1 root ·

THE AGENT

LEVEL 1

QUEST BUILDER · expand()

EASY

R L1

24 LEVELS

LEVEL 19

lev 2–18 L2

LEVEL 20

R L1

L3

LEVEL 22

R L2

L3

L1

lev 21 L2

LEVEL 23

R L1

L3

LEVEL 24

R L2

L3

L1

L2

L3

HARD

R L1

1

admit

3

prove

2

L3 1st

Proved

Admitted

Hidden

admit

L2

4

2nd

recurse

path through L2’s subgraph

Fig. 2: The quest of is_sorted: six of its 24 levels (left) and the four steps of expand() that generate it (right).

lemma is hidden. At Level 23, the executable function itself also becomes a proof obligation. Finally, at Level 24, the agent must verify the executable function without its original proof annotations or supporting lemmas. This final level is called the root level. In general, a proof is removed exactly when its corresponding lemma or function is admitted or hidden. In this verification game, a root is the final boss; one needs to be an expert in proof decomposition and obligation dispatching to conquer it. The levels before it are intermediate bosses: each removes a different part of the original proof, so the agent must prove, rediscover, or rely on a different set of lemmas. III. T HE S E V ERUS B ENCHMARKING F RAMEWORK We describe how S E V ERUS generates the levels of a quest, how a submission is graded, and how an agent is scored. A. Task Generation Dependency Graph Construction. Given a verified Verus project, S E V ERUS constructs a directed dependency graph G = (V, E), where V contains the symbols of the project’s executable, proof, and specification functions, and E ⊆ V × V represents dependencies between them. An edge (u, v) ∈ E indicates that u invokes v. Each symbol has a unique identifier of the form <file>:<line>:<name> and a source span. We further distinguish a subset P ⊆ V of proof functions and lemmas, which represent explicit proof obligations. For the example of Fig. 1, |V | = 20 and |E| = 21.

Identification of Verification Targets. S E V ERUS identifies verification targets by analyzing the roots of the dependency graph. A root is a symbol on which no other symbol depends (i.e., no other symbol invokes it). Formally, given a dependency graph G = (V, E), a symbol r ∈ V is a root if it has no incoming edges, i.e., ∄u ∈ V : (u, r) ∈ E. Each root is the verification target of one quest. Throughout the paper, we refer to a quest’s root as its target. For projects with multiple roots, S E V ERUS generates an independent quest for each. We call the set of symbols reachable from a symbol in G its cone. To construct a quest, S E V ERUS considers only the cone of its root. In the running example (Fig. 1), the executable function is_sorted, denoted by R, is the sole root, as no other symbol depends on it. The cone of R contains L1 , L2 , and their supporting lemmas. Proof Context Transformations. To generate verification levels, S E V ERUS systematically varies the availability of proof artifacts while preserving the executable behavior and correctness requirements of the original program. S E V ERUS assigns each symbol one of three states: Proved, Admitted, or Hidden. Each state determines how the corresponding symbol is represented in the generated level: Proved. The symbol retains its original definition, including its implementation and proof annotations. The agent can rely on it without reproving it. • Admitted. The symbol retains its original signature and specification, but the agent must supply its removed proof.

•

Hidden. The symbol is removed entirely from the generated verify runs Verus on the project with the agent’s changes, project, with its specification and proof. and make anticheat guarantees soundness by ensuring The admitted state is implemented differently for proof that the agent has not modified the executable code, weakened functions and executable functions. For a proof function, the specifications, or introduced unsound shortcuts. Agents S E V ERUS replaces its body with an assume(false) stub, may add auxiliary lemmas and proof annotations, provided so other symbols can still reference the lemma. The stub is they verify. In general, attempting every level of every quest is an obligation the agent must discharge. For an executable expensive: quests reach hundreds of levels, and an attempt may function, S E V ERUS removes its proof annotations, including run out of budget. Also, because agents are nondeterministic, a proof blocks, assertions, loop invariants, and decreases clauses, single attempt is insufficient to reliably assess success near the while preserving its executable statements and specification. boundary between solvable and unsolvable levels. To account Executable functions are never hidden, since doing so would for this variability, S E V ERUS evaluates agents using a noisy binary search [20], which assumes that difficulty increases remove the program being verified. Quest Generation. For each root identified, S E V ERUS across levels, an assumption empirically supported by RQ1. constructs a quest (§III-A). The process starts with the root Noisy binary search. Let ψ(ℓ) denote the probability that an task, in which the target’s proof annotations are removed and agent solves level ℓ in a single attempt. Our goal is to estimate its supporting lemmas are hidden. S E V ERUS then progressively ℓ∗ = max{ℓ : ψ(ℓ) > 0.5}, the highest level at which the restores the original proof context through two state transitions: agent succeeds more often than it fails. If ψ is non-increasing admit, which changes a hidden symbol to admitted, and across levels, ℓ∗ also gives the number of levels with success prove, which changes an admitted symbol to proved. Each probability above 0.5. To estimate this threshold, S E V ERUS transformation step produces a new task, or level, of the quest. uses a noisy binary search. At each step, it runs up to three attempts on a level ℓ and determines whether ψ(ℓ) > 0.5 by A single step may admit multiple symbols simultaneously. Dependency-aware expansion. Quest generation follows majority vote. Each step halves the remaining search interval, a depth-first traversal of the root’s cone. For each symbol, requiring at most 3⌈log2 (n + 1)⌉ attempts for a quest of n S E V ERUS first admits the symbol and its immediate de- levels. The search narrows the estimated threshold to a single pendencies, then restores the symbol’s original proof, and level. finally recursively expands its dependencies. Dependencies are Benchmark score. For a quest q of nq levels, ℓ∗q = nq processed in decreasing order of cone size, so dependencies when the agent solves the root level. Simply averaging the with larger cones are explored first. This deterministic order per-quest scores ℓ∗q /nq gives equal weight to quests of different restores the largest withheld cone first, so a dependency shared lengths. Since short quests are both more numerous and often by several cones is restored inside the largest of them. The solved completely, they would disproportionately influence the right panel of Fig. 2 shows the expansion process on a symbol overall score. Instead, S E V ERUS weights each quest by its with two dependencies. number P ∗ of Plevels, computing the Reliable Level Score RLS = Level ordering. Levels are numbered in the reverse order q ℓq / q nq . Under the assumed difficulty ordering, RLS of generation. For a quest with n levels, Level 1 gives the estimates the proportion of benchmark levels that the agent most original proof support and Level n is the root task, with solves reliably. This weighting treats each level as a distinct the least. This order reflects the available proof context, not verification task: longer quests contribute more, much like conventional benchmarks in which projects contribute different necessarily difficulty, which RQ1 investigates empirically. numbers of tasks. Obligations of a level. At every level of a quest, the target is the root. The obligations of a level are all Admitted symbols IV. E XPERIMENTAL M ETHODOLOGY in the root’s cone, including the root itself. A level is solved A. Benchmark Construction and Characterization when all of them are proved. At Level 1, the root is Proved and a single lemma is Admitted, so that lemma is the only Projects. We severify six open-source Verus projects that cover obligation. The final level is the one where only the root is different kinds of systems software to build S E V ERUS B ENCH S TRIX (Table I). Admitted and all other dependencies are Hidden. We selected these projects because they are among the Illustrative example. For the running example in Fig. 1, largest open-source Verus-verified systems, including Anvil, the S E V ERUS generates a quest comprising 24 levels. The traversal largest [18]. All but TLA-RS appear in VeruSAGE-Bench [18]. expands L2 before L1, since L2 has a larger cone. Con- Of its other three projects, Memory Allocator and Node sequently, the shared lemma L3 is restored through L2’s Replication do not verify with any Verus release we could dependencies before the traversal reaches L1. Since L3 is build, and Atmosphere needs a custom Nix-based multi-crate already proved, it is not processed again. Fig. 2 shows the build, which we leave for future work. states of the four named symbols at selected levels. Generated quests. S E V ERUS generates one quest per root B. Agent Evaluation (§III-A). Severifying the six projects yields 819 quests with An attempt on a level is considered solved only if the agent’s 10,095 levels in total (Table I). Most quests are short. In five submission passes both verification and our anti-cheat: make projects the median quest has three to five levels, because most •

TABLE I: The S E V ERUS B ENCH -S TRIX benchmark. Full benchmark: Rust code size (kLOC), proof functions, quests (one per target), levels (one task each), and median/maximum quest length. Sample: total levels across the ten RQ2 quests per project, and minimum/maximum agent attempts required by noisy binary search. Full benchmark Project

Sample

kLOC Proofs Quests Levels Length Levels Attempts

Vest [21] IronKV [22], [23] PMemLog [23] NRKernel [23] TLA-RS [24] Anvil [25]

10.9 10.9 3.4 26.6 94.6 83.9

221 91 45 289 1,447 600

147 96 16 82 427 51

544 3 / 11 356 3 / 13 167 8.5 / 35 3,953 5 / 214 3,935 3 / 237 1,140 3 / 894

All

230.3

2,693

819 10,095

68 82 157 968 528 981

50–96 54–105 72–129 100–180 86–159 64–123

2,784

426–792

roots depend on only a few lemmas. A few quests are long, and they account for most of the levels. Evaluated sample. Running every level of every quest is not affordable, so we evaluate a sample of ten quests per project. For each project, we first take its longest quest, which RQ1 also uses. We then draw nine further quests at random with a fixed seed among the quests that have at least five levels, until the project has ten. The sample contains 2,784 levels, representing 28% of all benchmark levels. Long quests dominate the sample, meaning that most evaluated levels correspond to the projects’ main theorems. The last column of Table I shows that the search methodology used in RQ2 (§III-B) requires 426–792 attempts on the sample, compared with 10,095 attempts to evaluate every benchmark level once.

agent context and stops at a cost of $5 or after four hours. The task description tells the agent to keep working until the environment ends the attempt. A level is solved if the final submission passes both verification and the anti-cheat (§III-B). Task packaging. Each task is a Docker image whose workspace holds the modified sources, a Makefile with the verify and anticheat targets, and a task description. Original sources and grading metadata never enter the agent’s container. make anticheat is an independent Rust checker that compares the submission with the original project. It requires the non-ghost code of executable functions to be byte-identical, every requires and ensures clause to be unchanged, and the target’s dependency scope, computed from the call graph of the submission so that helpers the agent adds are included, to contain no assume(...), admit(), #[verifier::external_body] or #[verifier::admit]. Access to the original proofs. As the source projects are public, an agent with internet access might download the proof it is asked to rebuild. A preliminary GPT-6 Sol campaign did exactly this: in 11 attempts on NRKernel and Anvil, it cloned the original repository and copied its proofs. We discarded that campaign and ran Sol and Luna with the network restricted: the container can reach only the model API, web search is disabled, and the task description states that there is no internet access. Most Sonnet attempts predate the restriction; we checked their logs, and none used the network or read the grading metadata. V. E XPERIMENTAL R ESULTS RQ1 tests whether quest levels are ordered by difficulty, the assumption behind S E V ERUS’s scoring (§III-B). RQ2 applies this scoring method to 60 quests to assess agent performance. RQ3 compares the proofs of the solved attempts of RQ1 and RQ2 with the original proofs, and RQ4 examines how the agents produced them.

The longest quests. The root of each longest quest corresponds to a verification target with a large number of dependencies, typically representing a key correctness property of the project. At the root level, the agent must rebuild every proof in the root’s cone. On NRKernel (214 levels), the root unmap_aux removes a virtual address from the x86 page table A. RQ1: How does the availability of proof context affect and proves that the abstract map loses exactly that address agents’ verification success and cost? while the page-table invariants still hold. On Anvil (894 levels), Method. All levels of a quest share the target and its the root core_holds proves that four Kubernetes controllers specification. They differ only in how much of the original sharing one cluster are safe and eventually reach a stable proof they retain. Although higher levels are expected to be reconciliation, a liveness property. Our artifact [26] describes harder, difficulty does not necessarily increase monotonically. the longest quests of the other four projects. An Admitted lemma used by a Proved proof must be proved as stated, whereas a Hidden lemma may be replaced by an B. Agents and Execution Environment alternative. For example, in Fig. 2, if L1 is difficult but a Agents. We evaluate Codex [27] with GPT-6 Sol and GPT- simpler lemma would also suffice to prove R, Level 22 forces 6 Luna, and, in RQ1, also Claude Code [28] with Claude the agent to prove L1 . At the root level (Level 24), however, the Sonnet 4.6. We initially evaluated Sonnet 4.6, the latest agent may use the simpler lemma instead, potentially making version available through our API of the model used by the final boss easier than Level 22. VeruSAGE, the state-of-the-art system for automated Verus We test the null hypothesis that the probability ψ(ℓ) of proof generation [18], alongside GPT-6 Sol, a state-of-the-art solving Level ℓ remains constant across a quest against the model at the time of writing. Since GPT-6 Sol substantially alternative that it decreases as the level increases. We evaluate outperformed Sonnet 4.6, we selected it for the subsequent Claude Code with Sonnet 4.6 and Codex with GPT-6 Sol and experiments. We also evaluated GPT-6 Luna as a lower-cost GPT-6 Luna on the longest quest of each project, ranging from alternative to assess the performance of a more cost-effective 11 levels on Vest to 894 on Anvil. For each quest, we select model. Each attempt starts in a fresh container with a fresh 35 equally spaced levels in advance (or all levels if fewer) and

TABLE II: RQ1 per quest of n levels. Bold: furthest agent; ∗ : significant success decrease; τb on solved attempts (–: under three). Pooled: stratified Z for success decrease and cost increase.

results in too few attempts per agent near the transition point to reliably detect a performance decline. TLA-RS is the only quest where this transition is not sharp. Sol solves every level up to 112, fails the next four, and then still solves two of the five levels it attempts after the switch, up to level 218; Luna Highest solved τb (level, cost) Cost ($) alternates between successes and failures from level 84 up to Project (n) Sonnet Sol Luna Sonnet Sol Luna Sonnet Sol Luna level 223, so the highest solved level overstates where success Vest (11) 9∗ 11 11 .72 .75 .49 36 6.3 0.3 stops, which motivates the repeated attempts of the search used IronKV (13) 11∗ 13 13 .89 .79 .67 29 8.2 0.8 PMemLog (35) 29∗ 35 35 .69 .62 .70 115 20 2.7 in RQ2. We discuss why TLA-RS behaves differently in §V-B. NRKernel (214) 7∗ 64∗ 57∗ – .71 .82 50 74 16 The agents reach different failure points, with Sonnet never TLA-RS (237) 22∗ 218∗ 223∗ 1.00 .82 .83 54 67 18 surpassing the GPT-6 agents. On the three small projects, Anvil (894) 1 1 27∗ – – – 48 43 8.0 Sonnet fails before the root, while Sol and Luna solve every Pooled (Z) 5.7∗ 5.0∗ 4.6∗ 6.4∗ 8.2∗ 9.0∗ level. On NRKernel, Sol reaches Level 64 and Luna Level 57; Total 333 218 46 both reach high levels on TLA-RS, but only Luna progresses beyond Level 1 on Anvil. Paired comparisons confirm this ordering: Sol and Luna each solve about 20 levels that Sonnet make one attempt at each, starting at Level 1 and progressing fails, while Sonnet solves none that either fails (exact McNemar, toward the root. After four consecutive failures, we switch to p < 10−5 ). Sol and Luna are statistically indistinguishable. six equally spaced levels between the current level and the At its highest solved level, an agent proves the target and root, including the root. Once an agent stops succeeding, higher all supporting lemmas not provided at that level. On the three levels are also expected to fail, and failed attempts tend to be small projects, Sol and Luna rebuild the entire proof, and the most expensive. This expectation held for 40 of the 42 Sonnet most of it. On the larger projects, all agents rebuild attempts made after a switch, allowing us to save 160 attempts only part: Sol and Luna prove about 160 of 180 lemmas on across the three long quests. For NRKernel, TLA-RS, and TLA-RS, 47 and 42 of 153 on NRKernel, respectively, while Anvil, the grid samples only part of each quest, so we can on Anvil (655 lemmas), they prove the target only when almost locate where success stops only within the grid spacing of 6, the entire proof is provided. Since these quests are sampled, 7, and 26 levels, respectively. A trend on the sample reflects these counts are lower bounds. across the quest: the grid is fixed before any attempts, and Cost increases with level for all three agents on every project. only the switch depends on the outcomes, which the statistical For Sonnet and Sol, this is partly because nearly all failures test described below accounts for. The experiment comprised reach the $5 cap, but the trend also holds for successful attempts 332 attempts at a total cost of $597: 93 with Sonnet ($333), alone on quests with sufficient data (τb in Table II). Luna costs 115 with Sol ($218), and 124 with Luna ($46). about an order of magnitude less than Sol at every level, while For each quest, we test for a decrease in success across levels Sol is several times cheaper than Sonnet where both succeed. using the one-sided Mann–Kendall test [29], [30]. Since the Sonnet and Sol exhaust nearly the full budget on successes switch makes subsequent attempted levels outcome-dependent, just below the switch, so their failure points depend partly on we use α = 0.025 and validate through simulations that the the $5 cap. Luna never reaches the cap, so its failures cannot false-positive rate remains below 5% (see artifact [26]). We be attributed to the budget. aggregate the six quests per agent using the stratified Mann– Kendall test and compare agents using an exact McNemar Answer to RQ1: As proof context is withdrawn, success decreases test [31] on commonly attempted levels. To assess cost trends, and cost increases for all three agents (stratified tests, p < .001). Quest levels thus form a generally increasing, though not strictly we compute one-sided Kendall’s τb [32] between level and cost, monotonic, difficulty scale, with agents reaching different depths. both across all attempts and solved attempts only, as Sonnet and Sol failures almost always incur the full $5 cap. B. RQ2: To what extent can S E V ERUS generate challenging Success falls and cost rises with the level. The pooled row verification tasks? of Table II combines the six projects of each agent into one stratified test, which uses every attempt and is therefore our Method. We run the noisy binary search (§III-B) with GPT-6 strongest evidence. For all three agents success falls and cost Sol and GPT-6 Luna on the 60 quests of the evaluated sample, rises as the level rises, and cost rises also when only solved under the same conditions as in RQ1, and score each agent with RLS. The search skips most levels, so we first check it attempts are counted (all p < .001). ∗ Fig. 3 shows a similar pattern across almost all quests: agents on the longest quest of each project. We also estimate ℓ from solve the shallower levels but begin to fail beyond a certain the RQ1 attempts, with the isotonic-regression method of Oron depth. Successes and failures rarely intermingle, resulting in a and Flournoy [33], and compare the two. generally sharp transition. The Mann–Kendall test confirms a The search agrees with RQ1 grid. On the longest quests, decreasing success trend for most quests with varying outcomes search-derived ℓ∗ agrees with the RQ1 grid estimate for all 12 (Table II). The only exception is Anvil, where no statistically agent–quest pairs: both find the root solved on the three small significant trend is detected due to the sparse grid, which projects, and all estimates for the long quests fall within the

Claude Code + Sonnet 4.6

Codex + GPT-6 Sol

Codex + GPT-6 Luna

solved

not solved

Vest (n=11)

9/11 p=0.023 11/11 n/v 11/11 n/v

NRKernel (n=214)

2/11 p=0.023 11/20 p<.001 10/19 p<.001

IronKV (n=13)

11/13 p=0.019 13/13 n/v 13/13 n/v

TLA-RS (n=237)

4/13 p=0.003 19/26 p<.001 24/35 p<.001

PMemLog (n=35)

27/35 p<.001 35/35 n/v 35/35 n/v

Anvil (n=894)

1/10 p=0.082 1/10 p=0.082 2/11 p=0.023

0.0

0.2 0.4 0.6 0.8 Relative level (0 is level 1, 1 the root)

1.0

0.0

0.2 0.4 0.6 0.8 Relative level (0 is level 1, 1 the root)

1.0

Fig. 3: Outcome of each attempt by relative level (0 = Level 1, 1 = root). Filled markers indicate success. Right-hand labels report successful/total attempts and Mann–Kendall p-values (n/v: no variance, as all attempts succeeded). TABLE III: RQ2 results over the ten quests of each project. Root: quests solved up to the root. Mean: per-quest mean of ℓ∗ /n. Attempts: agent attempts the search made. RLS

Root

Mean

Project

Sol Luna

Sol Luna

Vest IronKV PMemLog NRKernel TLA-RS Anvil

10 10 10 5 8 9

10 1.00 10 1.00 10 1.00 4 .58 6 .89 9 .90

1.00 1.00 1.00 1.00 1.00 1.00 .55 .22 .87 .67 .90 .11

1.00 50 1.00 55 1.00 72 .22 113 .65 92 .12 69

50 16 55 32 72 26 116 372 102 181 68 140

1.7 6.4 4.9 91 38 20

All

52

49

.89

.35 451

463 768

162

.90

Attempts

Cost ($)

Sol Luna Sol Luna Sol Luna

.35

and 108) falls inside it, but with at most three attempts per probe the search cannot separate success probabilities that are too close across levels. The reason is that from level 112 to 223 every level asks for the same three inductive lemmas of the Raft safety proof. These lemmas are likely to dominate the success probability as every failure of Luna in this range fails on exactly these three, while the added lemmas are proved. Answer to RQ2: The strongest agent, GPT-6 Sol, solves 52 of 60 quests up to the root but only about a third of their levels (RLS = 0.35). GPT-6 Luna scores the same at a fifth of the cost. Almost all unsolved levels lie on the long quests of NRKernel, TLARS and Anvil. Results show that S E V ERUS generates challenging tasks even for the strongest agents.

grid’s 95% intervals. Search requires fewer attempts at similar cost (76 vs. 115 for Sol; 80 vs. 124 for Luna) while pinpointing C. RQ3: How do agent-generated proofs differ from the ℓ∗ to a single level rather than intervals spanning tens of levels. original proofs? It places Sol at levels 62/214 (NRKernel), 104/237 (TLA-RS), and 23/894 (Anvil), and Luna at 64, 108, and 27, respectively. Method. We measure how agent-generated proofs differ from the original solutions. While we cannot rule out that agents The full comparison is in our artifact [26]. helped write them, each project’s top contributors suggest that At the quest level, Sol appears close to solving the benchmost are at least human-revised. Only in TLA-RS, the most mark, reaching the root in 52 of 60 quests. At the level recent project, is an agent (Claude Code) the main contributor, granularity, however, it reliably solves only 35% of the levels while the other projects have few agent-made commits. We (RLS = 0.35). Sol solves every quest with fewer than 50 levels therefore report each analysis with and without TLA-RS. up to the root, and Luna all but two. Failures are concentrated We compare the proofs across the 267 passed tasks for in longer quests: all eight quests that Sol leaves unsolved have GPT-6 Sol, pooling the RQ1 and RQ2 walks and counting at least 86 levels. Luna performs nearly as well as Sol, solving each task once (averaging its repeated attempts). At each 49 quests up to the root versus Sol’s 52. The three additional level, we compare the agent’s solution with the omitted failures occur on NRKernel and TLA-RS. Sol reaches a higher set, i.e., the hidden lemmas, the admitted lemmas and the level on 6 quests, Luna on 5, and the remaining are ties. Both target proof. We consider only successful attempts, since achieve the same RLS = 0.35. an incomplete proof does not show whether the agent was Why TLA-RS behaves differently. TLA-RS quests are as converging towards a correct solution. For each task with long as NRKernel’s, yet agents solve most of their levels (RLS hidden lemmas, we compare the generated lemmas against 0.67 and 0.65, against 0.22), and their results are the least stable. the ground truth, grouping results into four categories: no Success still decreases significantly with the level (Table II), but new lemmas, different lemmas, some reused, and most reused. slowly: over a wide range of levels ψ(ℓ) appears to stay close to Matching is based on lemma statements, with names removed, one half, so attempts flip between success and failure, and RQ1 parameters α-renamed, and external anchors (vstd lemmas, still succeeds at levels 218 (Sol) and 223 (Luna). Estimating ℓ∗ spec functions, and types) preserved verbatim; proof bodies from the RQ1 attempts with a 95% confidence interval (details are excluded. Two lemmas share a statement key if and only in the supplementary material of our artifact [26]) gives an if their canonicalized statements match, regardless of name interval of about 100 levels on TLA-RS. The search’s ℓ∗ (104 or proof. Solutions are compared by the intersection of their

statement sets over their union: agent stmt ∩ human stmt stmt jaccard = agent stmt ∪ human stmt Re-stated recall measures the fraction of deleted reference statements matched by agent-generated lemmas, ignoring additional helpers. It captures reference-claim coverage and thus provides an upper bound on agreement, whereas the symmetric Jaccard also penalises extra agent lemmas. We also compare proof dependency structures through call graphs, identifying each lemma by its statement (as defined above). Ideally, two solutions should match if one can be transformed into the other by consistently renaming their own lemmas while preserving external anchors. We approximate this equivalence using the Weisfeiler–Leman (WL) colour-refinement algorithm [34]. Each node is initially coloured by its canonical statement, with names removed, parameters renamed, and external anchors preserved; proof bodies are discarded. We then iteratively refine node colours using the colours of the lemmas they call. Consequently, two nodes share a final colour if they express the same claim and depend on lemmas with matching colours, capturing equivalent dependency structures up to renaming. Each solution is represented by the multiset of its nodes’ final colours, and structural similarity is computed as the multiset Jaccard similarity between the resulting fingerprints:

TABLE IV: Reference deleted-lemma coverage on each project’s Hidden tasks. Re-stated recall measures one-sided coverage (ignoring extra agent helpers), while Hidden-only statement Jaccard measures symmetric overlap. GPT-6 Sol, RQ1+RQ2 pooled, one row per task. Vest Anvil IronKV TLA-RS NRKernel PMemLog Tasks 23 Recall 0.73 Jaccard 0.56

19 0.11 0.06

13 0.10 0.05

56 0.02 0.01

34 0.01 0.00

All

55 200 0.00 0.11 0.00 0.08

TLA-RS, whose solutions may have been influenced by the use of a coding agent. The similarity between agent-generated and human-written solutions declines sharply with depth: as more lemmas are withheld, the agent’s solution increasingly diverges from the reference in terms of both claims and structure. The gap between the two metrics further indicates that, even when agents reuse some of the same lemmas as the reference, they often place them in a different dependency context. Deeper levels are therefore less exposed to data contamination. Including TLA-RS has little effect on the overall results. Although it may have been influenced by a coding agent, we hypothesize that differences in the harness and model family account for the distinct characteristics of its proofs.

Coding Practices. Code duplication and assertion use give insight into proof conciseness and maintainability. Repeated #(shared colours) proof fragments may indicate a lack of possible abstraction or stmt graph = #(colours in either) reuse, while frequent assertions may reflect greater reliance where both counts are taken with multiplicity. We evaluate, on explicit intermediate facts to guide the prover. As neither within traces, how the increasing difficulty (represented by the metric is inherently undesirable (duplication can improve local clarity, and assertions can make proof steps more explicit), we depth) affects this similarity. Beyond this, we examine two aspects associated with proof treat them as complementary indicators of proof structure. Figure 6 reports assert density, the fraction of proof lines quality: assertion density and code duplication. For each proof, consisting of assertions. It increases on shallower tasks before we measure how much proof code is duplicated rather than plateauing, with agents exceeding the reference at every depth abstracted into reusable lemmas. We use a sliding window of except the deepest (0.30 vs. 0.24 overall; higher in 71% of 20 consecutive tokens, hashing each window and marking those tasks). As the measure is normalized by proof length, this whose normalized sequence occurs elsewhere in the solution, difference cannot be attributed simply to agents writing longer either within the same lemma or across different lemmas. proofs. It is present on the easiest levels and generally widens Statement and Graph Comparison. Figure 4 groups deleted- with depth. Including TLA-RS narrows the gap only in the cone tasks into four outcomes: no new lemmas, different deepest bin, which consists entirely of this project’s levels. lemmas, some re-stated lemmas, or most re-stated lemmas. TLA-RS has a corpus-wide density roughly twice that of any Across the 200 tasks whose target depends on deleted Hidden other project, suggesting that the apparent convergence in bins lemmas (the All projects bar), agents build no new lemmas reflects the project’s unusually high reference assert density, in 32%, entirely different lemmas in 53%, and re-state at rather than a change in agent behaviour. Excluding TLA-RS, least one in only 15%. Results vary by project: 15–58% of agents discharge proof obligations using a higher density of tasks involve no new lemmas, while statement reuse ranges intermediate assertions than the human-written references, and from substantial (Vest 48%, IronKV 23%) to virtually none this difference tends to increase with task depth. (PMemLog / NRKernel ≈ 0). Figure 7 shows that agent-generated proofs generally have a From Table IV we see that recall is the most lenient reading, higher block-clone ratio than human-written proofs across depth yet it is barely above the symmetric overlap (0.11 vs. 0.08 bins. This difference is absent for TLA-RS, whose commits pooled), so the low reproduction of lemmas is genuine rather were reportedly produced by coding agents. This suggests that than an artifact of penalizing extra helpers; the one exception is agent-generated proofs tend to contain more duplicated code, Vest, whose agents re-state three-quarters of the deleted claims. although the TLA-RS results indicate that this tendency may Figure 5 shows stmt jaccard and stmt graph across depend on the agent and its development setup. quest-depth bins, including results for all projects and excluding

32

All (200)

53 52

Vest (23)

17

31

IronKV (13)

9 31

46

8

58

Anvil (19)

21

20

TLA-RS (56)

82

0

3 62

50

No new lemmas

How it ends

10 19

38

PMemLog (55)

15 11

61

15

NRKernel (34)

TABLE V: How failed attempts end (left) and, for those the agent ends itself, why it stops (right), from a reading of every one of these stops. S: GPT-6 Sol, L: GPT-6 Luna.

6

New, some reused (<½)

Similarity to reference

0.8

All projects Excl. TLA-RS

0.6 0.4

0.0

Statement set Statement graph

1–2

3–5

6–10

11–20

21–50

Omitted symbols at the snapshot

50+

Fig. 5: Variation of proof similarity with the quest depth. Answer to RQ3: Agent proofs differ substantially from the references: across 200 levels, they reproduce only 11% of deleted lemma statements (re-stated recall), with just 8% symmetric statement overlap. Structural similarity also decreases sharply with quest depth, indicating growing divergence in both lemmas used and dependency structure. Agent proofs contain more assertions and duplicated code, and this trend generally increases with depth.

D. RQ4: How does agent behavior vary with the availability of proof context?

0.3

Block-clone ratio

Assert density (asserts / line)

Method. We take every RQ1 and RQ2 attempt of GPT-6 Sol and GPT-6 Luna with at least one lemma to rebuild (565 and 581 attempts), average the attempts of each level so that it counts once (314 and 320 levels), and count decisions, the tool calls other than polls of a running command. A trend is the slope of a measure on log2 of the lemmas to rebuild, with 0.8

0.2 0.1 0.0

Agent Ground truth

1–2

3–5

6–10

All projects Excl. TLA-RS

11–20 21–50

Omitted symbols at the snapshot

50+

Fig. 6: Assert density across depth (fraction of proof lines that are assertions).

All projects Excl. TLA-RS

0.6 0.4 0.2 0.0

Agent Ground truth

1–2

3–5

Why the agent stops

S

mid-plan, no stated reason task impossible as stated work too hard, out of ideas believes time or tokens run out broke workspace, believes done

5 44 3 17 4 25 7 6 0 9

L

New, most reused (≥½)

Fig. 4: Lemma reuse across projects.

0.2

L

100

Share of deleted-lemma-cone tasks (%) New, different stmts

S

Failed attempts 107 126 $5 budget 88 0 4-hour limit 0 25 agent reports it incomplete 19 99 agent claims success 0 2

6–10

11–20 21–50

Omitted symbols at the snapshot

50+

Fig. 7: Clone ratio across depth (fraction of tokens in recurring 20-token windows).

a fixed effect per project, given as a factor per doubling. We record each attempt’s cost, tokens, turns, thinking time, and failure outcome. For agent-terminated failures, we analyse the closing reasoning to classify why it stopped Deeper levels take more steps, not larger ones. The median attempt takes 20 decisions at 1–3 lemmas to rebuild and 157 at 64 or more for Sol, and 33 and 337 for Luna, a factor of 1.39 and 1.44 per doubling. Verification runs and edits grow similarly, with agents maintaining a consistent edit–verify loop of 0.5–0.9 edits per verification run across all depths. Most of the growth comes beyond 16 lemmas, where solve rates drop from 95% to 70% and 21% for Sol, and from 94% to 63% and 32% for Luna. The final diff is largely additive: net additions grow from 24 to 326 lines (Sol) and 31 to 724 (Luna), with at most 20 deletions. Agents mainly fill in proof bodies and add lemmas, rarely restructuring existing code. Agents often stop working midway. Neither agent fully follows the instruction to keep working until the environment ends the attempt. As Table V shows, Sol largely complies: 88 of its 107 failed attempts end when the $5 budget is exhausted, after a median of 18 minutes of reasoning. Thus, most of Sol’s failures indicate that the budget was insufficient, making it part of what determines ℓ∗ . Luna voluntarily ends 101 of its 126 failed attempts, at a median cost of $0.4; the remaining 25 run until the four-hour limit. The largest category of Luna’s voluntary stops (44/101) occurs mid-plan, immediately after re-running both checks, with no stated reason. Otherwise, both agents tend to judge the task impossible as stated, either because a lemma requires a stronger precondition (17 cases for Luna, 3 for Sol) or because the remaining work seems too difficult (25 and 4 cases, respectively). These judgments are often premature: the original project proves every withdrawn lemma, and another attempt by the same agent solves the same level in 6 of Luna’s 17 cases deemed impossible and all 3 of Sol’s. Budget in dollars buys Luna far more work. Sol is held back by the $5 budget and Luna by its own stopping. Luna still gets almost as far as Sol (RQ2) because its tokens cost about 18 times less ($0.014 against $0.26 per million input tokens, mostly cached). On levels with 16 or more lemmas to rebuild, a solved Luna attempt takes a median of 224 turns and 48 minutes of thinking for $0.49, against 78 turns and 11 minutes for $1.94 for Sol. Over all attempts, Luna processes 3.8 times as many input tokens as Sol at a fifth of the cost ($207 against $988). On the 44 levels where a Sol attempt ran out of budget, Luna works a median of 79 minutes for $0.73 and solves 16

of them, 6 of which no Sol attempt solves. Under a budget in dollars, the ranking of agents therefore depends on the price per token as much as on the model.

VII. R ELATED W ORK

Agents for Software Verification. AutoVerus [35] and VeruSAGE [18] employ multi-agent pipelines for proof genThe anti-cheat steers the agents back to proving. Tasks eration and repair, incorporating verifier feedback, planning, start with the anti-cheat failing on Admitted stubs. Thus, we and context management. AlphaVerus [36] translates programs only count cheats introduced by agents, across the 1,362 (Sol) from established verification languages (e.g., Dafny [37]) into and 2,298 (Luna) self-invoked anti-cheat runs and final grading. Verus, refining them through verifier feedback and reusing These shortcuts, accepted by the verifier alone, occur in 13% of verified programs as exemplars. RagVerus [38] uses retrievalSol’s attempts and 24% of Luna’s. Most involve stubs: the agent augmented generation to provide repository context through reinstates needed hidden lemmas using assume(false) or semantic and dependency-based retrieval, while SAFE [39] external_body rather than proving them. Another shortcut adopts a self-evolving approach based on synthetic proof is placing helper lemmas in a new verus! block, outside the generation, verifier feedback, and model fine-tuning. Related code the checker permits agents to modify. Cheats involving work in theorem proving explores the generation and reuse of frozen code are almost exclusively Luna’s: 17 attempts edit auxiliary lemmas. LEGO-Prover [40] builds a library of verified a spec function, 5 alter the contract of a trusted function, lemmas for reuse or synthesis during proof construction, while and 5 modify an executable function. Most spec edits only DeepSeek-Prover-V2 [41] and Hilbert [42] use hierarchical add triggers or casts, but some weaken the proof obligations. decomposition to break complex theorems into intermediate In Anvil, Luna removed the external_body of the trusted subgoals. While these approaches improve proof generation, lemma vrs_vsts_str_neq, proved the first of its two facts they do not systematically evaluate agent performance as proof and deleted the second; once flagged, it restored and proved dependencies become harder to resolve. S E V ERUS addresses both, solving the level. Flagging pivots agents to the actual this gap by using dependency graphs from real-world projects task: 67 of Sol’s 72 and 101 of Luna’s 138 flagged attempts to construct progressively harder quests, requiring agents to were solved, with all shortcuts replaced by a proof, and only generate and prove auxiliary lemmas before tackling the target 3 submissions that pass verification still fail the anti-cheat. theorem. This enables evaluation of both individual proof synthesis and the handling of interdependent proof obligations. Answer to RQ4: Deeper levels lead agents to take more small steps, not different ones. Sol mostly exhausts the $5 budget, while Luna often stops early for ungrounded reasons. Luna’s costs let it work much longer on the same budget, nearly matching Sol. The anti-cheat checker keeps the agents on the tasks: it flags a shortcut in 13% (Sol) and 24% (Luna) of attempts, mostly stubbed lemmas, and once flagged the agents replace most of them with proofs.

VI. T HREATS TO VALIDITY Internal validity. The $5 budget limits where success stops (RQ1). Since agents are nondeterministic, reruns may change individual results with one attempt per level (RQ1) or three per probe (RQ2), but are unlikely to alter pooled trends. Although agents may recall public proofs despite network restrictions, RQ3 shows they rarely reproduce the original lemmas. The initial task description also announced an unenforced 30-minute thinking limit, which some agents treated as binding (RQ4). We therefore reran every walk and search where Luna voluntarily ended a failed attempt, and those where such a stop could have affected Sol’s result, without this limit. Construct validity. Each quest uses one depth-first withdrawal order through the root’s dependency cone. Other orders, such as smaller subtrees first, could produce different difficulty profiles. Evaluating multiple orders would require repeating the evaluation for each, which is prohibitively expensive. External validity. All tasks come from six Verus projects verified with one Verus release, and we evaluate two agents (three in RQ1). Other projects, verifiers or agents may behave differently. The models are versioned products that change over time; we report the versions we used, and include every attempt’s trajectory in our artifact.

Benchmarks. Existing Verus benchmarks vary in scale and scope, from isolated proof synthesis to end-to-end verification. Verus-Bench [35] provides 150 algorithm-level tasks, while HumanEval-Verus [43] adapts HumanEval into 85 functionlevel tasks; both require generating proof annotations for existing implementations and specifications. VeriContest [44] comprises 946 competitive-programming problems and evaluates specification, code, and proof generation separately or end-to-end. Other work does this for Lean [45], [46]. VeriStruct [47] targets 129 functions across 11 Rust datastructure modules, requiring generation of abstraction functions, invariants, specifications, and proofs. VeruSAGE-Bench [18] offers 849 proof-generation tasks from eight open-source Verus projects, covering real-world systems software. In all of them, each task is a standalone unit with its proof context. Other work explores controlled context availability: VeriSoftBench [48] for Lean and Cobblestone [49] for Rocq investigate curated proof contexts. However, neither systematically evaluates agents as auxiliary lemmas become explicit proofgeneration objectives. CoqDev [50], which served as an initial inspiration for our work, increases task difficulty by masking theorems and lemmas introduced in the same commit as the target proof. However, its masking strategy follows the project’s commit history rather than proof dependencies, whereas S E V ERUS follows the dependency graph of the proofs. VIII. C ONCLUSION AND F UTURE W ORK We presented S E V ERUS, a technique that turns verified Rust projects into quests of verification tasks that share one target and withdraw its proof context step by step, from a single

missing lemma up to the whole proof. Severifying six opensource Verus projects resulted in 819 quests with 10,095 levels, and it scores an agent with a noisy binary search that needs a roughlt 450 attempts to evaluate 60 traces. attempts per project instead of one per level. The levels of a quest generally form a difficulty scale for the agents we tested. The strongest agent reaches the root of most sampled quests but solves only 35% of their levels, and agents that succeed without the original lemmas rarely rebuild them. S E V ERUS B ENCH -S TRIX is only the first version of the dataset. Once agents saturate it, we will release harder versions, each named after a stronger monster, as in Fig. 2. Besides adding more projects, we can make the tasks harder by removing the specification functions that the target’s statement does not use, and the requires and ensures clauses of every function except the target. The agent would then also have to write the definitions and intermediate contracts its proof needs. Finally, since S E V ERUS relies only on the dependency graph of the proofs, it could be adapted to other verifiers. ACKNOWLEDGMENTS This work was supported by national funds through Fundação para a Ciência e a Tecnologia, I.P. (FCT) under projects UID/50021/2025 (DOI: 10.54499/UID/50021/2025), UID/PRR/50021/2025 (DOI: UID/ PRR/50021/2025), and cofunded by the European Union through the Lisboa 2030 Programme (ERDF) and by national funds through FCT, I.P., under project no. 15018 (project SafeIaC, DOI: 10.54499/ 2023.18089.ICDT). We thank Amazon Science for the Amazon Research Awards (Fall 2024), which enabled the experiments through access to AWS Bedrock. R EFERENCES [1] T. Kwa, B. West, J. Becker, A. Deng, K. Garcia, M. Hasin, S. Jawhar, M. Kinniment, N. Rush, S. Von Arx et al., “Measuring ai ability to complete long software tasks,” Advances in Neural Information Processing Systems, vol. 38, pp. 92 213–92 266, 2026. [2] Y. Wang, M. Pradel, and Z. Liu, “Are “solved issues” in swe-bench really solved correctly? an empirical study,” in Proceedings of the 2026 IEEE/ACM 48th International Conference on Software Engineering, 2026, pp. 169–181. [3] B. Yu, Y. Zhu, P. He, and D. Kang, “Utboost: Rigorous evaluation of coding agents on swe-bench,” in Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), 2025, pp. 3762–3774. [4] G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish et al., “sel4: Formal verification of an os kernel,” in Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, 2009, pp. 207–220. [5] X. Chen, Z. Li, J. Zhang, V. Narayanan, and A. Burtsev, “Atmosphere: Practical verified kernels with rust and verus,” in Proceedings of the ACM SIGOPS 31st Symposium on Operating Systems Principles, 2025, pp. 752–767. [6] X. Leroy, S. Blazy, D. Kästner, B. Schommer, M. Pister, and C. Ferdinand, “Compcert-a formally verified optimizing compiler,” in ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, 2016. [7] G. Malecha, G. Morrisett, A. Shinnar, and R. Wisnesky, “Toward a verified relational database management system,” in Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 2010, pp. 237–248. We used generative AI tools from Anthropic and OpenAI to assist with coding, text rewriting, and the generation of Figure 2.

[8] M. Staples, R. Jeffery, J. Andronick, T. Murray, G. Klein, and R. Kolanski, “Productivity for proof engineering,” in Proceedings of the 8th ACM/IEEE International Symposium on Empirical Software Engineering and Measurement, 2014, pp. 1–4. [9] K. Fisher, J. Launchbury, and R. Richards, “The hacms program: using formal methods to eliminate exploitable bugs,” Philosophical transactions. Series A, Mathematical, physical, and engineering sciences, vol. 375, no. 2104, p. 20150401, 2017. [10] V. D’silva, D. Kroening, and G. Weissenbacher, “A survey of automated techniques for formal software verification,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 27, no. 7, pp. 1165–1178, 2008. [11] 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,” in Proceedings of the IEEE/ACM 47th International Conference on Software Engineering, ser. ICSE ’25. IEEE Press, 2025, p. 347–359. [Online]. Available: https://doi.org/10.1109/ICSE55347.2025.00161 [12] H. Tu, H. Zhao, Y. Song, M. Zafar, R. Meng, and A. Roychoudhury, “Agentic verification of software systems,” Proceedings of the ACM on Software Engineering, vol. 3, no. FSE, pp. 3558–3581, 2026. [13] JetBrains. (2025) The state of developer ecosystem 2025. JetBrains. [Online]. Available: https://devecosystem-2025.jetbrains.com/ [14] L. Gäher, M. Sammler, R. Jung, R. Krebbers, and D. Dreyer, “Refinedrust: A type system for high-assurance verification of rust programs,” Proceedings of the ACM on Programming Languages, vol. 8, no. PLDI, pp. 1115–1139, 2024. [15] N. D. Matsakis and F. S. Klock, “The rust language,” in Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology, 2014, pp. 103–104. [16] 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,” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA1, pp. 286–315, 2023. [17] C. Barrett and C. Tinelli, “Satisfiability modulo theories,” in Handbook of model checking. Springer, 2018, pp. 305–343. [18] C. Yang, N. Neamtu, C. Hawblitzel et al., “Verusage: A study of agentbased verification for rust systems,” 2025. [19] Microsoft, “Verus proof synthesis leaderboard,” https://microsoft.github. io/verus-proof-synthesis/, accessed: October 13, 2026. [20] R. M. Karp and R. Kleinberg, “Noisy binary search and its applications,” in Proceedings of the eighteenth annual ACM-SIAM symposium on Discrete algorithms, 2007, pp. 881–890. [21] Y. Cai, P. Singh, Z. Lin, J. Bosamiya, J. Gancher, M. Surbatovich, and B. Parno, “Vest: Verified, secure, high-performance parsing and serialization for rust,” in 34th USENIX Security Symposium, USENIX Security 2025, Seattle, WA, USA, August 13-15, 2025, L. Bauer and G. Pellegrino, Eds. USENIX Association, 2025, pp. 6917–6935. [Online]. Available: https://www.usenix.org/conference/usenixsecurity25/ presentation/cai-yi [22] C. Hawblitzel, J. Howell, M. Kapritsos, J. R. Lorch, B. Parno, M. L. Roberts, S. T. V. Setty, and B. Zill, “Ironfleet: proving practical distributed systems correct,” in Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, October 4-7, 2015, E. L. Miller and S. Hand, Eds. ACM, 2015, pp. 1–17. [Online]. Available: https://doi.org/10.1145/2815400.2815428 [23] A. Lattuada, T. Hance, J. Bosamiya, M. Brun, C. Cho, H. LeBlanc, P. Srinivasan, R. Achermann, T. Chajed, C. Hawblitzel, J. Howell, J. R. Lorch, O. Padon, and B. Parno, “Verus: A practical foundation for systems verification,” in Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, SOSP 2024, Austin, TX, USA, November 4-6, 2024, E. Witchel, C. J. Rossbach, A. C. Arpaci-Dusseau, and K. Keeton, Eds. ACM, 2024, pp. 438–454. [Online]. Available: https://doi.org/10.1145/3694715.3695952 [24] Z. Zhang, T. Zhou, C. Jenkins, O. Chowdhury, and S. Mu, “Automan: Facilitating verified distributed systems development through automatic code generation and manual optimizations,” in Proceedings of the ACM SIGOPS 31st Symposium on Operating Systems Principles, SOSP 2025, Lotte Hotel World, Seoul, Republic of Korea, October 13-16, 2025, Y. Won, Y. Kwon, D. Yuan, and R. Isaacs, Eds. ACM, 2025, pp. 768–785. [Online]. Available: https://doi.org/10.1145/3731569.3764822 [25] 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, A. Gavrilovska and D. B. Terry, Eds. USENIX Association, 2024, pp. 649–666. [Online]. Available: https://www.usenix.org/conference/osdi24/presentation/sun-xudong [26] Anonymous Author(s), “Artifact for SeVerus: Context-Aware, Gamified Benchmarking for Rust Verification,” Zenodo, 2026. [Online]. Available: https://doi.org/10.5281/zenodo.23894085 [27] OpenAI, “Codex CLI,” https://github.com/openai/codex, accessed: 202611-03. [28] Anthropic, “Claude Code Documentation,” https://docs.anthropic.com/ en/docs/claude-code, accessed: 2026-11-03. [29] H. B. Mann, “Nonparametric tests against trend,” Econometrica: Journal of the econometric society, pp. 245–259, 1945. [30] M. G. Kendall, “Rank correlation methods.” 1948. [31] Q. McNemar, “Note on the sampling error of the difference between correlated proportions or percentages,” Psychometrika, vol. 12, no. 2, pp. 153–157, 1947. [32] M. G. Kendall, “The treatment of ties in ranking problems,” Biometrika, vol. 33, no. 3, pp. 239–251, 1945. [33] A. P. Oron and N. Flournoy, “Centered isotonic regression: Point and interval estimation for dose–response studies,” Statistics in Biopharmaceutical Research, vol. 9, no. 3, pp. 258–267, 2017. [Online]. Available: https://doi.org/10.1080/19466315.2017.1286256 [34] B. Weisfeiler and A. Leman, “The reduction of a graph to canonical form and the algebra which appears therein,” nti, Series, vol. 2, no. 9, pp. 12–16, 1968. [35] C. Yang, X. Li, M. R. H. Misu et al., “Autoverus: Automated proof generation for rust code,” PACMPL, vol. 9, no. OOPSLA2, 2025. [36] P. Aggarwal, B. Parno, and S. Welleck, “Alphaverus: Bootstrapping formally verified code generation through self-improving translation and treefinement,” 2024. [Online]. Available: https://arxiv.org/abs/2412.06176 [37] K. R. M. Leino, “Dafny: An automatic program verifier for functional correctness,” in Logic for Programming, Artificial Intelligence, and Reasoning, E. M. Clarke and A. Voronkov, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2010, pp. 348–370. [38] 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, ser. LMPL ’25. New York, NY, USA: Association for Computing Machinery, 2025, p. 27–39. [Online]. Available: https://doi.org/10.1145/3759425.3763382 [39] 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 The Thirteenth International Conference on Learning Representations, 2025. [Online]. Available: https://openreview.net/forum?id=2NqssmiXLu [40] H. Wang, H. Xin, C. Zheng, Z. Liu, Q. Cao, Y. Huang, J. Xiong, H. Shi, E. Xie, J. Yin et al., “Lego-prover: Neural theorem proving with growing libraries,” in The Twelfth International Conference on Learning Representations, 2024. [41] Z. Ren, Z. Shao, J. Song, H. Xin, H. Wang, W. Zhao, L. Zhang, Z. Fu, Q. Zhu, D. Yang et al., “Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition,” arXiv preprint arXiv:2504.21801, 2025. [42] S. Varambally, T. Voice, Y. Sun, Z. Chen, R. Yu, and K. Ye, “Hilbert: Recursively building formal proofs with informal reasoning,” in The Fourteenth International Conference on Learning Representations, 2026. [Online]. Available: https://openreview.net/forum?id=GN8OdkTo3B [43] A. Bai, J. Bosamiya, E. Fernando, M. R. Hossain, J. Lorch, S. Lu, N. Neamtu, B. Parno, A. Shah, and E. Tang, “Humanevalverus: Hand-written examples of verified verus code derived from humaneval,” https://github.com/secure-foundations/human-eval-verus/ commit/ddb9ba36557774251e728f5341c731390364bd91, 2024, gitHub repository. [44] Z. Xie, M. Pawagi, Y. Liu, A. Rai, L. Shao, J. B. Jr., S. Che, and W. Wang, “Vericontest: A competitive-programming benchmark for verifiable code generation,” 2026. [Online]. Available: https://arxiv.org/abs/2605.08553 [45] Z. Ye, Z. Yan, J. He, T. Kasriel, K. Yang, and D. Song, “VERINA: Benchmarking verifiable code generation,” in The Fourteenth International Conference on Learning Representations, 2026. [Online]. Available: https://openreview.net/forum?id=0A4Uf88pog [46] A. Thakur, J. Lee, G. Tsoukalas, M. Sistla, M. Zhao, S. Zetzsche, G. Durrett, Y. Yue, and S. Chaudhuri, “CLEVER: A curated benchmark for formally verified code generation,” in 2nd AI

for Math Workshop @ ICML 2025, 2025. [Online]. Available: https://openreview.net/forum?id=pqNFDA2TFm [47] 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,” in Proceedings of the 32nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2026. [48] Y. Xin, J. Q. Chen, G. Durrett, and I. Dillig, “Verisoftbench: Repository-scale formal verification benchmarks for lean,” in Third Conference on Language Modeling, 2026. [Online]. Available: https://openreview.net/forum?id=lkEVcIJmMg [49] S. R. Kasibatla, A. Agrawal, Y. Brun, S. Lerner, T. Ringer, and E. First, “Cobblestone: A divide-and-conquer approach for automating formal verification,” in Proceedings of the 2026 IEEE/ACM 48th International Conference on Software Engineering, 2026, pp. 704–716. [50] M. Lu, Z. Zhou, D. Xie, S. Jia, B. Delaware, and T. Zhang, “Adaptive proof refinement with llm-guided strategy selection,” in Proceedings of the 41st IEEE/ACM International Conference on Automated Software Engineering, 2026, pp. 649–661.

Related documents

• A Complete, Formal Semantics for Rust Source Code#1202422
• Corten - Foundational Verification of Rust Programs#927666
• Secure input validation in Rust with parsing-expression grammars#264958
• RAIN: Agentic Proof Generation for Rocq-based Software Verification#1423550
• RepoReasoner: Evaluating Repository-Level Code Reasoning Ability of Long-Context Language Models#411120