Verus: Verifying Rust Programs using Linear Ghost Types
summary
Verus is an SMT-based verifier that embeds proofs in Rust and uses linear ghost permissions to represent ownership-aligned memory permissions; the tool demands relinquishing a permission on dealloc and catches read-after-free via the Rust borrow checker. It implements a mode system: exact/proof/spec so executable code is checked for borrowing while proofs and specs are erased. The authors verify pointer code (pptr API), an xor-based doubly-linked list, interior mutability patterns, and concurrent protocols; the paper proves type safety and termination and supplies reusable artifacts on GitHub.
AI-written summary · about
chapters (4)
- 0:00Introduction to Verus
- 0:16Mechanism and application
- 12:19Project goals and conclusion
- 13:57Q&A session
related talks
20mVerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type(…)
19mA Hybrid Approach to Semi-automated Rust Verification
21mUsing Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust
17mRefinedRust: A Type System for High-Assurance Verification of Rust Programs
23mA Verified Thread-Safe Array in Rust
50mRust's Borrow Checker Proven Correct!
14mA Refinement Methodology for Distributed Programs in Rust
15mAeneas: Rust Verification by Functional Translation