[renox]

I'll have a look thanks but note that seL4 is implemented in C because C has a formally verified compiler CompCert which Rust doesn't have..

[steveklabnik]

... not to mention that seL4 was started in 2006, a full four years before Rust was even conceived of. The proof was finished a year before.