The Verification of a Distributed System
summary
Practical verification mixes formal specs, targeted tests, and injected failures. Teams use TLA+ and model checkers — Amazon verifies 10+ core services and finds two serious bugs alongside unit and integration tests. A study of 198 failures shows 98% reproduce on three nodes or fewer and 58% trace to missing error-handling. Property-based tools like QuickCheck/ScalaCheck discover counterexamples, while fault injectors — Netflix’s Chaos Monkey, Jepsen and lineage-driven Molly — trigger real-world partitions and expose consistency bugs. Canaries only validate the golden path.
AI-written summary · about
chapters (36)
- 0:00Intro
- 0:36About Caitie
- 1:13What is a distributed system
- 1:57Were all building distributed systems
- 2:29Any size system
- 3:02Overview
- 3:40Github Page
- 3:59Testing Properties
- 5:00Formal Verification
- 5:26Formal Specifications
- 6:17Our Clock
- 7:06Amazon
- 7:28Highlights
- 8:30Formal Methods
- 9:40Unit Tests
- 10:13Type Systems
- 12:31Integration Tests
- 14:45Staging Environment
- 15:32Error Handling
- 17:42Property Based Testing
- 18:21QuickCheck
- 20:17ScalaCheck
- 21:28Fault Injection
- 22:01Netflix Simian Army
- 22:34Jepsen
- 23:06Distributed Systems
- 24:09Game Days
- 25:47How to Run a Game Day
- 26:47Stripes Game Day
- 28:29Testing in Production
- 29:40Monitoring is not testing
- 30:15Verification
- 32:30Lineage Driven Fault Injection
- 35:00Netflix Fault Injection
- 36:43Conclusion
- 37:22Quote
related talks
48mThe Verification of a Distributed System
49mHow do we do it? Testing and Verifying bugs for released software
19mBridging the Verifiability Gap: Why We Need More From Our Specs and How We Get It
18mPreview: Verification (Correctness)
18mPreview: Verification (Correctness & Debugging)
53mFrom Algorithm to Production: How to Approach Verification of Distributed Systems
20mSift: Using Refinement-guided Automation to Verify Complex Distributed Systems
23mBeyond Tests What to Verify in AI Generated Code