Reasoning about Interior Mutability in Rust using Library-Defined Capabilities

TL;DR

This work tackles verifying Rust programs that expose interior mutability by introducing implicit library-defined capabilities—properties not captured by Rust’s type system. It presents Mendel, the first automated verifier that uses library annotations and a first-order logic encoding to reason about clients of interiorly mutable types (e.g., Cell, RefCell, Arc, Mutex). The approach demonstrates automatic verification on standard library types and highlights near-zero client-side annotations, while acknowledging limitations and incompleteness in certain intricate cases. By combining capability-based reasoning with a modular memory-model encoding, the method enables precise framing and non-aliasing reasoning in Rust’s safe subset, potentially improving practical verification of real-world libraries.

Abstract

Existing automated verification techniques for safe Rust code rely on the strong type-system properties to reason about programs, especially to deduce which memory locations do not change (i.e., are framed) across function calls. However, these type guarantees do not hold in the presence of interior mutability (e.g., when interacting with any concurrent data structure). As a consequence, existing verification techniques for safe code such as Prusti and Creusot are either unsound or fundamentally incomplete if applied to this setting. In this work, we present the first technique capable of automatically verifying safe clients of existing interiorly mutable types. At the core of our approach, we identify a novel notion of implicit capabilities: library-defined properties that cannot be expressed using Rust's types. We propose new annotations to specify these capabilities and a first-order logic encoding suitable for program verification. We have implemented our technique in a verifier called Mendel and used it to prove absence of panics in Rust programs that make use of popular standard-library types with interior mutability, including Rc, Arc, Cell, RefCell, AtomicI32, Mutex and RwLock. Our evaluation shows that these library annotations are useful for verifying usages of real-world libraries, and powerful enough to require zero client-side annotations in many of the verified programs.

Figures (11)

• Figure 1: Example of a client of the library.
• Figure 2: The motivating example from \ref{['fig-04-introduction-example-cell']}, together with an annotated version of the API. The annotations express implicit capabilities of the type, as well as postconditions and purity for its functions.
• Figure 3: Example of a client of the library. The full annotations on the library can be seen in the test suite of the evaluation.
• Figure 4: Example of a client of the library. The then-branch is correct, while all assertions in the else-branch might fail. Mendel verifies the then-branch successfully, using the conditional capability of the type.
• Figure 5: Structural properties of capabilities.