Library Operating Systems (libOS) are highly efficient because the entire software stack, from the kernel to the application, is compiled, optimized, and linked together. However, in certain scenarios, such as code injection for network packet analysis or adding custom drivers, it is necessary to extend the kernel as needed. The traditional approach of modifying and recompiling the kernel source code can be time-consuming and error-prone.

The memory-safe systems programming language Rust is gaining more and more attention in the operating system development communities, as it provides memory safety without sacrificing performance or control. However, these safety guarantees only apply to the safe subset of Rust, while bare-metal programming requires some parts of the program to be written in unsafe Rust. Writing abstractions for these parts of the software that are sound, meaning that they guarantee the absence of undefined behavior and thus uphold the invariants of safe Rust, can be challenging. Producing sound code, however, is essential to avoid breakage when the code is used in new ways or the compiler behavior changes.