I’m confused. Wasn’t the error actually in an unverified subsystem and isomorphic to an error caught by the model checker in a verified subsystem? Isn’t this more of a cautionary tale for someone not relying on formal verification?
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..