The other reason I don’t use it is that it’s very hard to inspect what you’re running. You can’t write something like “a trace of X state transition must be possible within N cycles with the right inputs”. It makes it really hard to convince yourself (and your peers) you haven’t assumed all of the state away.
After noodling with with the spec for half an hour or so, I’ll usually have enough insight/confidence to start coding/debugging.
You can, although possibility properties aren't for beginners: https://youtu.be/TP3SY0EUV2A?t=818
But there often are easier ways to do sanity checks to "convince yourself you haven’t assumed all of the state away," usually either by asserting something believed to be false or by intentionally introducing an error in the spec, and letting TLC find a counterexample.
A mistake that could be automatically checked is specifying a system that is equivalent to FALSE (and so implies anything). I hope TLC adds a feature that allows you to check if your system implies FALSE. In the meantime, checking the invariant ¬Init has the same effect.