Earlier quoted context omitted.
For a modern example, there's seL4. I believe it does no dynamic memory allocation. It's also formally verified for various properties. (Arguably?) its biggest contribution to kernel design is the pervasive usage of capabilities to securely but flexibly export control to userspace.
And unfortunately had its funding dumped because it wasn’t shiny AI.
seL4 is now a healthy non-profit, seL4 foundation[1].
0. https://microkerneldude.org/2022/02/17/a-story-of-betrayal-c...
1. https://microkerneldude.org/2022/03/22/ts-in-2022-were-back/