Yup, I'm aware they do a lot of work on this, and hired up half the Haskell and PLT researchers in the world, and have a bunch of projects on it scattered across their web properties.
And maybe some of it is trickling down into parts of Windows or .NET, like F# and others, but I wish they'd develop an entire ecosystem around it and make stronger push to commercialize it.
With all the aforementioned resources MS has at their disposal, by now they should have their own version of SEL4, comprehensive tooling for secure-by-design and correct-by-construction application development, and optionally secure sandboxed containers for backward compatibility with legacy apps. Though ideally MS funds a Manhattan project for rewriting the most popular apps using their SxD and CxC tooling.
Singularity was on the right track, but they let it languish and die for some reason, when instead they could be rebuilding an entire secure/correct ecosystem with Singularity as the focal point, and commercializing it with enterprise support, and selling it to governments and large enterprises with significant security concerns.
I wonder why this hasn't happened yet.
https://en.wikipedia.org/wiki/Secure_by_design
https://us-cert.cisa.gov/bsi/articles/knowledge/sdlc-process...