I think the next logical feature would be to have Runway compile a model-checked specification to an actual C++/Java/go/python implementation, using something like Thrift or CapnProto RPC codegen. There has been some work on doing similar spec->implementation compilation from Coq to erlang  but the author hit a lot of obstacles.
 - http://christophermeiklejohn.com/coq/erlang/2013/11/19/verif...
It's not only easy to learn, it's extremely powerful, mostly due to refinements (an advanced concept, better left for week 3 :)), which are absolutely necessary for large systems/algorithms.
There are also two breakthroughs in TLA, which you may come to appreciate: the expression of the program and the program's properties in the same minimal language, and the demonstration that simple, high-school math, plus one or two new concepts, is all it takes to specify and verify programs.
And yeah, code extraction from specification is an open research question, but I don't even consider this to be a top-ten desired feature, considering the amount of time spent specing and verifying vs. translating to the implementation language.
We've also released a tool for testing distributed systems, https://github.com/gundb/panic-server . It integrates with your existing tests (like mocha and others), and even reports/throws bugs back from the remote machines you're testing across.
> including formal specification, model checking, formal and informal
> proofs, simulation, and visualization. I’ve found all of these things
> valuable to learn about, and I think some of them are entirely practical
> to use. However, standard practice in industry is to use none of them.
This is what surprised me most when I started learning about formal specifications. I had been developing distributed systems for years armed with nothing but algorithms, papers, and my own sloppy thinking. I had worked alongside some very smart, senior people who never brought out any kind of formal specification.
It wasn't until I met a researcher developing his own specification method that I heard about such tools.
And I'm super-glad I jumped in.
I'm happy to see more tools entering the space. My feeling is that they are becoming sophisticated enough that we will be able to see people adopting them in the wider industry, even in open-source software. I believe they should be the state of the art. I also think that any distributed system should be published with a formal specification, if not proof, before being accepted into wider adoption by industry.