VerusBelt: A Semantic Foundation for Verus's Proof-Oriented Extensions to the Rust Type System

Verus is a verification tool for the Rust programming language that has already been put to use in several significant systems verification efforts. Verus offers a distinctive approach among Rust verification systems in that, in addition to offering fast SMT-based automation, it supports verification of both safe and unsafe Rust code in a single, unified framework. It achieves this by providing users with a range of proof-oriented types —types introduced specifically by Verus to aid in verification—on top of which one can then build verified implementations of Rust APIs that would otherwise require the use of unsafe Rust features. In this paper, we develop VerusBelt, the first semantic soundness proof for a significant subset of Verus. In addition to modeling the full range of Verus’s core proof-oriented types—including cells, invariants, resource algebras, and storage protocols—VerusBelt accounts (for the first time) for full-fledged Rust lifetimes, concurrency and thread safety, and mutable borrows. A central challenge involves building a model of shared borrows that is generic enough to support storage protocols—we tackle this by marrying RustBelt’s lifetime logic with the Leaf library for temporary resource sharing in Iris. All our proofs are mechanized in Iris/Rocq.