It’s being worked on, but I can see it as an absolutely huge undertaking
Indeed it is, though if they're using C (or C++) they're making an inherently arduous task even more difficult for themselves.
Ada/SPARK would probably be ideal, as Ada lends itself to these sorts of analyses fairly well and it has good low-level facilities.
A functional language would be excellent for implementing a large portion of the OS w/ verifiable properties, but there are efficiency issues (as well as that they're rather unsuited to low-level manipulations).
IMO we need the fundamental/base portions of our SW to be formally verified: OS, Compiler, the basics of the networking components (like DNS). If that's done the stability/reliability/security of everyday consumer-level software should be immensely improved.