[nickpsecurity]

High-assurance security from 80's-90's used them too in both formal specifications and coding approach. It was more like looking at the kernel as a giant, state machine but you can do protocols or app components, too. Many will complain about unreadability of C code. However, a proper spec or DSL for state machines makes them extremely readable with the C code autogenerated. They're also extremely easy to formally verify as you pointed out.

On page 15, you can see Rockwell-Collins combining model-driven development with Z, SPARK, and state-machines. It's a nice example of power of interacting, state machine approach combined with some other elements.

https://www.nsa.gov/resources/everyone/digital-media-center/...

[nitrogen]

If each state is a function that simply waits for events and returns the next state, the C code doesn't look that bad.

[nickpsecurity]

It doesn't look bad versus regular C. You still have the C-specific risks in the module and at module interfaces that other language reduce. It's also harder to parse, analyze, and compile in a secure way. With SPARK & formal tools, one can get a strong analysis that the code will always meet the spec. The ability to fully do that for C has only come online in the past few years. It appears to take more work, too.