SeL4 is a capability based operating system toolkit, entirely implemented in C. The core operating system is just a few thousand lines of code. Its even mathematically proven to be bug free - which is totally insane.

It even uses a capability to allocate (assign) memory. So you typically have a microservice (userland process) in charge of memory on the whole system. Other processes get heap memory allocated to them by asking that service for it. (Though typically you'll allocate large blocks, and divide it up using a normal allocator).