L4 is a joy to use.

I haven't worked with seL4, but used an earlier branch of the L4 family (L4Ka::Pistachio) as a base for a toy OS (university project).

If I had the time to tinker with base OS design today, I'd definitely start with seL4.

Edited to add: the whitepaper here is a good intro to seL4: https://sel4.systems/About/seL4-whitepaper.pdf