The next release of the TLA+ Toolbox will allow TLC to run in distributed mode. You will be able to execute a TLC run in parallel on dozens or hundreds of computers, potentially speeding up model checking by one or two orders of magnitude. However, this will require automating the process of starting the workers, and we don't know how to do that on all the different operating systems and networks that people use. The purpose of this forum is for users to share their experiences of running TLC in distributed mode, so we can all learn what works on what kinds of systems.
