You make it seem like the formal verification missed an issue. Not quite what happened: "The first effort consisted of analyzing part of the RA autonomous spac

You make it seem like the formal verification missed an issue. Not quite what happened: "The first effort consisted of analyzing part of the RA autonomous space craft software using the SPIN model checker. One of the errors found with SPIN, a missing critical section around a conditional wait statement, was in fact reintroduced in a different subsystem that was not verified in this first pre-flight effort. This error caused a real deadlock in the RA during flight in space." The model actually found an issue that was later reintroduced in a different part of the system that was not formally verified. If anything, it tells us we need _more_ formal verification!