As the author mentioned in the original article TLA+, ATPs etc verify the correctness of systems, they don't apply to the type of stability problems which have

As the author mentioned in the original article TLA+, ATPs etc verify the correctness of systems, they don't apply to the type of stability problems which have plagued CockroachDB. That emergent behavior arose from it's implementation, optimizations, etc. Just because a system is unstable doesn't mean it's incorrect (or correct). That is why a simulator is useful. The entire point of building a sim is so you can run the exact code that comprises CockroachDB and control for any situation. For example, an optimization that works great at 10 nodes may be terrible for larger clusters. You need to find that out through testing because most humans can't look at a line of code and infer that. A side benefit of this approach is that if you change some parameter and suddenly experience a big increase or decrease in db throughput you gain a sense for which parameters are most sensitive to the overall system and will then be able to more easily diagnose problems in production.