  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.
