The slides present benchmark results of TLA+tools model checker performance, as a number of states processed per second, when model checking a formal model generated by sbuilder. For controlling number of states in a state space refer to Heuristics Used in Creating Runnable Formal Models.
Benchmarks indicate that model checking is CPU bound, and heavily influenced by code volume in the formal model.
For scaling to real world applications the blog entry suggests 1) model checking application in chunks, and 2) distributing model checking tasks to several workers, 2a) using multiple cores in a CPU, or 2b) running on a distributed hardware.
Preparing a blog entry, which gives more details of the results, and an their impact on sbuilder roadmap v2.