Quite a few projects are rediscovering the value of state machines. The old projects (eg 80’s) in high-assurance security used state model to design and implement the security kernels. They’d have mathematical model of them as a state machine accepting input (eg interrupts, syscalls), performing computation atomically, and possibly some output. They’d analyze all execution traces for correct functioning, fail-safe under errors, enforcement of security policy, and leak prevention (covert channels). They’d then do an implementation that mapped to it close to 1 to 1 often in a safer language (eg Pascal subset, Ada). Results were that evaluators usually didn’t find shit in terms of implementation problems given basic, code review knocked most of that out. Usually problems were at the spec level and easier to see due to constrained, formal way they were specified.