Hi, I'm the author of this project (I didn't post this on HN someone else did). We have implemented NT processes. All device drivers and user executable are NT processes (created by NtCreateProcess or RtlCreateUserProcess). What we don't have is Win32 process, because there is no Win32 subsystem yet.

Ah, gotcha, I missed that. Thanks for the correction.

They can start an Native process (ntcmd.exe) but that's about it, as the commands available don't run due to missing bits.

The keyboard driver stack is working (we also have a PC speaker driver that makes an annoying beep). It's actually not as trivial as it seems, because passing IRPs across process boundary while maintaining the consistency of states is not that easy to get right, among other things. The goal of the very first release is to demonstrate that one can run Windows kernel drivers in seL4 user space and have a Windows (native NT, not Win32) application communicate with said Windows drivers via standard NT primitives (NtOpenFile and whatnot).