Skip to content

Material for a workshop on Apalache and TLA+. To be populated with more examples.

License

Notifications You must be signed in to change notification settings

informalsystems/tla-apalache-workshop

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

71 Commits
 
 
 
 
 
 
 
 

Repository files navigation

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+

About

Material for a workshop on Apalache and TLA+. To be populated with more examples.

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Contributors 4

  •  
  •  
  •  
  •