Skip to content

Latest commit

 

History

History
80 lines (58 loc) · 3.15 KB

README.md

File metadata and controls

80 lines (58 loc) · 3.15 KB

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:

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

2. Learning more about TLA+