Do you have experience with it? How hard is it to use TLA+ to solve every-day problems? Are there any other model checkers that worth looking at? Or TLA+ is the

Do you have experience with it? How hard is it to use TLA+ to solve every-day problems? Are there any other model checkers that worth looking at? Or TLA+ is the most sutable for concurrency problems?