This feels like the kind of bug you could really only catch in advance with a model checker. And, even then, you'd have to model things at the right granularity to actually catch it.