We are introducing TLA+ and the model checker Apalache. Prior knowledge of TLA+ is not required.

If you want to reproduce the steps, make sure that you have installed the following tools first:

• Apalache version 0.16.5. Check Apalache releases.
• optional: TLA Toolbox or VScode plugin for TLA+

Material for the TLA+ tutorial, co-located with DISC 2021.

Check the specifications in clock-sync and the extended version of the tutorial. Follow the clock sync: step-by-step instructions.

Material for the workshop at HackAtom RU 2021.

Follow the token transfer: step-by-step instructions.

WARNING: The final specification TokenTransfer10.tla is not a complete specification of ICS20. If you want to specify ICS20, you have to introduce the following missing features:

• acknowledgments.

Follow the ERC20: step-by-step instructions

• Apalache model checker
• TLA+ Home Page
• TLA+ Video Course
• Specifying Systems
• TLA+ language manual for engineers
• LearnTla.com
• Community Modules
• TLC model checker
• TLA+ examples