Extrapolating the effort involved in proving huge numbers of complex safety properties for an operating system written in C to programs in general is a bit silly. Doing formal verification in more abstract languages gets considerably easier, and considerably easier to mechanise large chunks of the work (a Hindley-Milner type system is a kind of proof of a safety property, for example, and that's totally mechanical).

So it might take 200,000 years to verify Windows, but considerably less to verify an equivalent amount of non-operating system Haskell code, for example.