[constantcrying]

Completely agree, but obviously you relied on the state machine being sufficiently separate and having a formal specification for it.

State machines are quite common, in aerospace software, where the requirements even specify the states and transitions. If you can formally verify them, I believe, you absolutely should, as often there can be a lot of subtlety going on there, especially if you have a distributed system of state machines sending messages to one another.