Positive note from me: one thing I've had good experience with is following the path from a project that does something similar to what I want; extract a tech-neutral prose spec from the source; convert that prose spec into a formal spec; use that spec to generate valid traces, a language-specific interface layer, and conformance checks to test whether an implementation of the interface generates good traces. Once you've got that, implementing the system is a matter of colouring the interface in by numbers, which is really easy for a model.

The bonus here is that you can cut in at the prose spec stage and change it to whatever you need, as well as being able to target it at specific technical choices at the last couple of steps.

Where I've seen this work really well is with privilege escalation management, where you do actually want to be careful about the states the system can get into, and the APIs available for managing privileges in a system might be super specific to that system. But I can imagine the workflow being quite a useful one any time you've got anything state-machine flavoured.