一句话：为 Verus 的核心证明类型及 Rust 生命周期、并发与可变借用建立首个语义可靠性证明。
Verus 是面向 Rust 的验证工具，通过一组面向证明的类型在统一框架中验证安全与 unsafe Rust，但其类型系统扩展缺乏语义可靠性基础。本文提出 VerusBelt，为 Verus 的核心子集建立首个语义可靠性证明。该模型涵盖 cells、invariants、resource algebras 与 storage protocols 等证明类型，并首次纳入完整的 Rust 生命周期、并发与线程安全以及可变借用。为支持 storage protocols，作者将 RustBelt 的生命周期逻辑与 Iris 的 Leaf 库结合，构建通用的共享借用模型。全部证明在 Iris/Rocq 中机器化。
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.
@article{HanceEMD26,
title = {VerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type System},
author = {Travis Hance and Laila Elbeheiry and Yusuke Matsushita and Derek Dreyer},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808325}
}