Licensing

The code and documentation in the repositories of the seL4 GitHub organisation are available under standard open-source licenses, identified by SPDX license tags.

The seL4 Foundation licenses and accepts contributions for

• the seL4 kernel itself under GPL Version 2,
• user code and proof libraries under the BSD 2 Clause license,
• code and proofs that depend on GPL-code or GPL-proofs under GPL,
• documentation under Creative Commons Attribution-ShareAlike.

Note that, as in the Linux syscall note for the GPL, the seL4 kernel GPL license does not cover user-level code that uses kernel services by normal system calls - this is merely considered normal use of the kernel, and does not fall under the heading of “derived work”. Syscall headers are provided under BSD.

For a longer explanation of how the seL4 license does or does not affect your own code see also this blog post.

The repositories of the seL4 GitHub organisation also contain third-party code under additional compatible open source licenses. See the individual file headers for details, or use one of the publicly available SPDX tools to generate a software bill of materials. The directory LICENSES/ in each repository contains the text for all licenses that are mentioned by files in that repository.