This is awesome very good combination. seL4 is formally verified and then slap a memory safe and performant user-level code on top.

More info about L4 micro-kernel:

https://sel4.systems/Info/FAQ/

Now user-level here means drivers as well. So that would be interesting how it would work with Rust. Will it all default to unsafe code and just end up with pointer twiddling and memory overwrites and all the same errors. I hope not.

Currently it seems that the verification mode had DMA turned off and for SMP they run a kernel instance on each core and then send messages to each other via shared memory. That probably means not load balancing or not scheduling?