Supported platforms

seL4 is available on 3 major hardware architectures, Arm, RISC-V and x86, for a number of platforms with varying hardware features.

The tables below list the platforms for which seL4 is available. For each platform, the tables list whether specific features are supported (e.g. Virtualisation, IOMMU/SMMU, etc) and to which degree (where applicable), as well as the verification status for that platform.

seL4 is formally verified for specific configurations for a subset of these platforms. The depth of the proofs and which properties are verified depend on the platform and are noted in the Verification Status column as follows:

• Unverified: this platform is not verified at all and is not scheduled for verification.
• Ongoing: this feature is currently undergoing verification.
• FC: the functional correctness proofs are complete.
• Verified: all proofs for this platform are complete, including functional correctness, integrity and information flow.

More information can be found on the Verified Configurations page.

Arm

seL4 has support for select ARMv7 and ARMv8 Platforms. In addition to the page with general instructions how to run seL4 on Arm, each board page may have additional instructions for running seL4 on it.

RISC-V

We currently provide support for some of the RISC-V platforms. Support for the hypervisor extension is yet to be mainlined.

x86

seL4 supports PC99-style Intel Architecture Platforms.

Platform	Arch	Virtualisation	IOMMU	Verification Status
PC99 (32-bit)	x86	VT-X	VT-D	Unverified
PC99 (64-bit)	x64	VT-X	VT-D	FC (without VT-X, VT-D and fastpath)

Simulating seL4

Running seL4 in a simulator is a quick way to test it out and iteratively develop software. Note that feature support is then limited by the simulator. See the QEMU Arm and RISCV targets and the simulation instructions for sel4test for x86 for how to run seL4 using QEMU. Some hardware platforms support the SIMULATION=1 option — this will be marked on the respective platform page and will generally be good enough to run most of the seL4 test suite, but QEMU usually does not provide enough hardware device implementation to build more complex systems in the simulated environment.

Not in the lists above?

If the platform, architecture, feature that you are after is not listed on this page, you have several options, listed below. It is important to note however that, as explained in the guidelines linked below, contributing new ports or features will require compelling arguments, discussion with the technical community (including through Request-For-Comments), as well as testing requirements and maintenance/expertise commitment, to a degree depending on the nature of the contribution.

• You can contact one of the seL4 Foundation Endorsed Services Providers to get commercial support or professional advice to develop such a port or feature (with the implications and expectations detailed in our guidelines for contributing kernel code);

• You can check the roadmap for any planned contributions, from the seL4 Foundation or larger community, such on any new architecture ports, new large formal verifications, or large or fundamental new features;

• You can contact the seL4 community through one of our communication channels to ask whether someone is developing such a port or feature already, or whether there is general interest in discussing such a new port or feature;

• If you are in a position to develop the seL4 port or feature yourself, you should follow our guidelines for contributing kernel code, which details the implications and expectations.