Hi.
I had a brief look at Runway when it was announced. I liked the visualizer a lot, but the language seemed clunky by comparison to TLA+. For example, non-determinism is a core component in allowing specification at different abstraction levels in TLA+. In Runway, from what little I gathered, nondeterminism is rather implicit, and I believe restricted to interleaving execution and to random numbers (and the distinction between randomness and nondeterminism is not quite made clear in Runway). My first impression was that Runway would be hard to scale to larger specifications. Also, I think it doesn't currently have a model checker, only a simulator; a model checker is a planned feature, but that could have changed by now.
As to a REPL, that is very useful. I find myself using the TLC evaluator as a REPL, but a more ergonomic one may be better.
The visualizer also seems very useful. I believe TLA+ can also be visualized via automatic translation to ProB, which I think has a visualizer, but I haven't tried that.
Ron