As a contribution to further increasing the accessibility of TLA+, I've created a VSCode Dev Container environment supporting it. I believe it's the shortest publicly available route as of this writing to a fully working environment, with TLA+, LaTex formatting, graphviz visualization of state machines, etc. Just go here and follow the instructions. It's 10-15 minutes to a working environment, and you can then go through the TLA+ tutorial using the environment for a nice introduction to TLA+ (albeit with sadly low resolution video) and a guided tour of how to use this environment. After the quietest of roll-outs, it's six forks and six stars. Hope you'll agree! https://github.com/kevinsullivan/TLAPlusDocker