With millions of LoCs, it is no surprise there are bugs.
Worse yet, the kernel runs in supervisor mode.
This kernel design is bankrupt. There's much better available, such as seL4+Genode.
replies(4):
I am sure that the tech community would love to read the details of your great success in deploying microkernels for large variety of production workloads.