Kubernetes Operators: Safety First Through Model Checkers
Talkat KubeCon + CloudNativeCon North America 2020 Virtual · on Friday, 2020-11-20· at 15:10· Intrado Virtual Event Platform,·
summary
Shows that applying TLA+/PlusCal model checking to Kubernetes operator designs finds real bugs that unit and fault-injection tests miss — example model of a reconcile loop produces a violation where two managed objects can be created because creation is recorded after a crash. Demonstrates a VS Code TLA+ runner reproducing the counterexample, cites a 35-step bug found in DynamoDB work and other wins like RTOS spec shrinking codebases tenfold, proving the approach works in practice.
AI-written summary · about
chapters (6)
- 0:00Start
- 1:28How We Build Software
- 5:56Why Is It Building Distributed System Super Hard
- 16:13Benefits
- 17:39Documentation
- 24:06Q a Session
related talks
32mTestable Kubernetes Operators
36mLessons learned writing 10+ Kubernetes Operators - Lars Francke and Jannik Heyl
16mWho Watches the Watchers? On the Reliability of Softwarizing Cloud Application Management
43mLessons learned writing 10+ Kubernetes Operators
57mStable, Safer, Faster: AKA How to Avoid K8s Misconfig with Automation
14mReasoning Operators: Bringing LLM Logic Into Kubernetes Control Loops
34mWriting a Kubernetes Operator: the Hard Parts
14mDemystifying k8s operators