As someone who started learning TLA+ in the new year, I'd also add: * The class of bugs it excels at finding which humans can't just aren't that important for

As someone who started learning TLA+ in the new year, I'd also add: * The class of bugs it excels at finding which humans can't just aren't that important for most cases! I'm learning it by modeling one of our systems which I know has a race condition that sometimes results in a request being dropped, with the goal of having TLA+ prove it. But if I actually filed this as a bug - three in every ~billion requests get dropped in a process that's already at best reporting 99.9% accurate anyway - it would go straight to the bottom of the backlog. Inconsistent CSS styling of our swagger probably costs us more than this.