Using Formal Reasoning to Build Concurrent Go Systems
summary
Uses TLA+ and a model checker to prove concurrency properties and find real bugs, including a gops deadlock caused by token-buffer ordering that the checker reproduces as a concrete trace. Demonstrates a pipeline race where pruning beats event insertion, fixes by moving who adds the shared object, and shows the checker exploring 900,000 states in 8 seconds. Notes this approach surfaces subtle faults preproduction and scales to real services (Amazon reports using TLA+ across many microservices).
AI-written summary · about
chapters (11)
- 0:00Formal reasoning in Go
- 2:08Why formal reasoning matters
- 7:19Programs as state machines
- 9:50TLA+ and temporal logic
- 13:02Model checkers verify specs
- 15:47Debugging Go concurrency bug
- 18:57Designing with TLA+
- 24:57Fixing pipeline deadlock
- 25:42Amazon’s TLA+ in production
- 26:46Key takeaways
- 28:52References
related talks
29mVerifying Concurrent Go Code in Coq with Goose
48mUnderstanding concurrency with behavioural types
40mDebugging concurrency programs in Go
24mMastering Concurrency in Go: From Patterns to Production
22mHigh(er) Reliability Software Patterns for Go
46mOptimizing Concurrent Applications
27mProduction Ready Concurrency
27mParadigms of Rust for the Go Developer