If not already extant, a FOSS, capabilities-secure, formally-verified RTOS somewhere in the space of seL4 and MINIX 3 microkernel would be useful. Rust might help, but the problem is a lack of attention paid to formal verification all the way downstream, perhaps including symbolic execution and thorough verification of the resulting binaries.
In general, the biggest microkernel design challenges are efficient IPC and handling complex transactions across multiple tasks/processes.
seL4 and such solved IPC performance bottlenecks by proving their moves of message structures were sound under invariants. This is something Rust might be able to solve through moves and lifetimes, but it might not have enough power directly and some edge-cases of unsafe code might be needed for performance reasons.
When it comes to handling privileged events, transactions touching multiple each tasks components must be carefully locked or some privileged helper must step in that violates ordinary constraints. In largely-monolithic Linux, this is relatively easy because when lock-free patterns are unavailable, some or all of the world can be stopped and essentially anything can happen almost anywhere. This simplicity comes at a cost of low/no amounts of isolation that weakens the design goals of a "pure" microkernel architecture which leads to real, hybrid microkernels.