@Moon Formally verifying an OS is a massive undertaking, that's why (usually) people don't verify the the system as a whole but certain functional properties of parts of the OS. This would make a functional language the best candidate for OS dev, however you lose a lot of versatility with a strict type system and at the end of the day it's more pragmatic to hackjob the OS in some language that implements easy to use concepts for OS dev and afterwards extract the relevant properties required to prove.
People are currently doing that with Linux right now (gl :blobcatgiggle2:) https://arxiv.org/abs/1809.00626