I think TLA+ is a great fit for what you want to do. What problems are you facing?
BTW, while state machines are certainly the recommended approach for TLA+ specifications (and for very good reasons), there are others, which may be useful in some cases. For example, here I have a rule-based specification of Tic-Tac-Toe: https://pron.github.io/files/TicTacToe.pdf Instead of describing a state machine, the specification is a conjunction of state machines in a style known as "behavioral programming".
Also, you may benefit from looking at the TLA+ subreddit (https://old.reddit.com/r/tlaplus/) for various posts on TLA+ and formal methods in general, and maybe get some ideas.
BTW, while state machines are certainly the recommended approach for TLA+ specifications (and for very good reasons), there are others, which may be useful in some cases. For example, here I have a rule-based specification of Tic-Tac-Toe: https://pron.github.io/files/TicTacToe.pdf Instead of describing a state machine, the specification is a conjunction of state machines in a style known as "behavioral programming".
Also, you may benefit from looking at the TLA+ subreddit (https://old.reddit.com/r/tlaplus/) for various posts on TLA+ and formal methods in general, and maybe get some ideas.