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