I've tried it a few times. I wanted to use it a couple days ago to help me understand how a bad state could be reached in a program I was debugging, but found

I've tried it a few times. I wanted to use it a couple days ago to help me understand how a bad state could be reached in a program I was debugging, but found out the tla toolbox no longer starts because it depends on something that's changed in the current java environment (anyone remember write once run anywhere? it was always a lie). I don't have the patience to fight more tools than I absolutely have to. I guess that's my biggest obstacle to using TLA+. I would likely use it if I could just install it from my distro's package manager and have a single clean binary that can be invoked from the command line like a compiler, passing it the path to my model. I find the java gui ux to be repulsive.