Part of the Embarrassing Trainwreck release. Full notes there, main highlights:
As always, critique appreciated, the more vitriolic the better. Thanks for reading!
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.