This has been done multiple times in research, see Verve OS from Microsoft, even Assembly is verified, that is where Dafny came from.

https://en.wikipedia.org/wiki/Verve_(operating_system)

However, worse is better on the market, and quality doesn't pay off, hence why such ideas take decades into mainstream.