1. 15

Part of the Embarrassing Trainwreck release. Full notes there, main highlights:

  • “Concurrency” section is slightly better
  • “Temporal Properties” section is slightly better
  • New “Techniques” section for how to write better specs.

As always, critique appreciated, the more vitriolic the better. Thanks for reading!

  1.  

  2. 2

    Although used up time on another thread, I’ll add at a quick glance that I like seeing addition of conditionals and infinite loops. In formal verification, a lot of things involve guarded conditionals or loop invariants. Good to have that represented in TLA+ guide.