The seL4 microkernel
The seL4 kernel itself is the core software program, running in privilege mode, providing applications with a minimal abstraction layer above the hardware. Applications can be built directly on top of seL4, or, for an easier entry point, using frameworks like Microkit or CAmkES.
General information about the seL4 microkernel, including details about its formal verification are found on the seL4 main site, which also contains other sources of learning, such as publications, courses, and a white paper, as well as an extensive FAQ.
We welcome contributions to seL4. Please see how to contribute.
The seL4 kernel itself is open source and licensed under the GPL, version 2. Application code, operating system components, and drivers can have any license, proprietary or open source. The GPL propagation clause of the kernel license stops at the kernel/user code boundary.
Tutorial
Verified Configurations
To build the seL4 kernel, please follow the set up instructions.
If you believe you have found a security vulnerability in seL4 or related software, we ask you to follow our vulnerability disclosure policy.