Skip to content

Formal Models of the Rust Borrow Checker

Stacked Borrows, the 2025 Tree Borrows replacement, and the trajectory of NLL / two-phase formalisation.

memory-safety verification

§1 Provenance

§2 Claim or Mechanism

Both Stacked Borrows and Tree Borrows are operational-semantics models of pointer aliasing in Rust: every memory access checks a per-location data structure (a stack or a tree) of “permission tags”; if the access is inconsistent with the tags, the program has Undefined Behaviour. The point of these models is to enable optimisations that reorder memory accesses around opaque function calls — optimisations that would be unsound under unrestricted aliasing but are sound under the aliasing discipline.

Stacked Borrows uses a stack per memory location. Each new borrow pushes; ends-of-lifetime pop. The stack discipline is conservative: a number of common real-world patterns (e.g., two-phase borrows from NLL, certain raw-pointer patterns) are rejected as UB.

Tree Borrows replaces the stack with a tree. Children inherit permissions from their parent borrow; siblings can coexist; raw pointers form their own branch. The tree allows much more permissive behaviour while still enabling the desired optimisations. Empirically, on the 30 000 most-downloaded crates, Tree Borrows rejects 54% fewer test cases as UB than Stacked Borrows does. Tree Borrows is the leading candidate to become Rust’s official aliasing model.

Both models are mechanised in Rocq (Coq) and run as a MIRI mode (the official Rust UB-detector). NLL / two-phase borrows — historically painful for Stacked Borrows, which had to treat them as raw pointers — are first-class in Tree Borrows.

§3 Scope and Limits

Covered. Pointer aliasing semantics for &T, &mut T, Box<T>, raw pointers *const T / *mut T, and their interactions through transmute and FFI. NLL and two-phase borrows.

Not covered. The full Rust language semantics (these are aliasing models, not whole-language semantics). Relaxed-memory effects (handled separately by RustBelt-Relaxed). The proof that Rust’s safe fragment respects the aliasing model — this is the RustBelt-Tree-Borrows integration, which is ongoing 2025-2026 work and not yet complete. LLVM-level optimisations correspondence (LLVM’s noalias is similar but not identical; an LLVM-formal-semantics convergence is also ongoing).

§4 May 2026 Status

Tree Borrows is the de-facto current aliasing model for Rust, replacing Stacked Borrows in 2025-2026 discourse. MIRI has both modes; the community recommendation is Tree Borrows. The PLDI 2025 paper won the Distinguished Paper award and became PACMPL’s most-downloaded paper. While the original author (Villani) has moved on, work continues at ETH (Hostert) and MPI-SWS (Jung’s group) to build:

  1. A program logic for Tree Borrows, ideally an extension of the RustBelt lifetime logic, so that safe Rust can be proved to satisfy Tree Borrows.
  2. Tools for unsafe-code authors to check that their unsafe blocks are TB-compatible.
  3. Convergence with LLVM’s formal-semantics effort and the noalias attribute.

The 2024 McCormack et al. paper on FFI-boundary UB is the canonical reference for how Rust’s aliasing model interacts with C / C++ across extern "C" boundaries.

§5 Cost

Tree Borrows itself was a roughly two-year PhD-scale research effort at ETH/MPI-SWS, with the proofs mechanised in Rocq. The cost of adopting the model is essentially zero for the average Rust user (it’s transparent), but the cost of integrating it with RustBelt and with LLVM is the active 2025-2026 research front, expected to be multi-person-year.

§6 Mochi Adaptation Note

The relevance of borrow-check formalisation to MEP-41 is conceptual, not direct. Mochi has no borrow checker. The relevant takeaways:

  • The category of vulnerability Tree Borrows addresses — temporal memory safety bugs arising from pointer aliasing across function calls — is exactly the category vm3 handles by generation tags. Both are doing the same job: detecting “I held a reference too long” violations. Tree Borrows does it statically (the compiler rejects programs with UB); Mochi does it dynamically (the runtime invalidates Cells when the generation advances).
  • MEP-41 should cite Tree Borrows as the leading static technique for temporal safety and explicitly contrast Mochi’s runtime-generation-tag approach. Both are valid solutions to the same problem; they make different cost / expressiveness tradeoffs. Static: zero runtime cost, language-design cost. Dynamic: runtime cost (the generation field, the check on access), but no language-design tax — the Mochi programmer never has to think about lifetimes.
  • The McCormack 2024 FFI study is directly relevant: when Mochi crosses into Go-native code, the same boundary-UB issues arise. MEP-41 should note that Cell handles crossing FFI boundaries must be treated like raw pointers in Tree Borrows terms — once they cross out of the Mochi-managed region, the generation invariant is suspended and the FFI caller must restore it before passing the Cell back.
  • Mochi need not prove any aliasing-model theorem. The bytecode-language-level guarantee is “no program written in safe Mochi can hold a stale Cell”, and this is a runtime property, not a static one.

§7 Open Questions for MEP-41

  1. Should MEP-41 explicitly contrast Rust’s static lifetime/borrow approach with Mochi’s dynamic generation-tag approach as a design-tradeoff explanation for readers who arrive expecting borrow checking?
  2. The FFI / extern "C" boundary in Rust is a known UB hazard; Mochi’s Go FFI boundary is the same hazard wearing different clothes. Should MEP-41 spell out the contract for Cells crossing into Go-native code?
  3. Tree Borrows allows two-phase borrows because real code wants them. Are there Mochi patterns analogous to two-phase borrows (e.g., “I want to read the length of this vector then write to it”) that should be designed-for at the Mochi-language level?
  4. Should MEP-41 commit to a Mochi-specific equivalent of MIRI — a runtime checking mode that detects “this Cell access would have been UB under stricter rules”? Useful for fuzzing and CI.