# TLA Toolbox ## Metadata **Status**:: #x **Zettel**:: #zettel/fleeting **Created**:: [[2026-01-15]] **Parent**:: [[TLA+]] ## Installation - From [GitHub Release](https://github.com/tlaplus/tlaplus/releases). - Install the [nightly build](https://nightly.tlapl.us/products/). ## Usage ### TLC Running TLC in Toolbox requires creating the model in the GUI. - Toolbox auto assigns model values for [[TLC Restrictions#Unbound `CHOOSE`|Unbound CHOOSE]] - The parameterized constant operators can be specified directly in the GUI. Example to run TLC in Toolbox using the same example as in [[#VS Code]]: - Add definitions for `Send`, `Reply`, `InitMemInt` directly. - Use normal assignments for `QLen` - Use model value sets for `Proc`, `Addr`, `Val` - Toolbox will handle `NoVal` automatically.