Isn't this what the Microsoft Singularity project have been working on for a long while? I remember reading some post about how they also have proven (verified)

Isn't this what the Microsoft Singularity project have been working on for a long while? I remember reading some post about how they also have proven (verified) the correctness of its operation a while ago, but I can't immediately find a link.