This discussion reminds me of the Alloy[1] language and the associated analyzer. The analyzer transforms an Alloy model and some formal statement about it (e.g

This discussion reminds me of the Alloy[1] language and the associated analyzer. The analyzer transforms an Alloy model and some formal statement about it (e.g. "a caller can never connect to callee without the callee's consent to that caller connecting") into a giant SAT problem, which it feeds to a SAT solver looking for counterexamples, which it can map back to a series of valid state transitions in the original model. Very cool stuff, at least 20 years ago when I was playing with it. [1] http://alloytools.org/about.html http://alloytools.org/about.html