Contribute

We welcome and encourage community contribution to the seL4 platform.

Contributions can take the form of code contributions, proof contributions, documentation contributions, and community support.

Code Contributions

We provide general guidance on contributing code to the seL4 platform as well as specific guidance on making contributions to the kernel and to user-level code.

• general code contribution guidance and rules
• kernel contribution

We also provide a list of suggested projects to start working on, as well as an overview of the different libraries and components available and what can be done to help contribute to their further development.

Proof Contributions

Contributing to the seL4 proofs requires a different skill set than contributing to the code, and so far we have not had many community contributions to the proofs.

As a result, our infrastructure for proof contributions is not as mature as that for code contributions.

We are aiming to provide more resources in the next few months. In the meantime, if you are interested in contributing to the seL4 proofs, please review the actual proofs and the tools and techniques used for the proofs. Then contact us to discuss ideas, plans, and options about your contributions.

To get started, you will have to be familiar with the Isabelle theorem prover. Some learning resources for it are described in this blog post.

Documentation Contributions

seL4 platform documentation is maintained either with the code sources, with the proofs, or on the docsite.

We welcome contribution to all of this documentation, and provide guidance on the docsite.

Community Support Contributions

The seL4 discussion and support platforms are open to the community and we invite community participation, not only in asking questions, but also in answering questions and providing help.

Please see our Community Guidelines on the docsite.