1. Home
  2. Learn
seL4

Learn about seL4

Docsite

We have a separate website for technical seL4 documentation, which we call the Docsite. The docsite is community maintained - its source is hosted on GitHub and can be edited using standard GitHub procedures as documented on the docsite itself.

Tutorials

The best way to learn to use seL4 is to follow our tutorials. We provide a series of hands-on tutorials that cover the basics of seL4, the kernel and core library APIs, user-level frameworks, and virtualisation.

If you want to know how to use seL4, then this is where you should start. See the Tutorials page on our docsite.

If you prefer unstructured learning and want to dive in and explore on your own then follow the links on the docsite's Getting Started page.

After getting a solid seL4 background you can move on to building seL4-based systems. Next steps include working on one of our suggested projects or helping to expand the collection of libraries and components available to build seL4-based systems.

Documentation

We've written a lot about the seL4 kernel: from overview papers, historical background, and project retrospectives, to detailed documentation of the kernel API, user-level libraries and components, and system frameworks.

Besides the kernel implementation and the systems aspects of seL4, we've also written about the seL4 proofs: from overview papers explaining the models and the proofs, details of proof techniques developed and used for the proof, insights gained through doing the proofs, to detailed documentation of the proofs themselves.

See the Documentation page on our docsite for information about all of these.

Courses

seL4 is being used as the basis of several (University-level) courses, including:

  • Advanced Operating Systems at UNSW. This course provides an extensive seL4-based assignment that teaches students how to build an operating system on seL4. The course material (all lecture slides, the project and related code) are publicly available. Videos of lectures covering seL4 are available from the UNSW CSeLearning COMP9242 YouTube channel.

  • Advanced Topics in Software Verification at UNSW. While not directly about seL4, this course teaches Isabelle/HOL and the program verification techniques used to develop seL4's proof. Following this, or a similar, course is necessary if you intend to contribute to the seL4 proofs.