For the last few months, I’ve on-and-off been working on a new microkernel / RTOS that I’m calling K5. Naturally, your first question will be, why would you make a new RTOS when there are so many good ones already? Just written in Rust alone there is Hubris, TockOS, MnemOS, Embassy, RTIC, and a bunch of other's I haven't listed. K5 has a few unique goals:
- It aims to target microcontrollers, low-power SOCs, and crossover MCUs. Many RTOSs aims to just target one of these groups
- K5 has strict isolation between tasks and the kernel. Many RTOSes targeting microcontrollers share address space between each task and the kernel. K5 requires a strict separation between applications. So bugs in one component will not affect other components
- K5 is a microkernel with a capability system based on seL4. Drivers are fully run in userspace, and all interactions between tasks are mediated through capabilities. This is a key difference over an RTOS like Zeyphr where drivers run in kernel space.
- K5 aims to have the best possible developer experience on a wide variety of processors. Rust developers largely expect their projects to “just build”, and K5 aims to continue that.
- Last but not least, K5 aims to be verified by various formal verification methods. Using mostly safe rust helps a good deal here, but there are all sorts of other things that we can verify. It would be fun to verify the upper bounds of run-time for task-switching.