> You can’t write something like “a trace of X state transition must be possible within N cycles with the right inputs”.

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.