I just took the leap this weekend from designing state machines on paper, mentally reasoning through them, and hoping I got it right, to doing verification on t

I just took the leap this weekend from designing state machines on paper, mentally reasoning through them, and hoping I got it right, to doing verification on them using TLA+. Lamport’s video series is really awesome, and the process really helped me nail down all the edge cases. I did it in a somewhat literate programming style too, and the output PDF is a beautiful spec that should be straightforward to implement in C (it’s for an embedded device that’s going to be installed in remote locations... knowing that the spec of the FSM can’t deadlock is delightful!)