I think it's mostly just sticker shock. Downloading another thing, and it's a bit spoiling these days when most toolsets have some amount of cross-editor suppor

I think it's mostly just sticker shock. Downloading another thing, and it's a bit spoiling these days when most toolsets have some amount of cross-editor support. You can do similar things in various language modes in VS Code, after all (plotting/fancy rendering/cloud APIs). 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.