L4.sec is already formally verified. So the microkernel is already done. You need the user land services to provide POSIX compatibility, and that you can possibly do in Rust.
Looks cool, thanks. They should take the opportunity to fix a few Unix/ACL security problems though, instead of just reproducing the same old POSIX quagmire. Make chroot isolation complete with plan9-like private namespaces, don't implement the traditional broken user/group security model and instead learn from the Polaris virus safe computing prototype (they're already partway there by using the capability secure seL4 kernel).
I would personally also want to eliminate a lot of the duplication in the POSIX API, but that probably won't fly. Can have your cake and eat it too.