I haven't looked into 'formal' verification methods for FSMs, so I did some light googling. I found this guy [0] which gives an overview of potential methods.

I'll have to think about testing methods more. There are a few things I would want to know about a single FSM: does it exit (various exit states, either error final state or valid final state), are there unreachable states, does it loop in places it shouldn't, does it enter states it shouldn't for a given stimuli (Events + Guards are the params for this test). I think there's also a place for event fuzzing to try and break the machine.

[0] https://www.linkedin.com/pulse/verification-testing-fsms-too...