The SeL4 kernel is 10k lines of code. OKL4 is 13k. QNX is ~30k.
I've asked this question a few times over the last few years when people bring up "we must use microkernel now! They already exist!"-type posts, and thus far the response has either been crickets or vague hand-waving with microbenchmarks that bear no relation to real-world programs.
"It's fun having access to everything."
— Terry A. Davis
I think this would get messy quick in an OS designed by more than one person
Ironic (in the alannis morrisette sense) that Apple has strictly controlled hardware AND OS-level software...if there's anybody out there that can possibly get away with a monolithic kernel in a safe way, it would be them. But Linux...where you have to support practically infinite variations in hardware and the full bazaar of software, that's a dumpster fire waiting to happen.