seL4-docs/getting-started.md

3.0 KiB

SPDX-License-Identifier SPDX-FileCopyrightText
CC-BY-SA-4.0 2020 seL4 Project a Series of LF Projects, LLC.

Getting Started

Building Systems on seL4

The quickest and easiest way to get started with building a system on top of seL4 is the seL4 Microkit. We recommend to:

The Microkit is for systems with a statically described software architecture. For dynamic systems, you may want to work on the seL4 API directly (see below), or use one of the tools & frameworks that the seL4 ecosystem has to offer.

Learning about seL4

If you are planning to write a dynamic system or you want to learn about seL4 itself, we recommend to:

If you are looking for deeper background reading material, you might be interested in the selection of research publications on seL4 on the main website.

Writing Rust on seL4

The Rust programming language is a great fit for writing applications on top of seL4. Check out:

Build instructions and tests

If you just want instructions for building and running the seL4 kernel, check the page on setting up your machine.

The proofs

seL4's claim to fame is that it is formally verified. These formal proofs are available in the l4v repository with their own setup and build instructions. See the verification pages on the main website for an overview of the proofs, and check the Verified Configurations to know which architecture/platform/configuration combinations of seL4 have verified properties.

Help and Support

Check out the navigation on the left for the main content of this documentation site.

If you have questions, you can head to the New to seL4 section on seL4 discourse or the general seL4 community help and support channels.