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+.
Yup, I agree strongly. I watched the Lamport videos when on paternity leave, and really enjoyed it. The main benefit for me was that writing a spec in TLA+ allows me to "get my mind right" before writing programs. I was in love with the notation from the beginning (but I was a math major in school so I'm biased).
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.
Coyote (concurrency exploration tool for .NET programs) can be used to do something "similar". My team often writes tests which set up focused concurrency between different APIs, the tests use Coyote to explore different ways that concurrency can unfold and write a strong set of assertions and invariants that must be true at the end. It's not TLA+ but it's still quite effective, very teachable as developers are already familiar with writing C# tests and helps catch safety and liveness bugs in our actual code base (as opposed to a model of it). It's not the same, by design, and does a decent job at finding concurrency and distributed system bugs.
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?