Software Verificationpalooza
Greg Colombo and Rain Paharia from Oxide Computer Company discuss rigorous software verification methods, specifically TLA+ for model checking distributed systems and the proptest Rust crate for property-based testing. Greg explains how he used TLA+ to verify the orchestration of live VM migration, uncovering race conditions and bugs in the control plane that were difficult to reproduce with standard integration tests. Rain details his use of proptest to validate complex data structures like 'buff-list' and 'Guppy' by comparing them against oracles like the standard library and Cargo, finding numerous bugs in both his code and upstream dependencies. The episode highlights how formal methods and property-based testing serve as complementary tools for ensuring correctness in high-concurrency, distributed environments.