The TLA-Plus Quick-Standard Project

The quick-stroke project sprung out of the property-based testing interest of mine. I was really interested and inspired by this temporal logic approach of specification, basically. And I saw some connection to the state machine testing that we discussed before. It's getting the specification right, it's as hard as getting the code right almost, right? Yeah. You have to fiddle with generators and stuff to trigger these edge cases, but not too often because it's unproductive. Exactly. Still, I haven't used TLA-plus for anything real. But I had this interest in temporal logic. So I've messed around with alloy a bit. We used it for some interesting problem, which