Now with the push for memory safe, high-integrity applications, I am looking for a separation kernel or formally verified OS to base my automation software upon. Rust was a contender a few years ago, but with no formal specification standard yet like C++/C, and having a steep learning curve, I decided on SPARK2014/Ada due to the simpler language and formal verification tooling as well as decades of high-integrity software in production. Has anyone worked with either Muen or Ironclad/Gloire? I'd prefer a microkernel vs. monolithic kernel, and I have started looking at Minix3 as a base due to that and its compatibility with a ton of NetBSD packages and great documentation in the form of a textbook. I think choosing Rust for such projects is high-risk given it is not even close to SPARK2014/Ada in this arena.
https://muen.codelabs.ch/
https://github.com/Ironclad-Project/Gloire