Monitoring and Verification of Multitenant Kubernetes Clusters using TLA+ Trace Checking

Ioana Silaş, Adrian Crăciun

In distributed systems, model checking is usually used at design time for specifying an abstract model of the system and then exhaustively checking all possible behaviors. TLA+ is…