The other serious issue with using virtualization to intercept Linux system calls is that there are many situations where hardware virtualization extensions are unavailable (running in a VMM without nested virtualization, virtualization extensions are disabled in the BIOS which is the default on some PCs, or some machines just don't support them at all). Saying "you must have a system with hardware virtualization available to use the Linux compatibility environment" would be a serious hindrance to the adoption of UX/RT as a desktop/server OS. I want it to be as easy to switch to UX/RT as possible, and supporting Linux applications on all installations regardless of hardware features is a very important part of that. I can't think of any other ways besides origin limits and virtualization to distinguish for which kernel system calls using the SYSCALL instruction are intended (INT system calls could be distinguished by the vector, but they're mostly deprecated at this point and typically won't be used by modern Linux programs). A general-purpose OS for the real world doesn't have the luxury of imposing restrictions like that just for the sake of academic elegance. I do consider myself a bit of an architectural purist, but purism in an OS intended for the real world must serve practicality and not hinder it. I'm beginning to think that my goal of making a full-featured general-purpose OS that doesn't sacrifice practicality and performance for academic purism is just too divergent from the goals of seL4, and I may have to make my own fork. A verified kernel would only be nice to have and not a critical feature, since UX/RT's root server is very likely to be essentially unverifiable, and it will be just as critical to security as the kernel (it will be the only part of the system that writes to CSpaces; UX/RT will treat kernel capabilities as just an implementation detail that is not exposed anywhere in the API). That being said, I would only be expecting to add a few simple hooks that further the goal of making a practical OS rather than making any fundamental architectural changes or adding anything large or complex. The general architecture of seL4 is already more or less ideal as far as I'm concerned.