- It shows you the ASCII and pretty printed spec side-by-side.
- It plots TLC data as it runs and presents live coverage data in a nice way. Soon it will also show TLC performance profiles as color maps. (https://twitter.com/lemmster/status/1082787089140183040)
- It makes running TLC in the cloud (single-node or distributed) very easy. (https://tla.msr-inria.inria.fr/tlatoolbox/doc/cloudtlc/)
- I don't know of any other way of using TLAPS. (https://tla.msr-inria.inria.fr/tlaps/content/Documentation/T...)
Then again, I'm really not a fan of either vim or emacs, despite having used the latter as my main editor for some years. I think this may be because I value tools that present more information in a convenient way that allows me to inspect and analyze my text over tools that allow editing more quickly (when I write code, I spend 80% of my time in Sourcetrail and only use the editor to punch-in characters), but I don't know.
There don't seem to be many developers working on TLA+ outside of Microsoft Research though, so I think their work is probably better spent elsewhere than just recreating the Toolbox in other editors. It's not that bad. Maybe in a year or two if TLA+ continues growing in popularity someone will help hash out an alternative.
In a prior project one of our developers checked their models in the Toolbox originally and then we just ran them in CI from the command line, which also worked fine and made it easier if people wanted to run/edit them "by hand" in vim or something.
I'd love to see a TLA+ package for vscode [1]. It seems there is more and more TLA+ adoption, it is surprising there aren't better environments to use it. The TLA Toolbox is awful (well, to be fair to the people that developed it, it does the job and maybe it's ok for some category of users).
EDIT: [1] there's one actually, https://github.com/TeamTilapia/vscode-tilapia