[ausimian]

I've used TLA+ professionally in a previous role and found it useful. I'd agree with the sentiments in the GG discussion:

1. A repl would be useful.

2. Better documentation for the individual tools, allowing other editors and toolchains to hook them more easily.

I would say that I found the TLC model checker extremely valuable, but learning what subset of TLA+ it can actually handle (and structuring your specifications appropriately) takes time.

Not sure about enums - seems like something PlusCal would do (if it doesn't already), but I would leave TLA+ alone, I think its support for sets is sufficient.