> It's worth noting that many fuzzers go to great lengths to produce examples that are as small as possible, but it's true that this just comes naturally with TLC.

While this is true for invariants, unfortunately it's not true for liveness properties. The currently implementation doesn't make any guarantees about the length of a minimum liveness counterexample, and in practice I find it's usually the _longest_ counterexample.

Still super useful, I'm just being a little pedantic here :)