https://spinroot.com/spin/Doc/rax.pdf
TL;DR: in the 1990s NASA flew an autonomous control system that was formally verified, tested out the wazoo, but which nonetheless failed in flight.
[UPDATE] I did not mean to imply that the formal verification failed. It did not. The formal verification worked as advertised. The cause of the failure was much more subtle and nuanced.
"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!
Sorry, that was not my intent. I added a clarification.
> Sorry, that was not my intent. I added a clarification.
I'm sorry but it didn't. Without reading next comment I wouldn't know why it failed.
No, it was quite a bit more subtle than that. The problem was that there was no mechanism to enforce the use of the formally verified API, and an application programmer put in a direct call to a system function that bypassed that API.
Source: I was the technical lead on the RAX executive.
I'm still a bit confused about the point though. I feel like an adequate rejoinder would be to enforce formal methods at all the levels? I'm obviously not talking specifics (because I don't know them! ... and you do), but this seems like a failure of process or lack of enforcement of formal methods "all the way down" as it were. I dunno, color me confused...
So sometimes you can build a 'self contained' unsafe part made safe with the right API but not always, which is already a significant improvement over other languages which are unsafe all the time..
Formal methods are super cool, and formal verification is even cool, but it can be really easy to think it's always perfect. It gives you such amazing guardrails most of the time that it can be easy to stop looking for when there aren't any.
For example, model checking is cool and useful, but sort of by definition it is exhaustive and as a result you end up having to restrict scope in a lot of cases (For example, redefining the INTEGERS set to {-1000...1000} in TLA+). This is almost always perfectly fine and can catch a lot of weird cases, but it's easy to forget that "nearly everything" is not the same thing as "everything".
Obviously I still think formal methods are worth it, but they're not a substitute for being careful.
Yes. Exactly this. I hereby dub this Tombert's law. :-)