My only time using TLA+ "in anger" was on an embedded system. There was a problem in the hardware portion and our boss wanted proof it was the hardware and not

My only time using TLA+ "in anger" was on an embedded system. There was a problem in the hardware portion and our boss wanted proof it was the hardware and not our software. He didn't accept any of our evidence that it was a hardware flaw, partially because our tests weren't failing 100% of the time. I used TLA+ and ended up with a handful of traces which we were able to recreate with the hardware and some small programs (remove everything our system actually did, just use the busted data bus) to demonstrate the failure, they always failed instead of failing only 90% of the time (shouldn't have been needed, it was obvious the hardware was broken). The TLA+ model started off being a reasonable fidelity model of the specified hardware bus, and then I started messing with it (in a deliberate fashion, altering state transitions) until I got traces and invariant violations similar to the real-world hardware. I've used Alloy for similar things, but only after the fact not during the investigation and as a way to learn Alloy. I'd use them both again (TLA+ especially) if I could convince people it was worth the time, but it can be difficult to get the time to spend on it at work while also meeting other work obligations. I've used TLA+ for some personal projects involving concurrent and distributed systems (toys, nothing notable just playing). I used TLA+ to demonstrate that my design worked as I intended, and then started writing code based on the model.