[BlueRock-Jake]

Spent a couple years essentially building exactly that at BlueRock. We had a partially formally verified microkernel that we would insert between the hardware and OS to intercept system calls. Under 10,000 lines of code by design, deployed in some very high-security environments.

Funnily enough we had to pivot to securing agentic AI (with a few pit stops along the way) because it was an extremely hard sell. We needed access to bare metal and the pitch to teams to allow us to do that was excedingly hard. Now, we've pretty much come full circle.

I believe AI could push people to look at securing Linux structurally but its hard for me to imagine they overcome the inertia we faced. Does bring up other interesting questions about AI-assisted formal verification, which even saying sounds weird. If you can verify a narrow slice of the call chain cheaply, you don't need to solve the whole kernel.

One more thing in regard to AI, the deployment model is shifting. Running agents on laptops is increasingly the wrong pattern. As they move to server infrastructure with real credentials and network access, the relevant security question changes too. Perimeter controls don't follow the workload, which is what's needed. The kernel approach addresses that but so does living/enforcing inside the execution itself.