I don't think possibility properties are directly expressible in any linear-time logic, just branching-time logics, and those have their own issues, even though

I don't think possibility properties are directly expressible in any linear-time logic, just branching-time logics, and those have their own issues, even though I think they're still sometimes used. 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.