The last time I looked at this (when having to deal with spaghetti-like execution flows through an Actor-based code base), I really liked the ideas of model che

The last time I looked at this (when having to deal with spaghetti-like execution flows through an Actor-based code base), I really liked the ideas of model checking with Colored Petri Nets and code generation (http://cpntools.org/ http://cpntools.org/), and the TLA+ language.