What is a conceptual difference between seL4 and Fuchsia's kernel?

Question

Originally I thought Fuchsia was the first kernel to extensively use capability-based security, but it looks like in seL4 they are also the main security primitive.

Answer 1

Fuchsia is a capability-based operating system built on top of Google's Zircon microkernel, which is itself is based on the little kernel.

It makes more sense to compare Zircon to seL4, or an operating system framework like Genode (which runs on seL4) to Fuchsia. I'll briefly compare seL4 to Zircon.

seL4 provides minimal mechanisms and is designed for high-assurance systems. Zircon provides a lot of policy and is not designed for high-assurance, with a focus on utility. I believe both aim at high performance. In short, seL4 is a very minimal microkernel compared to Zircon.

For example while seL4 provides the mechanisms to build a process abstraction, it does not define a process at all. Comparatively Zircon has much policy built into the microkernel itself, including processes. seL4 has proofs of many properties (functional correctness, integrity, isolation) when configured for specific platforms, and Zircon does not.