Statechart diagrams are even better than sequence diagrams, because they can encode quite a lot of behaviour visually.
And indeed they good for specifying, being the source of truth, but like code, they (afaik) don't really work for representing interactions with multiple actors (other than by sending/receiving messages), and they don't have a time component. But you could generate sequence diagrams from them, or at least verify them.
Xstate does have some functionality for interacting with the specified state machine, but I haven't played with it a lot. The idea of generating—or at least verifying—Xstate state machines with TLA+ has come across my mind, though.
Timed behaviour, like timeouts can be represented in statecharts by having transitions on time based conditions. For example an event puts the system in a 'waiting' state, and in the waiting state there is a 30 second transition to a 'fail' state unless some other event happens which pulls the system out of the 'waiting' state.
Also it provides a good indication of what behaviour is valid and what not valid and what are don't cares.
External interactions of a system can be model as the state changes of a system.
They also have 'memory', special elements that remember which substate the system was in before it jumped out of the state last time.
I recommend David Harel's very interesting paper on modelling behaviour with state charts.