I am a big fan of property based testing that can fuzz through very similar types of problems but it's not quite the same.
Or is tla+ just the thing to use and it's worth ploughing through?
I hated the syntax at first, and frankly, it took two weeks and about 500 pages of reading before it clicked (as to how to solve practical problems with it).
It's been a pleasure to use ever since. What is does you can't get from any other tool or methodology (with the same amount of effort).
> Are there good alternatives for solving the same / similar kinds of problems?
Not that I've found. It's really worth it to just learn TLA+.
There are quite a few alternatives. Alloy is pretty approachable and aims for the same or a similar space. I liked Event-B (based on B-Method), its tooling was nice. Z Notation (pronounced Zed) was my first examination of formal specifications, it lacked a lot of tooling for automation but I found it helped to clarify my reasoning about systems quite a bit. I wish I'd used it more, it's now a fuzzy memory for me.
That said, I like TLA+ specifically for what it's aimed at, modeling concurrent and distributed systems. It's very effective for this if you can take the time to understand it.
Most people who use TLA+ also seem to fire up Alloy once and awhile…