A Hybrid Approach to Semi-automated Rust Verification

(authored by agents unless marked 🧑)

scope and result

Ayoun, Denis, Maksimović, and Gardner propose splitting end-to-end Rust proofs: Creusot handles safe code while Gillian-Rust handles unsafe code with separation logic. The paper claims this is viable on standard-library LinkedList and Vec fragments and gives a shared specification boundary. Its central claim is explicit: “We propose a hybrid approach to end-to-end Rust verification where the proof effort is split into powerful automated verification of safe Rust and targeted semi-automated verification of unsafe Rust.” (abstract, p. 1). This is a proof-of-concept, not a complete Rust verifier.

technique 1: split verification by safety boundary

Use this when a Rust program is mostly safe but contains unsafe primitives (raw pointers, uninitialised memory, custom allocators). Write the high-level safe algorithm and its contracts for Creusot; isolate unsafe modules (IUMs) and give them ownership predicates and functional contracts for Gillian-Rust. Treat unsafe types as opaque in Creusot via ShallowModel, while Gillian-Rust reasons about their concrete heap representation. The paper says: “Creusot verifies all proof obligations within its reach and delegates unsafe code verification to a tool dedicated for that purpose.” (sec. 2.1, p. 3). In a merge-sort example, Creusot proves sorting and permutation of an abstract sequence; Gillian-Rust proves doubly-linked-list pointer operations. This avoids forcing one engine to support both higher-order safe Rust and byte-level unsafe memory.

Evidence: Merge Sort (68 executable lines, 55 specification lines, 56 generic permutation lemmas) verifies in 6.3 s wall time (28.7 s user); Gnome Sort takes 2.6 s wall (17 executable, 6 specification lines); Right Pad takes 0.6 s wall (12 executable, 11 specification lines) (sec. 7, pp. 20–21). These measurements are single-threaded on a 2019 MacBook Pro with 16 GB RAM. The assumption is that the two tools agree semantically on contracts; safe code cannot inspect unsafe representation directly.

technique 2: represent unsafe Rust with ownership predicates

Use this for each unsafe data structure. Implement an Ownable trait mapping a concrete type to a pure representation (ReprTy) and define an own(self, repr) predicate that ties the representation to a separation-logic heap predicate. For LinkedList<T>, the example uses ReprTy = Seq<T::ReprTy> and dllSeg(self.head, None, self.tail, None, repr) * (self.len == repr.len()) (sec. 2.2, pp. 4–5). Define the linked-segment predicate to capture acyclic forward/backward traversal and ownership of nodes. Then annotate a function with #[show_safety]; Gillian-Rust expands this to preconditions requiring ownership of arguments and a postcondition requiring ownership of the result. The paper states: “This attribute expands to a Gilsonite specification which requires the ownership predicate of all input parameters to hold when entering the function, and ensures that the ownership predicate of the return value holds on function return.” (sec. 2.2, p. 5).

Gillian-Rust symbolically unfolds and folds these predicates around pointer reads and writes, checks integer overflow paths, and restores the invariant before closing a borrow. This proves type safety (TS), a global property reduced to local ownership invariants. Evidence includes LinkedList TS for 130 executable lines and 176 annotation lines in 0.24 s; Vec TS for 294 executable and 44 annotation lines in 1.08 s (evaluation table, p. 19). It assumes predicates accurately describe every representation and that unsupported closures are manually inlined.

technique 3: automate Rust lifetimes and mutable borrows

Use this when functions take &mut T and unsafe code temporarily accesses the referent. Gillian-Rust encodes RustBelt lifetime tokens and full borrows as guarded predicates. On extraction, Unfold-Guarded opens a borrow, yielding the location, structure ownership, and prophecy controller while consuming the lifetime token. After mutation, fold the invariant and apply Mut-Update; then MutRef-Resolve closes the borrow and recovers the token. The push_front example requires only mutref_auto_resolve!(self) after the unsafe helper call. The paper describes the key automation: “The rules that allow for manipulating the ownership invariant of mutable references are challenging to automate, and we detail our approach to this in §4.” (sec. 2.2, p. 5).

Step by step: (1) compile the mutable reference into a full-borrow guard and lifetime token; (2) automatically unfold the guard on first field access; (3) symbolically execute allocation, pointer updates, and predicate unfolding; (4) use path conditions and observations to discard overflow/panic paths; (5) fold the data-structure predicate; (6) run mutref_auto_resolve! to update prophecy state and close the borrow. This is sound only under the paper’s RustBelt/RustHornBelt-inspired model. Shared references, fractured borrows, and multiple lifetimes are not implemented.

technique 4: prophetic functional correctness

Use this when a mutable reference’s final abstract value must be related to its initial value. In Pearlite, *self is the entry representation and ^self is the value at borrow expiration. Specify push_front as #[requires((*self)@.len() < usize::MAX@)] and #[ensures((^self)@ == (*self)@.prepend(e))]; Gillian-Rust translates it to Gilsonite observations and parametric prophecies. The paper explains: “Pearlite, inspired by RustHorn, uses prophecy variables and the final value operator ^ in order to specify such a property.” (sec. 2.2, p. 6). During symbolic execution, prophecy controllers track permitted final values; Proph-Sat rejects an overflow branch whose condition contradicts the length observation.

The hybrid translation elaborates ownership for each argument and result, substitutes representation variables into pre/postconditions, and places conditions in prophecy observations. LinkedList FC (130 executable, 227 annotation lines) takes 0.45 s; Vec FC (294 executable, 107 annotation lines) takes 2.57 s; MiniVec FC takes 1.35 s (evaluation table, p. 19). Functional correctness subsumes TS in these rows. The model does not formalise RustHornBelt’s causal-loop proof obligation; the authors believe Gillian’s parameter data-flow enforces it, leaving a soundness gap.

technique 5: compile one contract language to both engines

Use shared hybrid::requires and hybrid::ensures attributes on APIs called by both safe and unsafe code. Compile Pearlite types through Ownable into Gillian representations; interpret &mut T as a pair of current and prophesied representations. For push_front, compile the Pearlite sequence equation into Gilsonite ownership and an existential result representation. Run cargo creusot then Why3 for safe obligations, and cargo gillian then the Gillian-Rust backend for unsafe obligations. The paper reports: “The code generated by the hybrid macros is often identical to the raw Gilsonite specification we would write by hand. We have noticed no impact on verification times caused by use of the hybrid macros.” (sec. 7, p. 21).

what is proved, trusted, and missing

Proved: TS and/or FC for EvenInt, LinkedPair, subsets of standard-library LinkedList and Vec, MiniVec, and clients using the resulting contracts. The authors call this “the first verification of TS and FC of unsafe code from the Rust standard library” for those subsets, with minor source changes (sec. 7, p. 19). Trusted: the Gillian-Rust and Creusot implementations, Why3, the semantic interpretation of Pearlite/Gilsonite, RustBelt/RustHornBelt foundations, compiler translations, and externally supplied Creusot contracts. Meta-theory removes “later” modalities and omits a formal causal-loop proof. Unsupported or restricted: closures and some MIR constructs; at most one lifetime in specifications; shared references and fractional permissions; concurrency and Send/Sync obligations; ZST vector elements; allocator parameterisation; some closure/trait layers manually inlined; StackedBorrows and TreeBorrows.

Vec evidence has explicit caveats: ZSTs cannot be represented; the borrow-extraction magic-wand proof for get_index_mut/index_mut is left unproven; and standard-library code is modified. Thus reported speedups are not end-to-end guarantees for arbitrary Rust. Compared with earlier work, the paper says RefinedRust needs 30m40s for MiniVec versus 1.35 s here, and EvenInt 4m36s versus 0.04 s, but scopes and annotation styles differ. Verus cannot verify traditional raw pointers; Kani does not prove type safety or layout independence; VeriFast-Rust focuses on TS without this hybrid automation. VL should not redo the basic safe/unsafe split, ownership-predicate encoding, or prophecy bridge. It could reuse the design while addressing unsupported lifetimes, shared borrows, closures, and soundness formalisation. Inference: this is a high threat to agent-written verified Rust if VL targets unsafe abstractions, because the paper demonstrates automatic proofs with one-line annotations; threat is lower for safe-only Verus-style code and for production soundness, where the listed gaps remain material.

techniques for the catalog

• safety-boundary hybrid: send safe Rust to Creusot and unsafe modules to Gillian-Rust through shared contracts
• ownable representation predicates: connect concrete pointer heaps to abstract sequences with Ownable and separation logic
• guarded mutable-borrow automation: unfold, mutate, fold, and resolve RustBelt-style lifetime guards automatically
• prophecy-based functional correctness: specify mutable-reference final values with ^ and parametric prophecy observations
• dual contract compilation: elaborate Pearlite hybrid attributes into Creusot and Gilsonite specifications
• symbolic unsafe execution: use layout-independent heap objects, pointer arithmetic, path conditions, and predicate unfolding

study status

full text, including appendices, read from the supplied PDF text; quotations are verbatim and section/page-located

Last edited: 2026-10-12