But this is nothing more than a variation on the Two Generals Problem for distributed systems.

Given an FSM and a set of messages, and a model of timing, it may be possible to fully test out the most interesting subset of transactions and test out many of the pathological cases. But instrumentation in anticipation of finding unanticipated pathological cases is pretty important.

This is bounded by cost, just as all due diligence processes are. Well-designed instrumentation is the key.

FSMs are not the problem here - with infinite bandwidth channels and perfect transmission, you wouldn't even need all that.