The Toolbox uses the TLC model checker to model check the current spec. More precisely, TLC checks a model of the specification. The Models help page explains what a model is and how to manage models. The Creating a Model page explains how to create a model. The Checking a Model page explains how to run TLC and what to do when it reports an error.
TLC can make use of multiple processors, getting speedups that are almost linear in the number of processors. It can use multiple processors (cores) in a single computer, and multiple networked computers. See the How to run section of the Model Overview Page and Running TLC in Distributed Mode.