The Verification of a Distributed System
summary
Covers practical verification: use TLA+ and Coq for provable specs (Amazon uses them on S3 and finds serious bugs), rely on 77% reproduced by unit tests and find that error‑handling tests prevent ~58% of catastrophic failures, run small clusters (three nodes reproduce ~90% of failures), use Jepsen fault injection, Chaos Monkey, property‑based testing (QuickCheck/ScalaCheck) to shrink failing inputs, and practice canaries and game days; each technique increases confidence but none guarantees absence of bugs.
AI-written summary · about
chapters (7)
- 0:00Start
- 2:43Overview
- 8:41Program Extraction
- 20:50ScalaCheck Examples
- 23:15Netflix Simian Army
- 29:05Game Day at Stripe
- 33:58Verifying System Complexity
related talks
38mThe Verification of a Distributed System
19mBridging the Verifiability Gap: Why We Need More From Our Specs and How We Get It
20mSift: Using Refinement-guided Automation to Verify Complex Distributed Systems
53mFrom Algorithm to Production: How to Approach Verification of Distributed Systems
34mThe Math Behind Distributed Systems
25mProperty-agnostic base case extension for scalable verification of distributed systems
27mUnderstanding Distributed Systems with Deterministic Simulation
42mWelcome to TLA-La-Land (or An Introduction to Software Verification)