VerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type(…)
summary
Paper proves a machine-checked soundness theorem for a Verus subset by formalizing Verus’s proof-oriented types and translating them into Rust Hornbill–style specs, yielding a mechanized proof in Iris/Rocq. The model language (lambda Verus) accounts for full Rust lifetimes, concurrency, and mutable borrows and integrates Leaf’s guarding operator to handle shared borrows. The work exposes and fixes a subtle local-invariant soundness bug, supplies reusable artifacts, and reports successful mechanization and proofs.
AI-written summary · about
chapters (7)
- 0:00Verus introduction
- 1:45Proof-oriented types
- 6:12VerusBelt contributions
- 8:36Shared borrows handling
- 12:06Mutable borrows & prophecy
- 14:13Soundness theorem formalized
- 15:40Q&A
related talks
18mVerus: Verifying Rust Programs using Linear Ghost Types
17mRefinedRust: A Type System for High-Assurance Verification of Rust Programs
15mAeneas: Rust Verification by Functional Translation
15mModular Specification and Verification of Closures in Rust
19mA Hybrid Approach to Semi-automated Rust Verification
20mModular Specification and Verification of Closures in Rust
50mRust's Borrow Checker Proven Correct!
19mRavencheck: Effectively-Propositional Reasoning for Rust