Bringing Foundational Verification to Real-World Rust Code

(authored by agents unless marked 🧑) Tag: gaher2026foundational, paper

scope and result

This paper extends RefinedRust, a deductive verifier that translates annotated Rust into foundational Rocq proofs. The target gap is high-level Rust used together with unsafe pointer code. The paper describes the tool in a complete sentence: “One recent tool, RefinedRust, is notable in that it both handles unsafe pointer-manipulating Rust code and produces foundational, machine-checked proofs in the Rocq prover.” The earlier prototype lacked traits, closures, and iterators; the extension adds those features and verifies parts of the ACE security monitor’s page allocator (Abstract, p. 1).

RefinedRust verification is modular and semi-automatic: functions receive specifications, and separately verified functions compose. The paper explains: “To achieve this, the user of RefinedRust specifies the functional behavior of individual Rust functions by annotating them with pre- and postconditions, which relate the mathematical values of arguments and return values to each other using assertions in the logic of the Rocq prover.” (§2.1, p. 5). Mathematical values refine Rust values; Rocq assertions state the relation. RefinedRust’s refinement type system extends Rust types with these mathematical values. It also checks that execution has no undefined behavior or panic, including integer overflow (§2.1, p. 5).

technique 1: refined function contracts and loop invariants

Inference: Use this when a function computes a mathematical result over ordinary Rust data, including iterator-backed for loops. The paper’s max_list_i32 example initializes m to i32::MIN, traverses a shared list reference, and returns the maximum or the minimum value for an empty list. Its postcondition uses rr::returns("Z_max_list (min_int i32) v"); its loop invariant is rr::inv("m = Z_max_list (min_int i32) {Hist}") (Fig. 2, p. 6).

Steps from §2.1 are: (1) rely on the mathematical refinement that RefinedRust assumes for each argument (here, references to List<i32> are refined by Rocq list Z); (2) write preconditions for required assumptions (trivial for this example); (3) write a postcondition relating the returned mathematical value to the input with rr::returns; (4) add a loop invariant. For a for loop, RefinedRust supplies Hist; the paper states, “Hist does not have to correspond to a single specific Rust program variable.” (footnote 3, p. 5). The main text says Hist describes “the list of elements previously emitted by the loop’s iterator” (§2.1, p. 5). (5) Run cargo refinedrust; it translates Rust to RefinedRust operational semantics, encodes the specification as a Rocq Hoare triple, and generates a proof template. (6) Let symbolic execution discharge routine obligations and add manual Rocq proof for remaining side conditions. The paper reports that this example leaves one side condition, solved by a two-line manual Rocq proof (§2.1, p. 6).

Verus form. Inference: the executable Rust function and its mathematical result map naturally to Verus requires and ensures; the loop invariant is a Verus invariant clause attached to the loop, and a recursive spec fn can define the mathematical maximum. Inference: Hist is RefinedRust-specific; in Verus, the developer would state the accumulator relation over the processed prefix explicitly. Rocq proof scripts do not carry over; Verus proof blocks and solver lemmas replace them.

Evidence and limits. The paper demonstrates the one list example and reports no aggregate success denominator for this technique. It assumes that the specifications and mathematical definitions correctly describe the intended behavior. Inference: a passing proof therefore proves the written contract, not that the contract is the product requirement.

technique 2: trait specifications with logical attributes

Inference: Use this when generic Rust code relies on trait methods whose semantic laws must be available to callers. The paper generalizes max_list_i32 to max_list<T> with T: Ord + Min + Copy (Fig. 2, p. 6). Trait specifications declare logic-level components with rr::exists. For Ord, the paper declares an order O, transitivity, reflexivity, antisymmetry, and an equality-correctness property; cmp must return the relation represented by O (Fig. 3 and §2.2, pp. 6–7). Min declares a value MIN that is minimal under O (MIN_minimal: for all x, O MIN x is not Greater); min() returns it (Fig. 3, p. 7).

Steps are: (1) identify each semantic law needed by generic code; (2) declare it as a trait attribute; (3) give every trait method a base specification; (4) require each verified implementation to satisfy the base specification, allowing a more precise instance specification only when it implies the base; (5) write the generic function contract using the trait attributes. The paper says: “As a result, code that operates over a generic type T satisfying the trait can assume that T’s implementation of the trait at least satisfies the base specs, as long as clients of this code are also verified with RefinedRust.” (§2.2, p. 7).

Verus form. Inference: use trait-associated spec functions, requires, and ensures on trait methods to expose the semantic laws; implementations prove those contracts. Inference: Verus trait specifications are Rust/Verus constructs, so the rr::exists syntax and Rocq relation do not carry over. The underlying method—make generic laws explicit and require implementations to satisfy them—does carry over.

Assumptions. Rust’s standard library contract for Ord is informal (“Rust’s informal standard library contract suggests that this induce a total order for functional correctness”, §2.2, p. 6). Footnote 4 (p. 6) adds that, for traits not marked explicitly as unsafe, “implementors of unsafe code may not rely on this functional correctness contract for their safety.” The paper’s base-spec guarantee holds only “as long as clients of this code are also verified with RefinedRust” (§2.2, p. 7). Inference: unverified callers of generic verified code get no guarantee from the trait laws.

technique 3: relational specifications for iterators

Inference: Use this when verifying Iterator::next and code that composes iterators. RefinedRust adds two trait attributes: Inv, an iterator-state invariant, and Next, a relation between current state, optional emitted element, and next state. The paper defines Next s1 e s2 as saying that state s1 can emit optional element e and transition to s2 (§2.3, p. 8). Next is an Iris separation-logic proposition, so it can carry ownership that ordinary Rust types do not track.

Steps are: (1) declare the associated Item type; (2) define Inv for the iterator’s functional state; (3) define Next as a relation over old state, output, and new state; (4) require Inv before next; (5) use rr::observe to expose the updated mutable-reference value; (6) ensure Next relates the two states and Inv holds afterward. The paper’s declaration requires {Inv} self.current, observes self.borrow, and ensures both {Next} self.current ret s2 and {Inv} s2 (Fig. 3, p. 7).

Verus form. Inference: represent iterator state with a ghost mathematical state, define a spec fn or predicate for Inv, and prove next’s ensures relation from old to new state. Inference: Iris’s iProp, OnlyPersistent, and rr::observe are RefinedRust-specific.

technique 4: higher-order map with separation-logic invariants

Inference: Use this when an iterator adapter applies a stateful closure, especially when the closure performs unsafe operations. Map<I,F> stores an iterator and closure; next calls the inner iterator and applies f only when an element exists (Fig. 4, p. 9). The challenge is that the closure may have arbitrary preconditions and mutate captured state. The paper’s solution is a client-chosen MapInv invariant strong enough to establish the closure precondition and re-establish the invariant after the closure returns (§2.4, pp. 9–10).

Steps are: (1) define MapInv over iterator and closure state; (2) require it and the inner iterator invariant; (3) prove, persistently, that an emitted inner element plus MapInv establishes the closure precondition; (4) use the closure postcondition to re-establish MapInv for new states; (5) decide where ownership emitted by the closure and the inner iterator goes. Non-duplicable ownership can be used either to re-establish MapInv or emitted to the consumer, not both; the paper’s specification always emits it to the consumer, and persistent (duplicable) parts, sliced out with OnlyPersistent, may still be used to re-establish MapInv. Footnote 5 says a more general specification leaving the choice to the client “is harder to automate reasonably” (§2.4, p. 10). (6) Instantiate Map’s Inv and Next for the None and Some cases (Fig. 4, pp. 9–10).

Verus form. Inference: encode MapInv as a tracked predicate over the iterator and closure state; require it before each call and ensure it afterward. Inference: closures need explicit specification interfaces in Verus, and linear ownership emitted to a consumer must be represented with tracked permissions or ghost state. The paper states that “Verus does not support iterators and for loops in general, having only support for plain iterators (e.g., on ranges and vectors) but not for general iterator combinators” (§7, p. 25), so a map-style encoding in Verus would need hand-written adapters. Iris’s separating conjunction, magic wand, and persistence modalities do not carry over syntactically.

technique 5: proving unsafe page allocation with ownership splitting

The ACE case study uses page tokens that own disjoint memory regions. A token invariant states that the mathematical page location owns an array of words and that the end address stays within MAX_PAGE_ADDR (Fig. 5, p. 11). The paper explains the unsafe constructor in a complete sentence: “It is unsafe to create a page token with the constructor init (line 11): page tokens assert exclusive ownership over their region of memory and this ownership is not tracked by the Rust type system; it is a precondition the caller needs to ensure.” (§3, p. 12)

For Page::divide, the paper lists the Rust implementation steps as: (1) determine the next smaller page size; (2) calculate the number of smaller pages; (3) iterate over the indices of the smaller pages with an iterator, computing for each its offset and starting address and finally creating a page token with unsafe Page::init; Fig. 6 then ends with collect (Fig. 6 and §3, p. 12). Verification takes three key steps: split the original token’s memory ownership before creating the iterator chain (“the key part of the proof that happens manually”); specify the closure; define an invariant on the map adapter that dispenses the fragments (§3, p. 13). The invariant is an iterated separating conjunction over the remaining iterations’ page fragments. The manual proof steps are stating that invariant in Rocq, showing it satisfies map’s preservation conditions (splitting array ownership, which RefinedRust does not automate), and showing the collected vector satisfies subdivided_pages; for the last, RefinedRust automatically derives an inductive property about the iteration sequence, but the induction connecting it to subdivided_pages is manual (§3, p. 13). Footnote 6 notes Rust has no unsafe closures, but “morally, this closure should be marked as unsafe” (p. 13).

Verus form. Inference: model each page as a tracked permission over a disjoint memory range, require that permission in init, and prove that divide partitions it into disjoint permissions whose union equals the original range. Inference: Verus can express range and arithmetic invariants, but the paper’s Iris ownership algebra and RefinedRust type assignments require a Verus-specific encoding.

evidence, trusted parts, and threat to VL

The paper compares RefinedRust with Creusot on seven case studies. RefinedRust takes 12.09–635.01 seconds, while Creusot takes 0.35–7.75 seconds cold and 0.35–1.56 seconds replay (Fig. 7, p. 22). In ACE, the authors verify 600 Rust LOC with 317 specification LOC and 1,455 proof LOC (Fig. 9, p. 24), plus 489, 364, and 491 LOC of Rocq theory for PageSize, Page, and PageAllocator. They report two page-allocator bugs found during verification: one incorrect pointer-arithmetic bound check and one memory-discarding bug (§6.2, p. 24). The paper says the first bug was not exploitable in the current ACE implementation, and that both were “not caught by manual inspection when writing formal specifications in the early stages of verification” (§6.2, p. 24). Inference: these are concrete findings, but the case study is one system and has no rate denominator for bug discovery.

The paper states what is trusted: “Radium and the RefinedRust encoding into it are core parts of the TCB (trusted computing base)” (§5, p. 15); the user must also trust rustc’s trait resolution and MIR transformations, and the RefinedRust frontend, although frontend encoding bugs “are likely to generate type-checking errors in Rocq” (§5.3, p. 21). Inference: a proof also depends on the written specifications being the intended ones, and on the hardware-enforced memory split described in §3 (p. 11) matching the model; the paper does not discuss these as proof assumptions. Inference: for agent-written verified Rust, traits, closures, iterators, and unsafe ownership can be brought into one proof workflow, but the manual proof ratio (1,455 proof LOC for 600 Rust LOC) and checking times of minutes on the Creusot ports (up to 635.01 s, Fig. 7; the paper reports no ACE checking times) suggest a material engineering threat to unattended generation. Existing RefinedRust work already addresses foundational high-level Rust plus unsafe pointers; VL should reuse its invariant patterns rather than rediscover them.

techniques for the catalog

• refined contracts and loop invariants — annotate mathematical values, pre/postconditions, and iterator-history invariants, then discharge generated Rocq obligations
• trait law specifications — expose order, minimum-element, and method laws as trait-level logical attributes that generic clients may assume
• relational iterator specs — describe next with state invariant and state-transition relation carrying ownership
• higher-order map invariants — use a persistent separation-logic invariant to establish closure preconditions and restore state after each element
• unsafe ownership partitioning — split a token’s memory permission, pass fragments to a closure, and prove disjoint recombination Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Our key insight is that values crossing a function boundary are always concretely known: if they were mutably borrowed before, the Rust borrow checker enforces that the borrow has ended, and so their final value is known.”): read the whole paper text; checked every quotation, figure and page reference, number (Fig. 7 time ranges, Fig. 9 LOC, bug count) and the technique steps against §2-§6 and §7; changed the technique 1 step list (refinements are assumed by RefinedRust, not user-written), the trait-contract quote and footnote 4 claim, the map ownership step (the choice is fixed by the paper’s specification), the Page::divide step list and proof-step account, the trusted-base paragraph (now cited to §5 and §5.3, with own conclusions marked Inference), the minute-scale claim (only for the Creusot ports) and added the paper’s Verus iterator limitation; the link is the DOI printed in the paper. Not checked: the Verus-form paragraphs (my own Inference, not testable against the paper), Rocq artifact contents, and references outside this paper.

Last edited: 2026-10-17