Kubernetes Operators: Safety First Through Model Checkers - Neven Miculinic, grid.ai

Today's Kubernetes Operators aren't just a fancy toy, but utilities managing critical infrastructure. Many best practices are already applied, increasing their safety: unit/e2e testing, code reviews and post mortem analysis. This talk introduces some more recent tooling for working developers toolbox: model checkers. The likes of TLA+ and alloy have already been used for helping design many real-world systems, from S3 all the way to RTOS (real-time operating system) with massive success. They allow us to design and model our systems in the abstract, state the system facts, assumptions and expected rules to hold, and finally, they analyze our model for inconsistencies or scenarios we haven't thought of - like code review for system design on steroids. This talk introduces model checkers, covers the motivation behind them, and finishes with a short example.