Yeah, their verification tools are incredible. They applied VCC to Hyper-V. The driver tools mostly wiped out blue screens. Got a new one called P language used in USB stack. The methods you mentioned like Dafny got applied in ExpressOS by another team:
Microsoft did it first in VerveOS although Nucleus was ripped off a mainframe OS from the 1970's. VerveOS was impressive where it was one of first safe to the assembly with much less effort than other projects. They also did CoqASM for verified assembly.
http://joeduffyblog.com/2015/11/03/blogging-about-midori/
Yeah, their verification tools are incredible. They applied VCC to Hyper-V. The driver tools mostly wiped out blue screens. Got a new one called P language used in USB stack. The methods you mentioned like Dafny got applied in ExpressOS by another team:
https://github.com/ExpressOS/expressos
Microsoft did it first in VerveOS although Nucleus was ripped off a mainframe OS from the 1970's. VerveOS was impressive where it was one of first safe to the assembly with much less effort than other projects. They also did CoqASM for verified assembly.
https://www.microsoft.com/en-us/research/publication/safe-to...
https://www.microsoft.com/en-us/research/publication/coq-wor...