I've met people who worked on Midori and they describe it as the best project they've ever worked on. Used to work in a building with a bunch of old Midori-folks and would ask them about it anytime I heard the word 'Midori'. I don't think it was MSR though.
Personally, I've always been most impressed by the research into formal verification: Z3, Dafny, TLA+, F*, Lean, and many more.
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.
Personally, I've always been most impressed by the research into formal verification: Z3, Dafny, TLA+, F*, Lean, and many more.