# TLC Model Checker ## Synopsis The model checker for [[TLA+]] bundled in the TLA Toolbox. See also [[TLC Restrictions]]. ### Current Version Differences between the current version and the one used in [[Lamport - Specifying Systems The TLA+ Language and Tools for Hardware and Software Engineers]]: - TLC supports instantiation but does not support parametrized instantiation. See details in [github.com](https://github.com/tlaplus/tlaplus/blob/master/general/docs/current-tools.md). ## Getting Started There are different ways to run TLC: - [[VS Code TLA+#TLC]] - [[TLA Toolbox#TLC]]