Hello! Operating system noob here, I understand that in most mainstream operating systems (Linux, BSDs, MacOS, Windows) drivers are part of the kernel. And in micro kernel operating systems like Minix and seL4, drivers are part of user space. But Minix is a lot closer to a traditional POSIX kernel, and seems to implement some of that (IE posix threads, IPC) in the kernel, which makes the environment for a driver programmer a bit more familiar. How do drivers work in seL4, then? How does a driver obtain permission for hardware access from the kernel? I imagine it works with a capability delegated by the root task, but how do you solve chicken and the egg type problems, like loading driver code, without driver code already loaded? Is it an initramfs like Linux/Unix? Also, what if seL4 is being used _as_ the firmware/bootloader? Obviously it can load the seL4 kernel and user space OS components from a file system to put them in the booting OS’ memory, but how does it load drivers for itself? I’m assuming there’s some low level platform specific code, but is that code verified or part of the proofs?