TLC is an explicit-state model checker for verifying safety and liveness properties of finite instances of TLA+ specifications. The tutorial will give a brief overview on TLC in general and then focus on recent extensions that support running TLC on a cluster of distributed computing nodes.