I've seen microkernels mentioned a few times between these LPE posts and I'm curious about why. Would they be fundamentally more secure against forgetting to add bounds checking, or assuming user-provided input buffers should be writable without checking?