# TLA+ ## Metadata **Status**:: #x **Zettel**:: #zettel/fleeting **Created**:: [[2026-01-10]] ## Synopsis ### Checkers - [[TLC Model Checker]] - [[Apalache]] ## Notes - [[TLA+ Symbols]] - [[TLA+ Fold Pattern]] - [[Create Sample Traces from TLA+]] - [[Learn TLA+ from PlusCal]] ## References ### Books - [[Lamport - Specifying Systems The TLA+ Language and Tools for Hardware and Software Engineers]] ### Modules - Standard Modules - [Java Implementation](https://github.com/tlaplus/tlaplus/tree/master/tlatools/org.lamport.tlatools/src/tlc2/module) - [TLA+ Stubs](https://github.com/tlaplus/tlaplus/tree/master/toolbox/org.lamport.tla.toolbox.uitest/farsite) - [[TLA+ Community Modules|Community Modules]] - [PT](https://github.com/Apress/practical-tla-plus/blob/master/PT/PT.tla) from the book [[Hillel Wayne - Practical TLA+ (Highlights)|Practical TLA+]]. ### Examples - [tlaplus/Examples](https://github.com/tlaplus/Examples) ### Others - [VS Code TLA+ Knowledge Base](https://github.com/tlaplus/vscode-tlaplus/tree/master/resources/knowledgebase) ## Highlights - [[Hillel Wayne - Learn TLA+]]