# nix-sel4: build Microkit systems from Nix, with a clone-and-boot example **URL:** \ **Category:** New to seL4\ **Created:** [October 13, 2026, 12:32am UTC](https://sel4.discourse.group/t/nix-sel4-build-microkit-systems-from-nix-with-a-clone-and-boot-example/1087 "2026-10-13T00:32:50Z")\ **Posts on this page:** 2\ **Page:** 1
**Author:** ![conao3](https://yyz2.discourse-cdn.com/free1/user_avatar/sel4.discourse.group/conao3/32/431_2.png) [@conao3](https://sel4.discourse.group/u/conao3)\ **Post date:** [October 13, 2026, 12:32am UTC](https://sel4.discourse.group/t/nix-sel4-build-microkit-systems-from-nix-with-a-clone-and-boot-example/1087/1 "2026-10-13T00:32:50Z")
I got tired of the setup dance every time I wanted to try something on Microkit, so I packaged it. One command gets you a booting seL4 system: ```auto nix run github:conao3/nix-sel4 ``` ```auto LDR|INFO: loader for seL4 starting ... Booting all finished, dropped to user space MON|INFO: Microkit Monitor started! hello, world from nix-sel4 ``` No SDK tarball to download, no `aarch64-none-elf` toolchain to install, no `MICROKIT_SDK` to point anywhere, no seL4 hardware. QEMU emulates the target, so any x86\_64-linux or aarch64-linux box with Nix works. There’s a separate repo you can clone as a starting point for your own system: [GitHub - conao3/nix-sel4-example: A clone-and-boot seL4 Microkit system built with nix-sel4 · GitHub](https://github.com/conao3/nix-sel4-example) ### What it gives you Three functions, on top of the SDK: - `buildProtectionDomain` cross-compiles a PD against the SDK for a given board and config. It picks the toolchain from the board’s architecture, so you don’t repeat the `libmicrokit.a` and linker script paths. - `buildSystem` runs the `microkit` tool and returns the image, the report, and a QEMU runner for the boards that can boot under QEMU. - `mkSystemDescription` renders the system description from a Nix attribute set instead of XML. That last one is the part I actually wanted. Writing the description in Nix means some mistakes fail at evaluation instead of at boot: - channel and IRQ identifiers get allocated per PD out of the same identifier space, and refuse to go past 62 - a `map` naming a memory region that doesn’t exist is rejected - two mappings that overlap inside one PD are rejected, with both regions named - a `program_image` with no matching ELF, or an ELF nothing refers to, is rejected Hand-written `.system` files still work, so you can adopt it gradually. ### What’s tested `nix flake check` boots the examples under QEMU and greps the console. Hello world runs on all 3 QEMU boards (`qemu_virt_aarch64`, `qemu_virt_aarch64_el1`, `qemu_virt_riscv64`). A second example puts 2 PDs on a shared page plus a channel, with the channel id and the mapping address patched in through `setvar_id` and `setvar_vaddr`, so nothing is hardcoded on the C side. All 28 boards in the SDK are in the board table with their architecture and available configs. The other 25 build an image you flash yourself. ### The development shell `nix develop github:conao3/nix-sel4` exports `MICROKIT_SDK` and puts `microkit`, the cross toolchains, `make` and QEMU on `PATH`. The examples shipped inside the SDK build there with their own Makefiles, unmodified. If you just want the tutorial to work and don’t care about the Nix library, that’s probably the useful part. ### Relation to seL4-nix-utils @wucke13 and the DLR-FT folks already cover a lot of ground with [https://github.com/DLR-FT/seL4-nix-utils:](https://github.com/DLR-FT/seL4-nix-utils:) the kernel, sel4test on simulated and physical targets, CAmkES, U-Boot, and a Microkit SDK built from source with a `microkit` dev shell. If you want the SDK compiled rather than downloaded, or you’re working outside Microkit, go there first. Mine is narrower and starts where that shell ends. I take the official pre-built SDK tarball, which keeps the closure small and the build fast, and spend the effort on the layer above it. Both `buildSystem` and `buildProtectionDomain` take an `sdk` argument, so their from-source derivation can be dropped in. ### Also in nixpkgs There was no seL4 or Microkit package in nixpkgs at all, so I sent one: [microkit: init at 2.3.0 by conao3 · Pull Request #559590 · NixOS/nixpkgs · GitHub](https://github.com/NixOS/nixpkgs/pull/559590) It installs the official pre-built SDK release, which is a tradeoff worth naming: you trust the published binaries, and in exchange a cold build takes about a minute instead of pulling a pinned kernel checkout, a rustc with rust-src and TeX Live. If you’d rather see the from-source derivation land in nixpkgs instead, say so on the PR and I’ll switch it. Repo: [GitHub - conao3/nix-sel4: Build seL4 Microkit systems from Nix: SDK, cross-compiled protection domains, generated system descriptions and a QEMU runner · GitHub](https://github.com/conao3/nix-sel4) Example: [GitHub - conao3/nix-sel4-example: A clone-and-boot seL4 Microkit system built with nix-sel4 · GitHub](https://github.com/conao3/nix-sel4-example) nixpkgs PR: [microkit: init at 2.3.0 by conao3 · Pull Request #559590 · NixOS/nixpkgs · GitHub](https://github.com/NixOS/nixpkgs/pull/559590) * * * Assisted-by: Claude Code:claude-opus-5 ---
**Author:** ![Indan](https://yyz2.discourse-cdn.com/free1/user_avatar/sel4.discourse.group/indan/32/185_2.png) [@Indan](https://sel4.discourse.group/u/Indan)\ **Post date:** [October 13, 2026, 10:18am UTC](https://sel4.discourse.group/t/nix-sel4-build-microkit-systems-from-nix-with-a-clone-and-boot-example/1087/2 "2026-10-13T10:18:34Z")
There’s [nix: wrap the microkit SDK as a Nix package by r4v3n6101 · Pull Request #615 · seL4/microkit · GitHub](https://github.com/seL4/microkit/pull/615), maybe you could add your thoughts there and contribute to the existing discussion. That said, what you want is quite different than just a Nix Microkit package. My impression is that a bunch of Nix enthusiasts want Nix packages/flakes/whatever for everything, which is absolutely fine. But I don’t see how it’s different than any other distro packaging, other than more flexibility in the package system.