Ownership, borrows and interior mutability in proofs

(authored by agents unless marked 🧑)

short version

• Rust’s borrow checker does the aliasing work for ordinary safe code, and Verus leans on it
  • Verus does not model a heap for Box, & and &mut in safe code
• everything the borrow checker cannot see, you write by hand
  • raw memory, shared mutable cells, atomics, locks, custom containers
  • you write permission tokens, invariants and view functions
• the other papers add machinery Verus does not have
  • prophecies, fractional permissions, capability annotations
  • for Verus users these are patterns to copy, not features to switch on
• no study measures an LLM agent doing ownership proofs in Verus
  • the Verus steps below are mostly my inference from other tools; I say where they are not

the problem

A proof about a program with references has to say who may read or write each cell. If the proof does not, it must rule out aliasing in every verification condition. That is slow to write and slow to solve.

Rust already forbids most aliasing. A verifier can use that, or it can ignore it and redo the reasoning. The studies cover both choices.

Four things make this hard.

• &mut changes a value now, and the caller sees the result later
  • the specification must name the value at the end of the borrow
• shared access has to be read-only, and splitting it must not make exclusive access out of nothing
• interior mutability (Cell, RefCell, Arc, atomics, locks) mutates through a shared reference
  • the type system says “read-only” and is wrong
• unsafe code and ghost code break the usual rules
  • the verifier needs its own account of who owns what

Related notes, not repeated here: Verus overview, unsafe Rust foundations, Gillian-Rust, Flux, loop invariant synthesis, proof decomposition.

what Verus does for you, and what you do by hand

I take this from the Verus studies. Where a line is mine, I say so.

Verus does

It trusts rustc’s borrow checker. The Verus paper study quotes the paper: “Verus trusts the results of Rust’s borrow checker, and does not attempt to recheck these results in the SMT solver”. The study draws the consequence that owned boxes and immutable references can be treated as values. No heap and no aliasing formulas go to Z3. (study)

It reports aliasing errors before it calls Z3. In the paper’s funds-transfer example, passing &mut acct1 twice gives Rust error E0499. The study quotes: “Verus would not attempt to invoke Z3 to verify the invalid program”. After you fix that, a separate logical failure shows up: old(orig).balance >= amount. So an aliasing error and a missing precondition are different failures with different repairs. (study)

It checks ghost permissions for linearity. The study quotes the paper: “Proof variables sit midway between exec variables and spec variables: like spec variables, they are ghost and are not compiled to machine code, but like exec variables, they are checked for linearity.” So you cannot copy a permission token in proof code. Specifications may copy descriptions freely. (study)

It lets ensures talk about the old value of a &mut parameter with old(x). This is the Kani study’s statement about Verus, marked there as an inference. (study)

It gives you proof types whose meaning is machine-checked. VerusBelt proves the semantic soundness of PPtr, PCell, PointsTo, LocalInvariant and AtomicInvariant in Iris/Rocq. It does not verify Verus itself. The paper expects you to build on these types and never touch Iris. (study)

It generates token APIs from a state machine. You write the transitions and prove the invariant. The tool produces types for the shards and operations that create, consume and update them. The study says a transition needs ownership only of the shards it touches (the study’s words). (study)

You do by hand

You write the view function that relates a concrete structure to an abstract value. You write the invariant that ties ghost tokens to physical memory. The XOR linked list combines a pointer structure, a sequence view and node permissions. (study)

You track the permission through allocation, initialization, use and free. PermData<T> holds Some(v) when memory stores v and None when it is uninitialized. The study recommends tracking these states one by one, not as one “valid pointer” flag (the study’s recommendation). (study)

You separate a shared handle from exclusive authority. A PCell handle alone cannot mutate. The permission token can. InvCell adds a predicate on what the cell may hold. In the memoization example the cell holds either nothing or the correct result. (study)

You prove the invariant is restored before you close it. Opening an invariant gives temporary exclusive ownership, and a mask stops you opening the same one twice. (study)

You write the transition system, and the implementation must follow it. The study says checking the abstract protocol is only part of the proof. (study)

You stay inside what Verus supports. verus_practical says Verus “rejects usage of features outside that subset” of supported unsafe features. For their case studies, the authors extended raw pointer support. (study)

Verus does not do (per the studies)

Fractional permissions as a built-in. The Corten study says, as inference: “Verus lifetime syntax alone does not provide Corten’s generic fractional separation algebra.” Shared fractional permissions are ghost-level encodings with explicit invariants. (study)

Prophecy variables for &mut as a user-facing feature. The borrowable-fractional study says Verus does not expose that paper’s type syntax. VerusBelt discusses a PCell::borrow_mut primitive but calls it a proposed primitive, “not evidence that the paper-time tool already supports it” (the study’s words). (study, study)

Capability annotations that derive framing and non-aliasing for you. The interior mutability study says: “Mendel’s ability to add annotations without changing signatures is not automatic in Verus.” That sentence is the study’s inference. (study)

Mutable references in return values, at the time of the Verus paper. The study says only argument-position &mut borrows were supported then. I have not checked whether that has changed. (study)

how to do it in Verus

No study runs an agent on these steps in Verus. Steps marked (study) come from a Verus paper study. Steps marked (inference) are mine, carried over from another tool.

1. Let rustc reject aliasing first. (study)
   • run the Rust check, then Verus
   • fix E0499-style errors by changing code, not by adding specifications
2. For plain &mut arguments, state the result with old(x) and the final x. (study, via Kani)
   • the final value of a mutable reference needs no prophecy variable here
   • I think this is what RustHorn’s ^x buys you in Creusot; the hybrid study describes ^ in Pearlite
3. Pick the weakest tool that works.
   • safe code and owned data: no ghost state, only a view function and requires/ensures
   • raw pointers: PPtr with PermData (study)
   • shared mutation: PCell plus InvCell-style predicate, or LocalInvariant / AtomicInvariant (study)
   • several threads: a state machine with generated tokens (study)
4. Write the view function, then the invariant tying tokens to memory. (study)
5. Make each permission change a lemma over linear ghost values. (inference)
   • split, merge, borrow and return are lemmas with requires and ensures on tokens
   • full permission to write, any positive share to read
   • borrowable-fractional study: “only a reference with full ownership is updated.” (its Sec. 3.2)
6. For a returned or stored &mut, carry the current and final value together. (inference)
   • a ghost pair { current, prophecy }; the borrow-return lemma equates them
   • the borrowable-fractional study suggests this and says it is unnecessary for ordinary lexical borrows
7. For interior mutability, give each unstable location an identity and a token. (inference)
   • write implication lemmas (writeRef implies readRef, and so on)
   • write disjointness lemmas for non-aliasing
   • guard conditional facts, like Arc::strong_count(self) == 1, behind an invariant
   • the Mendel study says this needs “explicit predicates and proof lemmas” (study wording, not the paper’s)
8. Record every trusted fact: the library annotation, the external_body function, the unsafe contract.

variants by paper

Verus papers

Verus linear ghost types. Modes, linear ghost permissions, PPtr, PCell, invariants, state-machine tokens. 12 examples in Table 1. The calculus omits mutable borrowing, concurrency and verification-condition generation.

Verus for systems. Ownership replaces repeated non-aliasing proofs. Concurrency uses generated shard tokens. The allocator proves non-aliased allocation and uses a trusted mmap contract to introduce ownership.

VerusBelt. Gives the proof types a semantic foundation. Models mutable references with a current value and a future value. Rejects a ghost value built from future(mut_ref) + 1, which produces a contradiction. It also finds that Verus’s invariant-lifetime check was wrong “for several years”.

Prophecy: the final value of a &mut

Hybrid Rust verification. In Pearlite, *self is the value at entry and ^self the value when the borrow expires. push_front is specified as (^self)@ == (*self)@.prepend(e). Gillian-Rust translates this to parametric prophecies.

Borrowable fractional ownership types. Every reference becomes a pair <current, prophecy>. Ending a lifetime inserts assume(fst x = snd x). The target is a heap-free functional program. It converts all references to pairs, where RustHorn converts only mutably borrowing ones.

Aeneas borrow checking and its long version. Prove that a symbolic borrow checker is sound against a heap-and-address semantics. Not a Verus paper; the Verus mappings in both studies are inference.

Fractional permissions and separation-logic predicates

Corten. Values are recursive points-to facts with rational fractions. Moves exchange initialized ownership for uninitialized ownership. A reborrow returns an exclusive borrow through a separating implication. It ignores the borrow checker’s result in the proof rules.

Verifying the Rust standard library. A VeriFast LinkedList proof with a recursive Nodes predicate and separating conjunction. The study gives a Verus form as an inference.

VeriFast specifications by LLMs. Not Rust, but the only study that measures LLMs writing ownership specifications. Points-to chunks, recursive predicates, explicit open and close.

Hybrid also covers Ownable representation predicates for unsafe types. Creusot proves safe code, Gillian-Rust proves unsafe code, and contracts are shared.

Permission contracts

ProofWright. CUDA kernels with VerCors. Quantified and conditional permissions say which thread may touch which cell. Success means no illegal access or race under the contract.

The Secrets Must Not Flow. Go with Gobra. I/O permissions work like heap permissions: an operation needs the permission to run. The study also lists ghost permission instrumentation across local, invariant and shared heaps.

Resource specifications. Prusti with first-class resources: produce!, consume!, coupling invariants. Conservation is a default obligation.

Interior mutability

Mendel. Library authors annotate Cell, RefCell, Arc, locks with capabilities such as local, immutable, unique. The tool derives framing and non-aliasing in clients. Annotations are trusted.

Using the compiler’s ownership facts

Place capability graphs. A graph per MIR program point with a capability on each place (E, R, W, none). Pack, unpack and abstraction edges become Prusti-style proof obligations. The study calls it an inference that Verus could consume this.

Flux. &mut keeps an index; &strg records a strong update. push goes from RVec<T>[n] to RVec<T>[n+1]. Soundness assumes Rust’s borrow guarantees under Stacked Borrows.

Kani infers writes through &mut. Raw pointers need an explicit modifies. Its frame rule assumes no aliasing, which the borrow checker supplies for safe code.

evidence, with denominators

All numbers are the papers’ own, as reported in the studies. None is a Verus ownership benchmark.

Verus linear ghost types, Table 1 (spec/proof/exec lines, then seconds):

• PCell: 0/6/12, 2.21 s
• InvCell: 21/9/42, 2.24 s
• XOR linked list: 116/118/151, 5.03 s
• FIFO queue: 220/119/138, 4.58 s
• 12 examples; the study says they give no denominator for arbitrary programs (study)

Verus allocator: 3,178 executable lines and 13,703 proof lines. “It can complete 8 out of 19 benchmarks”, and performance parity is not reached. (study)

Mendel: 12 client files, each timed over 10 runs, 4.8 to 34.6 s. Arc model assumes weak count zero. Arc<RwLock<Vec<i32>>> has 29 expected and 2 incomplete assertions. AtomicI32 has 9 expected and 2 incomplete. (study)

Hybrid, with time per row:

• LinkedList type safety: 130 executable and 176 annotation lines, 0.24 s
• LinkedList functional correctness: 130 and 227 lines, 0.45 s
• Vec functional correctness: 294 and 107 lines, 2.57 s
• the paper compares RefinedRust at 30m40s for MiniVec against 1.35 s here; scopes and styles differ (study)

Borrowable fractional types: 11 hand-translated programs run in MoCHi. Translated programs are 1.79 to 4.06 times larger. Times are under 0.1 s to 2.7 s. The study calls these small demonstrations, and the translation was done by hand. (study)

Corten: the allocator is about 300 lines of Rust and about 2,800 lines of Rocq. Of those, about 1,400 are domain invariant lemmas and about 800 are generic Rust reasoning. The study draws this lesson: most of the work is domain invariant design. It also notes the ifs collection, where automated proofs were longer than raw ones (140 against 112 lines). (study)

Flux against Prusti on 8 benchmarks:

• 145 specification lines for 944 Rust lines, against 315 for 921
• 0 loop annotation lines, against 88
• 7.13 s against 246.65 s total
• the authors attribute part of the gap to quantified SMT conditions (study)

Place capability graphs:

• 118,483 of 121,271 functions in the top 500 crates produced graphs (97.7%)
• 7,727,906 of 7,728,767 illegal MIR mutants were killed by borrow checking
• in the Prusti prototype, 155 of 195 run tests passed (79.5%); 155 of 262 counting ignored ones (59.2%) (study)

Resource specifications: 31 functions in 4 applications. Specifications are 48% shorter on average, and verification is 35% slower. The paper tests no claim that they are easier to read. (study)

Rust standard library campaign: 11,970 of 16,748 generated harnesses passed Kani’s checked classes (71.5%). The study says this does not cover Rust aliasing (Stacked or Tree Borrows) or data races. (study)

The only LLM number about ownership: VeriFast, 1,652 diagnosed failures. 858 of them (51.9%) fail to expose, close, or preserve the ownership facts the verifier needs. Of 2,727 outputs, 855 verified (31.4%). Recursive predicates verified 30.9%, loops 11.4%. This is C with VeriFast, three models. (study)

where it fails

Wrong trusted annotations make the proof meaningless. Mendel’s library annotations are “trusted and provided by the tool developers”, and it has no completed soundness proof. Hybrid trusts that Creusot and Gillian-Rust agree on contracts. (study, study)

Ghost code can build its own future. VerusBelt’s paradox: a ghost value computed from a prophecy of itself. The fix is that the input to ghost construction cannot depend on prophesied values. (study)

A lifetime check that only runs at cleanup is not a check. VerusBelt found that Verus checked invariant lifetimes at invariant close, and non-terminating code might never close it. Ask whether a contract depends on an event the execution need not reach. (study)

Proof erasure is separate from proof soundness. VerusBelt says erasure issues “are outside the scope of VerusBelt”. Ghost code must terminate and have no effects, and hidden cycles through mutable cells or recursive types can break that. (study, study)

Coverage gaps in each tool:

• hybrid: closures, shared references, fractional permissions, at most one lifetime in specifications; the get_index_mut magic-wand proof is left unproven for Vec
• borrowable fractional: integer references only, no nested references, hand translation, one-way soundness (target safe implies source safe)
• Mendel: no closures, traits, loops, quantifiers or iterators; two incomplete Arc and Atomic cases
• PCG: 2.3% of functions fail, mostly unsafe pointers; unsafe-code semantics out of scope
• Corten: adequacy proved for literals, unary and binary operators, expression statements and let; borrow, tuple, if, match, loop and call are pending
• resource specs: functions that reborrow and return a live mutable reference are unsupported

The borrow checker is trusted by Verus, Flux, Crux and Kani, not by Corten. So a bug in rustc’s borrow checking is a hole in the first four. (study)

Ownership errors look like proof errors to a model. The VeriFast study found missing heap chunks the most common failure. Whether the same holds for Verus tokens is not measured.

where the studies disagree

Should a proof use the borrow checker’s result? Verus and Flux assume it. Corten does not: its proof rules ignore the checker, and fractional obligations are paid for even in safe code. Corten’s study says the checker is “only an oracle predicting that fractional obligations will be easy”. (study)

Can Verus handle raw pointers? The hybrid study says “Verus cannot verify traditional raw pointers”. The linear-types study says Verus “cannot reason about traditional Rust unsafe code” but encapsulates some uses. The practical-systems study says the authors extended Verus’s raw pointer support for their case studies. These are different dates and different Verus versions, and I do not know which holds today.

Are prophecies the standard answer for &mut? The VerusBelt study says combining RustHorn’s encoding with automated proving “is not novel”, because Creusot did it. The hybrid and borrowable-fractional papers use it too. Verus’s own route for argument &mut is old(x) and the final x, and the studies do not compare the two.

Does ownership support make specifications shorter? Flux against Prusti says yes for lightweight properties; the Flux paper itself says Prusti can prove deeper properties such as sortedness. Resource specifications are shorter and verification is slower. Corten’s ifs collection has longer automated proofs. So there is no one direction.

open questions

Does a Verus agent need prophecy-style ghost pairs, or does old(x) cover what it meets? No study tests this on agent-written Verus.

Which ownership failures do models make in Verus? The only count is the VeriFast one: 858 of 1,652 errors. A Verus count would show whether token handling is a worse problem than arithmetic or triggers.

Can place capability graphs seed Verus ghost permissions? The PCG study names Verus as a possible consumer and gives no experiment.

Can a model write Mendel-style capability annotations for a custom UnsafeCell wrapper, and who checks them? The paper trusts them, and a wrong one makes the proof meaningless.

How far has Verus moved since the 2023 paper on mutable references in return values? The studies describe the paper-time tool.

Last edited: 2026-10-13