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).
I think Apple uses an L4 variant for their SEP co-processor, though I'm not sure if it's that specific one. Sounds like another OS I'll probably have to do a deep dive into at some point.
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).