PaperlayerView exact revision on arXiv

Source-linked AI summary

Scaling Lean Theorem Proving for Real-World Code Verification

Debargha Ganguly, Divya Raghunathan, Dejan Jovanović, Vikash Singh, Soonho Kong, Aaron Tomb, Aman Goel, Ferhat Erata, Sam Bayless

arXiv:2610.38174v1cs.CLcs.AIcs.LOcs.SE

TL;DR

Long-horizon Lean proving requires coherent search under finite context and compute, while established benchmarks are nearing saturation and verified-programming benchmarks remain small. EasyProver combines recursive, asynchronous proof search with independent Lean checking, and Aegis generates verification tasks over translated implementations. EasyProver nearly saturates established mathematics and code-verification benchmarks, yet proves only 1,054 of 1,997 attempted Aegis statements within the stated budget.

  • Problem

    Proof agents must coordinate local verifier feedback across long searches, while established benchmarks are nearing saturation and existing verified-programming benchmarks are small and costly to construct.

    Source: §1 · p. 1

  • Method

    EasyProver uses recursive agents and task-parallel search for fixed Lean statements, while Aegis generates specifications over translated Rust implementations and assigns kernel-checked proof or refutation labels.

    Source: §1 · p. 2, §3.1 · p. 3, §3.2 · p. 5

  • Results

    EasyProver nearly saturates established mathematics and code-verification benchmarks; with a 30-minute budget per statement, it proves 1,054 of 1,997 attempted Aegis statements (52.7%).

    Source: §4 · p. 8, §5 · p. 9

  • Takeaways & Limitations

    Aegis’s kernel-checked tasks can serve as benchmarks for other provers and as reinforcement-learning rewards.

    Source: §5 · p. 9

    The paper does not ablate harness components, compare the same model using Lean without the harness, or evaluate Aegis with other provers or for reinforcement learning.

    Source: §4 · p. 9

Abstract

from arXiv · show

We present EasyProver, a Lean proving system built from recursive agents with isolated contexts, asynchronous search, parallel tactic probing, and an elastic elaboration service. Using an off-the-shelf frontier model with no additional training, it proves 669/672 PutnamBench problems and all six IMO 2026 formalizations and resolves 597/600 NTP4VC verification conditions and all 189 VERINA tasks by proof or refutation. Because these benchmarks are close to saturation, we also introduce Aegis, which converts competitive programming problems into much harder verification tasks over real implementations. The pipeline writes safe Rust solutions, translates them into Lean with Aeneas, generates specifications, and labels each frozen statement with a kernel-checked proof or refutation. It produces 2,045 differentially validated Rust-Lean program pairs and 11,533 candidate specifications. Unlike hand-written benchmarks, these tasks carry implementation-level obligations from fixed-width arithmetic, explicit failure, generated loops, casts, and functionalized mutation. On a stratified sample of 2,000 statements, EasyProver proves 1,054 (52.7%) within a 30-minute budget per statement. The same tasks can also be used to benchmark other provers and as rewards for reinforcement learning.

1 Introduction

Building capable theorem-proving agents requires coherent long-horizon search under limited context and compute, while current benchmarks offer limited room for evaluation. The paper presents EasyProver and Aegis as a prover and a harder, automatically generated verification test set.

1 Introduction

  • Long proof searches must coordinate correct local steps with revisions when decompositions, lemmas, or abstractions fail, despite verifier feedback being local.Program verification adds recursive structure, representations, invariants, and implementation-level obligations to this challenge.Source: §1 · p. 1
  • Existing verified-programming benchmarks are small and costly to write because each task needs a formal specification, program model, and meaningful proof obligations.Automatic generation can address this bottleneck if specifications capture intended behavior and proofs span a range of difficulty.Source: §1 · pp. 1–2
  • Finite tests provide limited correctness evidence, whereas kernel-checked proofs certify claims against formal specifications and can serve as RLVR rewards.The motivation passage contrasts proof-based rewards with test-based rewards that may encourage exploiting a test harness.Source: §1 · p. 2
  • EasyProver combines recursive agents, isolated contexts, asynchronous search, parallel tactic probing, and elastic Lean elaboration to prove or refute fixed statements.Aegis generates verification tasks over translated implementations, with kernel-checked labels; the pipeline produces 2,045 validated Rust–Lean programs and 11,533 candidate specifications.Source: §1 · p. 2
  • 669/672 PutnamBench problems and all six IMO 2026 formalizations are proved, while 597/600 NTP4VC conditions and all 189 VERINA tasks are resolved by proof or refutation.The reported results use an off-the-shelf frontier model with no additional training, and each result is kernel-checked.Source: §1 · p. 2
  • 1,054 of 2,000 sampled Aegis statements are proved, leaving the generated tasks substantially less solved than the established benchmarks.The same tasks can benchmark other provers or provide reinforcement-learning rewards.Source: §1 · p. 2

2 Related Work

Prior work develops learned-policy proof search, code-verification systems, and task-generation approaches, while this paper distinguishes its untrained, model-directed search and separates task generation from solving. It also positions Aegis as a source of new translated-program tasks with proof and refutation labels.

Neural theorem proving and proof search

  • Unlike trained provers, EasyProver uses no fine-tuning or separately trained policy or value network; its parent agent chooses branches from returned proofs, counterexamples, or partial findings.This differs from UCT’s visit-based selection and averaged rollout values; it also contrasts with existing interfaces that bind an agent to a local Lean server.Source: §2 · p. 2

Data, benchmarks, and contamination

  • Aegis separates task generation from solving and labels each frozen statement with a kernel-checked proof of the statement or its negation.Refutations supply negative labels absent from proof-only or execution-graded loops, and fixed-task contamination mitigations do not generate new tasks.Source: §2 · pp. 2–3
  • Aegis’s source problems are public, but translated programs and specifications are new, and additional tasks can be generated with more compute.The reported 52.7% proof rate indicates these tasks remain far from saturation; mutation can create further negative-label tasks, though those are not evaluated here.Source: §2 · p. 3

Autoformalization and Rust-to-Lean verification

  • Aegis’s specification agent turns natural-language programming problems into Lean statements about Aeneas-extracted programs.Labels concern the extracted Lean program; differential testing separately provides evidence that it behaves like the Rust source.Source: §2 · p. 3
  • EasyProver freezes the theorem statement and requires compilation without sorry and with only allowlisted axioms, limiting ways a prover could game the checker.A separate specification agent writes each statement before the prover sees it, preventing the prover from choosing an easier statement.Source: §2 · p. 3

3 Methodology

EasyProver searches over fixed Lean statements using recursive agents and independent elaboration and acceptance checks; Aegis generates verification tasks over differentially validated Rust implementations translated into Lean. The method combines parallel search with explicit controls on task scope, validation, specification generation, and proof-or-refutation outcomes.

3.1 EASYPROVER: A Task-Parallel Proving Runtime

  • Each task fixes a Lean environment and proposition, and acceptance requires a kernel-checked proof or refutation of the frozen statement under a declared axiom policy.Lean Comparator independently checks the generated file; neither reported agent success nor a successful local tactic probe counts as acceptance.Source: §3.1 · p. 3
  • Recursive agents pursue alternative strategies or helper lemmas in fresh contexts and private project copies, while parents choose branches from children’s returned results.Completed results return without waiting for unfinished siblings, allowing early findings to redirect search without importing failed attempts into the parent’s context.Source: §3.1 · p. 4, Figure 1 · p. 4
  • Parallel tactic probing evaluates candidate tactics and automation concurrently, returning a successful tactic while discarding failed-probe diagnostics.The figure’s example contrasts a roughly 30-token returned tactic with roughly 30,000 tokens of probe traces.Source: §3.1 · pp. 4–5, Figure 2 · p. 4
  • INFINILEAN serves interactive elaboration through stateless, load-balanced replicas, while final proof acceptance is checked separately by Lean Comparator.Mathlib-preloaded REPL workers amortize imports; the cited setup reports imports taking tens of seconds and warm-worker elaboration about 0.2 seconds.Source: §3.1 · p. 5, Figure 3 · p. 5
  • The harness promotes candidate proofs under a lock, rechecks the solution file against build and acceptance criteria, and ends search at the first accepted candidate.Search uses an off-the-shelf model without fine-tuning or separately trained policy or value networks.Source: §3.1 · pp. 3, 5

3.2 AEGIS: The Data Environment

  • Aegis writes safe Rust solutions, translates them through Charon and Aeneas, and generates Lean verification tasks over the resulting implementations.The pipeline is limited to pure functions over first-order data and excludes unsupported stateful or class-based interfaces, including hash tables, closures, nested references, and unrestricted aliasing.Source: §3.2 · pp. 5–6
  • Differential validation retains programs only when Rust tests pass and Rust outputs match Lean evaluations on the same inputs; 2,045 of 2,356 attempted problems pass every stage (86.8%).Representations include ASCII byte arrays for strings and owned recursive enums for trees and linked lists; integer values, sequence lengths, and test-set sizes are bounded for tractable Lean evaluation.Source: §3.2 · p. 6
  • Translated-program obligations include machine-word range bounds, explicit failure branches, generated loop control flow, and functionalized mutation that requires reasoning about updates and invariants.Specifications cover intended-to-hold properties and intended-to-fail claims, are filtered for duplicates, triviality, vacuity, or elaboration errors, then frozen for proof search; only checked proof or refutation outcomes resolve tasks and provide RLVR rewards.Source: §3.2 · pp. 6–7

4 Results

EasyProver resolves nearly all tasks on several established mathematics and code-verification benchmarks, while AEGIS supplies harder implementation-level statements on which many remain unresolved. The reported results use kernel-checked proofs or refutations.

Formal mathematics

  • 669/672 PutnamBench problems (99.6%) were solved, 72 more than Chung et al.’s strongest reported configuration (597/672); EasyProver also solved all six IMO 2026 problems and all twelve Putnam 2025 problems.These results use an off-the-shelf model with no fine-tuning or separately trained policy or value network.Source: §4 · p. 7, Table 1 · p. 8
  • EasyProver was not evaluated on IMO 2025 or USAMO 2026, and the model’s undisclosed training cutoff means informal-solution contamination cannot be ruled out.The authors report that contamination would affect interpretation, not the correctness of kernel-checked proofs.Source: §4 · p. 7

Code verification

  • 597/600 NTP4VC tasks (99.5%) were resolved, alongside all 189 VERINA tasks, all 77 AlgoVeri tasks, and 113/143 CLEVER tasks translating to Lean 4.32 (79.0%).NTP4VC included 588 proofs and nine refutations.Source: §4 · pp. 7–8, Table 2 · p. 8

AEGIS

  • 1,054 of 2,000 sampled AEGIS statements (52.7%) were proved within 30 minutes per statement, leaving 943 unresolved.The sample covered 1,257 translated programs and excluded statements already refuted by Plausible and the category requested to fail.Source: §4 · pp. 7–8

Limitations

  • The authors did not ablate individual harness components or compare the same model using Lean without the harness.Each configuration would require a full benchmark run.Source: §4 · p. 9

5 Conclusion

The conclusion presents EasyProver’s near-saturation of established benchmarks and AEGIS’s harder verification tasks over mechanically translated safe Rust. The appendix case studies describe the translation’s proof obligations and recurring notation for proofs of totality.

5 Conclusion

  • EasyProver resolves nearly all tasks in several established mathematics and verification benchmarks without additional model training, while AEGIS statements remain challenging and carry kernel-checked labels usable for benchmarking or reinforcement-learning rewards.The conclusion reports a 52.7% proof rate on a sampled set of AEGIS statements.Source: §5 · p. 9

A Case Studies and Measurement Conventions

  • Seven safe Rust programs illustrate how Aeneas translations make checked arithmetic, bounds-checked indexing, failure, termination, loop-carried state, and mutation explicit proof obligations.The appendix presents each problem, frozen theorem, generated Lean definitions, and accepted proof, or the unresolved theorem for the last program.Source: A Case Studies and Measurement… · p. 14
  • For fixed-width scalars, .val exposes the mathematical integer or natural-number value; the weakest-precondition judgment requires termination with an ok result satisfying the postcondition.Even a True postcondition establishes totality because failure and divergence do not satisfy the judgment.Source: A Case Studies and Measurement… · p. 14
  • Generated loops use a loop-body/driver pair: the body returns either a continuation state or final result, and a separate driver invokes it through Aeneas’s loop combinator.Mutation is functionalized: index_mut returns the current element and a backward function that builds the updated vector.Source: A Case Studies and Measurement… · p. 14

A.1 Measuring proof size

The proof-size appendix counts complete accepted developments, including their supporting definitions and lemmas, and distinguishes those lines from the original Rust and translated Lean program counts. It also describes a source-level sorting example.

A.1 Measuring proof size

  • 145,646 physical lines make up the 1,054 accepted proof artifacts; the median artifact has 104 lines and the largest has 1,167.Counts include comments, models, helper lemmas, loop invariants, generated-code relations, and the target proof.Source: §A.1 · p. 14, Table 3 · p. 14
  • Table 3 orders selected programs by accepted proof size and reports physical line counts for the programs, translations, and proof artifacts.The merge-sort theorem is unresolved; “Added” counts lines introduced when replacing the original one-line sorry, while “Rust” and “Aeneas” count solution.rs and Funs.lean lines.Source: Table 3 · p. 14, §A.1 · p. 14

B.1 Problem and source-level approach

  • The sorting example splits signed integers by index parity, selection-sorts each sequence, then interleaves them to restore their original parities.The implementation scans once to split the input and uses quadratic selection sort on each vector.Source: §B.1 · p. 15

B.2 What the proof must establish

The theorem establishes that the translated call succeeds and returns a vector with the input’s length, not that it sorts the output. Its proof composes length and index-validity invariants across the split, sorting, and emission loops.

B.2 What the proof must establish

  • The frozen theorem proves successful return and exact output length, without requiring a precondition or asserting that the output is sorted.The proof still verifies both sorting phases because all preceding monadic computations must succeed.Source: §B.2 · p. 15
  • After processing i positions, the parity-split vectors have lengths (i + 1)/2 and i/2, supporting valid reads during final interleaving.Each reconstructed vector must preserve its length so later indices remain valid.Source: §B.2 · p. 15

B.3 Complete Rust implementation

  • The Rust implementation separates values at even and odd indices, sorts the two vectors, then interleaves them into the result.The generated Lean representation expresses loops as body/driver pairs and models indexed mutation through successive calls.Source: §B.2 · p. 15

B.2 What the proof must establish

  • The proof proceeds bottom-up from split-loop length invariants through length-preserving sorts to a four-component emission invariant, then composes loop specifications.The final composition establishes totality and exact output length for the top-level function.Source: §B.2 · p. 15

B.5 Accepted proof artifact

The accepted proof establishes successful execution and exact output length by composing loop-level length and parity-count invariants. The same section also sketches a source-level approach for the subset-XOR sum problem.

B.5 Accepted proof artifact

  • The proof tracks parity counts through splitting and emission while showing both in-place sorting loops preserve vector length.For i processed positions, the temporary vectors have lengths (i + 1)/2 and i/2; the emission loop pushes once for each index k < n.Source: §B.5 · pp. 20, 22
  • The theorem proves that every successful call returns a vector whose length equals the input length, with no precondition.This structural bound follows from the final loop’s one push per input index, starting from an empty result.Source: §B.5 · p. 23
  • The proof is assembled from specifications for the splitting, sorting, and emission loops, then applied to the top-level output-bound theorem.The loop specifications establish length preservation and the parity-based counts needed for valid emission reads.Source: §B.5 · p. 24

C.1 Problem and source-level approach

  • For the subset-XOR sum problem, each input bit appears in the XOR of 2^n−1 subsets when the input is nonempty; the Rust approach computes an OR and multiplies by that factor.The implementation computes the input OR, obtains the factor by repeated doubling, and multiplies the two values.Source: §C.1 · p. 25

C.2 The theorem and fixed-width arithmetic

The subset-XOR theorem proves that the translated call succeeds and returns the exact sum of subset XORs. Its proof combines a natural-number identity with bounds ensuring the fixed-width computation completes.

C.2 The theorem and fixed-width arithmetic

  • The theorem proves exact functional correctness: the call succeeds and returns the sum of the XOR folds of all input sublists.The proof must relate machine bitwise operations to their mathematical counterparts and show repeated doubling and multiplication fit signed 64-bit integers.Source: §C.2 · p. 25
  • All three preconditions—nonemptiness, at most twelve elements, and values in [1, 20]—bound the OR, doubling factor, and product enough to avoid overflow and failure.The bounds include an OR below 32, a factor no greater than 2^11, and a product bounded by 31 · 2^11.Source: §C.2 · p. 25

C.4 Complete AENEAS-generated Lean implementation

  • The proof first establishes the subset-XOR identity over natural numbers, then matches fixed-width XOR and OR to natural-number operations on small nonnegative inputs.The translated implementation accumulates the OR, handles the empty-input case, and otherwise computes the doubling factor before multiplication.Source: §C.2 · p. 25, §C.4 · p. 26

C.5 Accepted proof artifact

This section presents accepted Lean specifications and proofs for subset-XOR summation and matrix reshaping, covering bounded 64-bit operations, shape and indexing conditions, and machine safety. It also shows the Aeneas-generated loop structure and dimension-product checks underlying the reshape proof.

C.5 Accepted proof artifact

  • For 1 ≤ n ≤ 12, the doubling loop returns 2^(n − 1), with intermediates bounded by 2^11 = 2048 and therefore within I64.The proof uses a decreasing-loop invariant relating the counter to the factor’s power of two.Source: §C.5 · p. 27
  • The pure-N scaffolding proves that subset-XOR totals equal the list’s fold-OR multiplied by 2^(length − 1), using bounded-bit identities and induction.The key bit identity is verified over all 32^3 cases; auxiliary lemmas handle OR folds and the recursive decomposition of sublists.Source: §C.5 · pp. 27–28
  • For small nonnegative values below 32, the artifact bridges I64 XOR and OR operations, their folds, and the subset-XOR sum to corresponding natural-number computations.The sum bridge assumes every list element lies in [1, 20].Source: §C.5 · pp. 28–29
  • With list length at most 12 and elements in [1, 20], the first subset-XOR loop is proved to return the fold-OR of the inputs as a nonnegative value below 32.Its invariant tracks the OR of the processed prefix and preserves the accumulator’s range at each step.Source: §C.5 · pp. 30–31
  • The subset_xor_sum specification equates the return value with the XOR-total sum over every positional subset, for nonempty lists of at most 12 values in [1, 20].These constraints keep checked operations within range, so the call returns ok.Source: §C.5 · p. 31

D.1 Problem and source-level approach

  • For legal dimensions, matrix_reshape flattens the input in row-major order and regroups consecutive elements into the requested shape; otherwise it returns a copy with the original shape.The source-level mapping sends output coordinate (a, b) to flat index ac + b, then to source coordinate (⌊k/n⌋, k mod n).Source: §D.1 · p. 33

D.3 Complete Rust implementation

  • The Rust implementation’s fallback is reachable through three guards, and its flattening, regrouping, and fallback code yields ten loop-body/driver pairs.The legal-shape theorem hypotheses rule out the fallback paths.Source: §D.2 · p. 33, §D.3 · p. 33

D.2 Representation and bounds

  • The accepted matrix_reshape_spec proves successful execution, an r × c output, and row-major cell preservation under rectangularity and the stated bounds.Euclidean division establishes valid source indices, while bounds make the machine products and casts safe; the cell-value bound is not used by the proof.Source: §D.2 · p. 33

D.4 Complete AENEAS-generated Lean implementation

  • AENEAS represents the Rust loops as Lean loop-body and driver definitions, with Result-based indexing, pushes, and cursor increments.The generated code includes loop bodies for traversing rows and cells and constructing the flattened and regrouped outputs.Source: §D.4 · pp. 34–35
  • Nested loops build the output by reading elements from the flattened vector, pushing them into rows, and pushing completed rows into the result.The shown loop bodies advance element and row indices as they accumulate the row and output vectors.Source: §D.4 · pp. 37–38
  • The `matrix_reshape` function computes dimensions and compares the requested row-by-column product with the input element count before calling reshape loops.It obtains the first row’s length when the matrix is nonempty, computes the input total, and compares it with `r * c`.Source: §D.4 · p. 38

D.5 Accepted proof artifact

The accepted MatrixReshape artifact proves a legal reshape returns a matrix of the requested shape with entries preserved in row-major order; the adjacent triangular-sum example proves reversal invariance through its reduction model.

D.5 Accepted proof artifact

  • The reshape proof specifies flattening as row-major and regrouping as consecutive chunks, then connects those loop results to the output specification.The flatten loop returns the row-major sequence with length m * n; the regroup loop builds rn rows of cn elements.Source: §D.5 · pp. 40–41
  • Under the stated bounds and legal-shape precondition, MatrixReshape returns an r × c matrix whose entries preserve the input’s row-traversing order.The input matrix is nonempty, rows are uniform-width, and r * c = m * n.Source: §D.5 · p. 42

E.1 Problem and source-level approach

  • The source repeatedly replaces adjacent digits with their sum modulo 10 until one digit remains, and binomial-coefficient symmetry explains the reversal invariance.The implementation copies the slice into a vector and repeatedly constructs a vector one element shorter.Source: §E.1 · p. 44
  • The triangular-sum theorem proves that reversing the input leaves the returned value unchanged.The proof applies executable correctness to the original and reversed inputs, then identifies their list models.Source: §E.1 · p. 44

E.2 Proof architecture

The triangular-sum proof connects executable loop behavior to a list model before establishing reversal invariance. Its architecture specifies each loop and discharges arithmetic-safety and termination obligations.

E.2 Proof architecture

  • The proof first connects the translated program to a list model through specifications for copying, one reduction, repeated reductions, and the final indexed read.Digit bounds ensure checked additions succeed, while length invariants bound reads and show each pass shortens the vector.Source: §E.2 · p. 44
  • The final theorem proves reversal invariance by applying executable correctness to both slices and identifying their list models.Its declaration and proof occupy the final 25 lines of a 431-line artifact.Source: §E.2 · p. 44

E.3 Complete Rust implementation

  • The Rust implementation copies the input and repeatedly builds shorter vectors from adjacent sums modulo 10 until one value remains.The generated Lean implementation exposes corresponding loops and operations using Result-valued computations.Source: §E.3 · p. 44, §E.4 · p. 45

E.4 Complete AENEAS-generated Lean implementation

  • AENEAS-generated Lean represents the copy and reduction loops explicitly, including indexed reads, checked addition, remainder, and vector pushes.The generated definitions use Result and ControlFlow for loop execution.Source: §E.4 · pp. 45–46

E.5 Accepted proof artifact

This section presents Lean proof artifacts for triangular sums, including a specification of the Rust implementation, its correctness on nonempty inputs with digits from 0 to 9, and reversal invariance. It also describes a shift-invariance theorem for a grid statistic.

E.5 Accepted proof artifact

  • The Lean model repeatedly replaces adjacent pairs with their sum modulo 10, shrinking the list by one per pass until one value remains.The empty-list result uses 0 as a dummy, while the specification’s non-emptiness precondition prevents that case.Source: §E.5 · pp. 46–47
  • The model is invariant under list reversal because each symmetric pairwise reduction commutes with reversal and the repeated process ends in a singleton.The artifact formalizes reversal for one reduction pass, for iteration, and for the final model.Source: §E.5 · pp. 47–48
  • Under nonempty-input and 0–9 digit constraints, the Rust triangular-sum function returns exactly the Lean model’s result.The specification relates the result to the model applied to the input values; the outer loop is proved to implement the repeated reduction.Source: §E.5 · p. 50
  • Under nonempty 0–9 digit constraints, reversing the input preserves the result of the real extracted triangular-sum function.The theorem assumes the original call succeeds; the result follows because the binomial-coefficient weights of the triangular sum are symmetric.Source: §E.5 · p. 51

F.1 Problem and source-level approach

  • For equal-shaped grids, adding a fixed signed integer to every cell leaves the output matrix of `difference_of_distinct_values` unchanged.The function compares distinct-value counts strictly above-left and below-right of each cell; translation preserves equality patterns, so those counts do not change.Source: §F.1 · p. 52

F.2 Relational proof structure

The relational proof carries equality through the translated program’s nested loops, while transporting length and cursor bounds between levels. Its theorem assumes both grids have rows of length n.

F.2 Relational proof structure

  • The relational argument follows six loop components: matching scan decisions and counts, pointwise shifted vectors, equal per-cell counts and differences, and identical output rows.Source: §F.2 · p. 52
  • Each proof level transports length and cursor bounds; the theorem assumes every row in both grids has length n, while two additional frozen hypotheses are unused.Those unused hypotheses bound first-grid cells to [1, 50] and mathematical sums to the signed 64-bit range; the program receives the second grid rather than computing its shift.Source: §F.2 · p. 52
  • The target theorem and proof occupy the final 38 lines, after 1,129 lines of definitions and loop lemmas supporting six loop components.Source: §F.2 · p. 52

F.3 Complete Rust implementation

  • The Rust implementation scans each prefix to count distinct values, collects above-left and below-right diagonals, then appends each absolute count difference to its output row.Source: §F.3 · pp. 52–53

F.4 Complete AENEAS-generated Lean implementation

  • AENEAS-generated Lean represents nested loops with separate loop-body and driver definitions, passing loop state explicitly through tuples.Source: §F.4 · p. 54

F.5 Accepted proof artifact

The accepted proof artifacts use Lean to verify implementation-level properties of Aegis programs, including loop and indexing relations and the invariance of grid outputs under uniform shifts. They also include an AENEAS-generated `relative_sort_array` implementation and a theorem establishing safe execution and termination under input-length bounds.

F.5 Accepted proof artifact

  • A generic relational simulation theorem shows that if related loop bodies preserve state relations and decrease a natural-number measure on continuations, successful termination of the first loop implies related successful termination of the second.The proof proceeds by strong induction on the measure.Source: §F.5 · p. 56
  • Successful slice and vector indexing is characterized by an in-bounds index and equality between the result and the indexed element.The artifact states this characterization separately for `Slice.index_usize` and `alloc.vec.Vec.index_usize`.Source: §F.5 · p. 57
  • A common offset applied to every slice element preserves `count_distinct`’s result exactly.The proof establishes preservation first for the inner equality-testing loop and outer counting loop, then for `count_distinct` itself.Source: §F.5 · pp. 57, 59, 60
  • Vector push succeeds when lengths match and appends the supplied element, while indexing a one-element list append returns either the prior list element or the appended element.These helper lemmas support reasoning about the implementation’s collection loop.Source: §F.5 · p. 60
  • The left-diagonal collection loop maps accumulators related by a common offset to outputs with equal lengths and the same elementwise offset relation.The theorem assumes equal row counts, rectangular grids with equal row lengths, and a common offset between corresponding grid elements.Source: §F.5 · p. 61
  • The right-diagonal collection loop maps shift-related accumulators to shift-related outputs.The artifact invokes the right-diagonal shift theorem when transferring the collections between grids.Source: §F.5 · pp. 63, 67
  • The per-cell loop returns the same row on uniformly shifted grids because the shifted diagonal slices retain their distinct counts.The proof uses the count equality to show that the pushed absolute differences coincide.Source: §F.5 · pp. 66–67
  • The row loop returns the same answer matrix on uniformly shifted grids.The proof applies the per-cell row result while processing each row.Source: §F.5 · pp. 68–69
  • Uniformly shifting every entry preserves the diagonal-distinct-difference output, provided both grids meet the stated shape and range conditions and the original run succeeds.The result follows because the function depends on entry equality patterns, which a common offset preserves; shifted values must remain within signed-64-bit range.Source: §F.5 · p. 70

G.1 Problem and source-level approach

  • The relative_sort_array_totality theorem proves an ok result under two input-length bounds, but its True postcondition does not specify the returned vector.It requires no element-value bounds, nonemptiness, distinctness, or membership conditions because these are unnecessary for safe execution.Source: §G.1 · p. 72

G.2 The totality obligations

  • Seven generated loop-body/driver pairs are proved safe using invariants and decreasing measures for bounds, vector growth, cursor updates, and subtraction.Element values need no magnitude bounds: input-length bounds control Std.Usize increments and vector growth.Source: §G.2 · p. 72

G.4 Complete AENEAS-generated Lean implementation

  • Generated loop bodies use vector indexing and mutation, and append elements with `push`.The excerpts show indexed access and `index_mut` in loop bodies, plus a loop body that pushes an element into the result vector.Source: §G.4 · p. 76
  • The `relative_sort_array` definition sequences generated loops to build and process vectors, returning a `Result`.The shown function initializes a Boolean vector, runs loops 0–4, and returns a vector of `Std.I64`.Source: §G.4 · pp. 76–77

G.5 Accepted proof artifact

The accepted artifact proves successful completion of the extracted relative-sort program by establishing loop invariants and termination under input-length bounds. Its totality claim guarantees an `ok` result, not a particular output vector.

G.5 Accepted proof artifact

  • Loop-specific invariants establish bounded growth and preserved lengths for vectors such as `used`, `result`, and `rest`.For example, the outer matching loop bounds `result` by 1000 times its target index, while the collection loop bounds `rest` by its scan index.Source: §G.5 · pp. 77–78
  • The insertion-sort inner walk proves that its index decreases toward zero while accesses remain in bounds and the vector length is preserved.The outer insertion-sort loop also preserves the vector length across iterations.Source: §G.5 · pp. 78–79
  • The proof decomposes the function into counted loops that build `used`, match targets, collect unused values, insertion-sort them, and append the result.The generated function runs six counted loops over fixed lengths; the matching loop accumulates at most n entries in `result`.Source: §G.5 · pp. 79–80
  • The totality argument rules out faults and divergence under the stated length bounds; the function performs no arithmetic on element values.Index accesses are guarded by loop bounds, and termination follows from cursors moving toward fixed bounds or zero.Source: §G.5 · p. 80
  • Both input slices are bounded by 1000, ensuring cursor increments and decrements cannot overflow and supporting the successful-completion claim.The theorem asserts only that the function returns an `ok` result, not which vector it returns.Source: §G.5 · p. 80

H.1 Problem and implementation

This section presents an AENEAS-generated Lean implementation of bottom-up merge sort and a frozen theorem asserting successful return for non-empty inputs of at most 50,000 elements, without specifying the returned values. The theorem remains unproved within the 30-minute budget, with generated code exposing cursor, arithmetic, vector-update, and termination obligations.

H.3 Complete Rust implementation

  • The Rust source implements bottom-up merge sort by copying input into an owned vector, merging adjacent runs into an equally sized scratch vector, and copying each pass back.Run widths double from 1, and array elements are copied and compared rather than used in signed arithmetic.Source: §H.1 · p. 81

H.1 Problem and implementation

  • The theorem sort_array_returns_ok requires only successful return for 1 ≤ |nums| ≤ 50,000, but the agent did not resolve it within 30 minutes.It does not require the output to be ordered or to be a permutation of the input.Source: §H.1 · p. 81

H.4 Complete AENEAS-generated Lean implementation

  • AENEAS expands the 66-line Rust implementation into 328 Lean lines with eight loop-body/driver pairs and five index_mut calls.The generated code exposes mutually dependent obligations for the run and merge cursors.Source: §H.2 · p. 81

H.2 Obligations in the unresolved theorem

  • The generated proof obligations include cursor bounds, representable checked arithmetic, vector-length preservation, loop termination, and compatible cursor relations between merge loops.Intermediate checked additions must be representable before later minimum operations, and each index_mut backward closure must rebuild a vector of the expected length; full sorting correctness would additionally require orderedness and permutation.Source: §H.2 · p. 81

H.4 Complete AENEAS-generated Lean implementation

  • The Lean implementation copies the input into a vector, returns immediately when its length is at most one, and otherwise runs a width-doubling merge-sort driver using a scratch buffer.Its outer loop merges adjacent runs and copies the buffer back into the working vector.Source: §H.4 · p. 86

H.5 Unresolved theorem artifact

  • The totality argument rules out faults through guarded accesses, bounded Usize computations, and the absence of signed arithmetic, and rules out divergence through finite loop bounds and increasing indices.It relies on the stated input-length precondition of 1 to 50,000.Source: §H.5 · pp. 86–87
  • The unresolved theorem asserts successful completion for slices with lengths from 1 through 50,000, but makes no claim about which integer list is returned.The frozen theorem retains a sorry proof body and specifies only that the result satisfies True.Source: §H.5 · pp. 86–87

I Recurring Proof Obligations

Translated-program proofs require obligations beyond the algorithms’ mathematical descriptions, including bounds, mutation, and safety invariants. Even a totality-only target can require coupled cursor and overflow invariants, and accepted proofs are substantially longer than their Rust sources.

I Recurring Proof Obligations

  • Weak postconditions can still require proving every preceding sort, lookup, update, and increment succeeds.The even/odd sorting theorem constrains only output length, but its weakest-precondition judgment covers those earlier operations.Source: I Recurring Proof Obligations · p. 88
  • Input bounds justify casts, arithmetic, pushes, and indexed accesses, while some cell-value bounds are unused when values are not arithmetically processed.The subset-XOR and reshape proofs use bounds for machine-word doubling, signed products, and signed-to-unsigned casts.Source: I Recurring Proof Obligations · p. 88
  • In-place Rust assignments translate into forward reads and backward vector-rebuilding functions, so proofs repeatedly establish length preservation and lookup behavior.A source-level swap becomes several monadic update steps.Source: I Recurring Proof Obligations · p. 88
  • Relational theorems connect separate executions through a common model or synchronized loop boundaries while carrying representation and safety invariants.This applies to reversal and uniform-shift invariance despite their short mathematical arguments.Source: I Recurring Proof Obligations · p. 88
  • The unresolved merge-sort theorem asks only for termination and no generated failure, yet the translated fixed-width program requires coupled cursor and overflow invariants.The corresponding mathematical sorting function has trivial totality, unlike the translated program.Source: I Recurring Proof Obligations · p. 88
  • Across six resolved cases, Rust sources span 19–67 lines while accepted proofs span 289–1,167 lines.Most proof length connects the mathematical claim to the concrete representation and safe execution of generated control flow.Source: I Recurring Proof Obligations · p. 88

Related papers

Loading 2610.38174v1…