Converos: Practical Model Checking for Verifying Rust OS Kernel Concurrency
summary
Claims a practical workflow that verifies 12 Rust OS concurrency modules (≈4k LOC) using PlusCal/TLC and lightweight logging, finds 20 real bugs (9 via model checking, 11 as byproducts), and completes in four person‑months. It translates Rust into low‑level specs, uses multi-grain specs to avoid state explosion, and performs missing-event trace validation to match noisy timestamps and incomplete logs. Counterexamples turn into reproducible tests and fixes; specs are incrementally tightened until TLC proves safety and liveness.
AI-written summary · about
chapters (12)
- 0:00Converos introduction
- 1:21OS kernel challenges
- 2:05Converos workflow
- 3:49Multi-layered specs
- 5:55Trace conformance
- 8:07Incomplete logs handling
- 10:15Logging efficiency
- 11:19Evaluation results
- 12:23Concurrency bug case
- 13:06Reader-writer bug
- 13:49Manual effort and scalability
- 14:13Summary
related talks
21mA Tour of Empirical Verification in Rust
58mRust for The Curious C++ Developers
19mA Hybrid Approach to Semi-automated Rust Verification
17mRefinedRust: A Type System for High-Assurance Verification of Rust Programs
28mBuild bigger in less time: code testing beyond the basics
50mRust's Borrow Checker Proven Correct!
31mValidating Rust for industry: Certification meets formal analysis
28mRust on Morello