3 ms·

Isn't seL4 a microkernel with a strict capabilities model?

• johncolanduoni 6y ago
  SeL4 currently doesn’t have shared memory concurrency, and is only the kernel part. It’s focused heavily on formal verification, and makes a number of other sacrifices (in particular to performance) to achieve that. I’m a big fan of formal verification, but seL4 levels of assurance are still too unwieldy with current tools for an application that doesn’t place a massive premium on it. It’s also worth noting that the Fuchsia equivalent would be Zircon, which is a relatively small part of the Fuchsia project (and will only get smaller in proportion).