OKE
OKE, the Open Kernel Environment, is an extension to the Linux OS which allows users other than root to load native and fully optimised code in the kernel. It is an example of a no-kernel system.[Actually, this is not quite true: there are limitations on what can be loaded into the kernel, and there is still a kernel and a userspace.) -- A N Other, probably one of the authors]
[Please, read carefully, we are consistent with our definition of no-kernel. The relevant excerpt:
Insecure tasks, such as Unix/DOS programs running in an emulation box, or a low-level reflected implementation of the system being under development, will be isolated from the rest of the system by the traditional protection barrier, and be fully preemptively taskswitched.
-- MaD70]
The project uses a modified version of the Cyclone language to produce verified C code that the kernel can safely load.