Thinking about protocols with TLA+ and Apalache

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

1. Step-by-step instructions

1.1. Setup

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+

1.2. Incremental specification of clock synchronization

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.

1.3. Incremental specification of token transfer

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.

1.4 Specification of ERC20 tokens including the Approve-TransferFrom attack

Follow the ERC20: step-by-step instructions

2. Learning more about TLA+

• 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