From my understanding, it was designed to be a small, verifiable kernel intended for use in applications with high-end reliability requirements (e.g., military, aerospace).
In the case of seL4, verifiability comes from a formal specification of its key operations that is proven using a theorem prover. The spec is implemented in multiple languages including Haskell and of course C.
As it stands, formal verification is limited to very small codebases: seL4 itself is on the order of 10k lines of C. Extending the proof further outside the current boundary to cover additional functions that are typically found in OS kernels would be prohibitive to say the least!
>From my understanding, it was designed to be a small, verifiable kernel intended for use in applications with high-end reliability requirements (e.g., military, aerospace).
It's immediately and very obviously useful for these fields. It is small indeed, because it follows the principle of minimality, introduced by Liedtke's L4. But do not get this wrong: It is a general purpose µkernel.
This principle of minimality (the supervisor mode µkernel should only do something if it can't be done by a service in user mode) is the difference between 1st and 2nd generation µkernels. seL4 is a 3rd generation µkernel: It's designed around capabilities.
Genode is building a framework to create OSs based on µkernels. They do support many µkernels, but there's been some serious effort put into their seL4 support. Genode isn't quite there yet for this purpose, but does have ambitions of being the base for a general purpose OS.
In the case of seL4, verifiability comes from a formal specification of its key operations that is proven using a theorem prover. The spec is implemented in multiple languages including Haskell and of course C.
As it stands, formal verification is limited to very small codebases: seL4 itself is on the order of 10k lines of C. Extending the proof further outside the current boundary to cover additional functions that are typically found in OS kernels would be prohibitive to say the least!