TLA+ Tiramisu

Hillel Wayne

There’s a gap between knowing how to write specifications and knowing how to write them well. Much of this gap is from the “small stuff”: all of the little tips, tricks, and traps that experts implicitly know but beginners rarely learn. Things like “the best way to represent nested state” or “how to debug a slow model.” This talk will be a general introduction to intermediate-level techniques. Topics will include:

  • Action best practices
  • Complex liveness properties
  • Using action-level fairness
  • Auxiliary variables
  • TLC configuration and model performance
  • Community modules

Most topics will be applicable to both TLA+ and PlusCal, but some language-specific techniques will also be covered. Advanced specification topics such as partial specifications may be discussed if time permits.