TLA+ is really good at finding problematic traces involving concurrent agents, so it naturally shines in distributed systems. For something that relies on find

TLA+ is really good at finding problematic traces involving concurrent agents, so it naturally shines in distributed systems. For something that relies on finding problematic inputs (like for compilers), SMT solvers like Z3 are a more natural fit