TLA+ is not so different from real-world programming languages: wewrite (abstract) programs, then we compile/typecheck them, we runthem, we debug them. The workflow for TLA+ should be similar to, say,Haskell. GHC has a compiler, a REPL, and a few command-line tools. Itdoes not have an isolated IDE; nor does it need one. Even tools likeCoq or Isabelle, which have their own little IDEs for interactiveproof assistants, are usually used via other generic IDEs likeEmacs.