I know nothing about differences between fuchsia and sel4 but it would be rather strange if something as complicated as a OS kernel wouldn't have many parts where you have to make trade-offs. People compete fiercely in the field of todo applications, I don't see why there shouldn't be competition in microkernel space.
Things changed in hardware in last 20 years and maybe we've learned something about software as well.
Not to mention that sel4 is GPLv2, which is kind of problematic for a commercial company.
In the end, the micro-kernel is a very small part of the whole stack.
I think author meant L4 kernels were performance tuned for 20 years to be the fastest. Then, one using applying such lessons was mathematically verified for correctness down to assembly. It's proprietary and open-source depending on what your end product will be. They'd probably even add features to it for a Google-specific version that leveraged as many proven compinents as possible.
That's true in its current state. Remember, though, that they're working on multithreading in a way that ties into their proof from high-level spec down to the code down to the assembly. Googles people are just putting together a kernel with review & testing. They could take seL4, modify it for concurrency, check it with concurrency-related tooling, and still get quite a bit of assurance from original work. Proof no longer applies but most things it applied to haven't changed. And model-checkers for concurrency are among easiest tools to use in formal verification w/ TLA+ getting adoption even by mainstream companies.
Things changed in hardware in last 20 years and maybe we've learned something about software as well.
Not to mention that sel4 is GPLv2, which is kind of problematic for a commercial company.
In the end, the micro-kernel is a very small part of the whole stack.