A Refinement Methodology for Distributed Programs in Rust
summary
Presents a bottom-up refinement method that pairs guarded transition systems with a novel locally inductive invariants proof rule, implemented as a Rust library that uses ownership to represent guards and runs on an off‑the‑shelf verifier (Prusti). Verifies evolving implementations from a single‑threaded Memcached to a fine‑grain locked multithreaded variant, plus Paxos and a lock‑free hash set, demonstrating practical performance (uses atomics/threads) and reproducible artifacts rather than thousands of manual interactive proofs.
AI-written summary · about
chapters (10)
- 0:00Refinement methodology intro
- 1:25Memcached case study in Rust
- 2:28Transition systems technique
- 4:17Verifying single-step actions
- 6:06Modular verification
- 7:50Inductive invariants and guards
- 9:39Decoupling models from impls
- 10:22Evaluation and case studies
- 11:47Summary and future
- 12:28Q&A
related talks
17mRefinedRust: A Type System for High-Assurance Verification of Rust Programs
20mSift: Using Refinement-guided Automation to Verify Complex Distributed Systems
40mRust’s approach of getting things right
19mA Hybrid Approach to Semi-automated Rust Verification
21m“Fearless Refactoring & the Art of Argument-Free Rust”
18mVerus: Verifying Rust Programs using Linear Ghost Types
20mModular Specification and Verification of Closures in Rust
19mRavencheck: Effectively-Propositional Reasoning for Rust