This is more true than many here may realize. If you're not familiar with how microkernels work, remember that everything is moved from kernel to user space if

This is more true than many here may realize. If you're not familiar with how microkernels work, remember that everything is moved from kernel to user space if it's at all feasible to do so. In L4 and related systems, that usually means that the kernel doesn't even include the memory manager (the "pager"). So even page faults are handled by application code, which IIRC is not part of the current verification.