Bleeding-edge was VerveOS: https://www.microsoft.com/en-us/research/publication/safe-to-the-last-instruction-automated-verification-of-a-type-safe-operating-sy

Bleeding-edge was VerveOS: https://www.microsoft.com/en-us/research/publication/safe-to-the-last-instruction-automated-verification-of-a-type-safe-operating-system/ https://www.microsoft.com/en-us/research/publication/safe-to... It's legacy will be in their IronClad Apps. Look into those if you want to see how far they've gone. Also, Microsoft Research & HLL vs Nix and C in security are a gap that's ever widening. ;)