You can already use Rust on seL4, today! It's not ready for public consumption yet since there are no docs, but I've been working on it a lot recently and hope

You can already use Rust on seL4, today! It's not ready for public consumption yet since there are no docs, but I've been working on it a lot recently and hope to have a release of the foundational libraries sometime in the next two weeks. There's a mailing list, if you want to watch: https://lists.robigalia.org/listinfo/robigalia-dev https://lists.robigalia.org/listinfo/robigalia-dev And the (still in-progress) source code: http://gitlab.com/robigalia/sel4-sys http://gitlab.com/robigalia/sel4-sys. I have some ideas about encoding RPC protocols as DFAs in Rust's type system, and then doing verification of the protocols in a more abstract setting (perhaps NuSMV or a similar checker). This is somewhat similar to the (ancient at this point) "protocol compiler" that used to be in Rust, doing a similar thing for channels. I'm interning at Data61 (née NICTA) on the verification team starting Jan 18, and I'm hoping to transfer some of that experience and knowledge into verifying Rust.