Testing one execution is a start but isn't enough in a nondeterministic distributed system. If you need to check that an invariant is held across all possible executions (e.g. node 3 is down and node 4 is suddenly faster than node 5), you could brute force that yourself but TLA+ has it built in.
That's exactly it. A test verifies one potential execution path. A TLA+ model verifies every execution path, in every ordering that those events could happen.
One of the tricky parts I found was figuring out what granularity to use when writing specifications.
