Recently I revisited my previous interest in seL4 - a fast, highly assured operating system microkernel for building secure systems.

The seL4 Microkit tutorial uses a simple Wordle game example to teach the basics of seL4 Microkit (formerly known as the seL4 Core Platform), which is a framework for creating static embedded systems on top of the seL4 microkernel. Microkit is also at the core of LionsOS, a new project to make seL4 accessible to a wider audience.

The tutorial is easy to follow, needing few prerequisites beyond a QEMU emulator and an AArch64 cross-compiler toolchain (Microkit being limited to 64-bit ARM systems currently). Use of an emulator makes for a quick test-debug cycle with a couple of Makefile targets, so time is spent focusing on walking through the Microkit concepts rather than on tooling issues.

This is an unusually good learning experience, probably because of the academic origins of the project itself. The Di├ítaxis documentation framework would class this as truly a “tutorial” rather than a “how-to guide” - you do learn a lot by implementing the exercises.