We had an internal bear metal implementation already.

L4 was just pushed as the “hotness”, and ironically as a way to get around the linux GPL issues at the time.

I don’t want to sound to critical. L4 is actually easier to build drivers for than Linux, and you are much less likely to shoot yourself in the foot.

It’s a great microckernel. It’s just that 4% may all come from the most human sensitive application.

I still can't tell what L4 you're talking about. I've heard that there are some pretty big differences in performance between other L4s and seL4, for example.

The 4% come from a application-level benchmark that was popular back then. This is about ARM9/armv5 too, which is not suited for any multi-user OS as address spaces switching is very expensive compared to today's architectures (armv6+) due to the needed cache flushing on every address space switch. This has nothing to do with L4 variants, this is an architectural issue.