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