> A challenge in high-reliability software is that the systems they are running on top of have few reliable properties.

I don't dispute this, and is infact related directly to my point, it seems that people are reading my comment as formal verification is a Panacea, I was only trying to point out that are primitives and abstractions provided by operating systems as well as programming languages are one major area that stops one from writing a formal spec.

Real formal verification is very very hard.

You do seem to miss the point that I am saying many of these subtle inconsistencies can be still complex but encoded into a formal model and I was showing how the file system abstraction adds it's own complexities.

Operating systems probably would be one thing that could be a massive project to undertake but would be worth it. We already have a formally verified micro kernel sel4 that proves lots of useful features and as you point out hardware issues an important thing at this level of correctness and sel4 simply assumes certain models for this.

> Operating systems probably would be one thing that could be a massive project to undertake but would be worth it

I don't think so. Even if you take small embedded project, there's a lot of unreliability that could creep in. You're not really sure what you got from a sensor is good or noise. Which is why you got all those error checking and ack in the protocols. You can make assumptions and try to verify your own code, but that's only if it brings enough benefits (mostly give you a clear sense of how likely something could go wrong). And that holds only for one version of the software.

You can do reliability study on hardware because it stays mostly in one configuration. But all bets are off if you're constantly modifying stuff inside.

Regarding formally verified OSes, IIRC an early version of CICS (what we would call application server today) has been formally verified in the 1980s.