Sponsored Content
Releases Contribute Contact Support Main Site seL4 on GitHub

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.

Platform System-on-chip Core Virtualisation SMMU Proofs Proof config
Avnet MaaXBoard i.MX8MQ Cortex-A53 Quad 1.5 GHz – AARCH64
BeagleBoard OMAP3 Cortex-A8 – – ARM
BeagleBone Black / Blue AM335x Cortex-A8 – – ARM
Jetson TK1 NVIDIA Tegra K1 Cortex-A15 ARM, ARM_HYP
Odroid-C2 Amlogic S905 Cortex-A53 – AARCH64
Odroid-C4 Amlogic S905X3 Cortex-A55 – AARCH64
OdroidXU Exynos5 Cortex-A15 ARM, ARM_HYP
OdroidXU4 Exynos5 Cortex-A15 ARM, ARM_HYP
QEMU Arm Virt virt Multiple – N/A
ROCKPro64 RK3399 hexa-core Cortex-A53 Quad 1.8 GHz – AARCH64
Raspberry Pi 3-b BCM2837 Cortex-A53 – ARM
Raspberry Pi 4B BCM2711 Cortex-A72 – AARCH64
Raspberry Pi 5B BCM2712 Cortex-A76 – AARCH64
Rock3b RK3568 quad-core Cortex-A55 Quad 2.0 GHz – AARCH64
STM32MP25 EV1 STM32MP25 Cortex-A35 – AARCH64
Sabre Lite i.MX6 Cortex-A9 – – ARM
TK1-SOM NVIDIA Tegra K1 Cortex-A15 ARM_HYP
TQMa8XQP 1GB i.MX8X Quad Plus Cortex-A35 – – AARCH64
TX1 NVIDIA Tegra X1 Cortex-A57 Quad AARCH64
TX2 NVIDIA Tegra X2 Cortex-A57 Quad, Dual NVIDIA Denver AARCH64
Ultra96v2 Evaluation Kit Zynq UltraScale+ MPSoC Cortex-A53 AARCH64
Zynq ZCU106 Evaluation Kit Zynq UltraScale+ MPSoC Cortex-A53 ARM, AARCH64
Zynq ZCU102 Evaluation Kit Zynq UltraScale+ MPSoC Cortex-A53 ARM, AARCH64
Zynq-7000 ZC706 Evaluation Kit Zynq7000 Cortex-A9 – – ARM
i.MX8M Mini IMX8MM-EVK Cortex-A53 Quad 1.8 GHz – – ARM, AARCH64
i.MX8M Plus IMX8MP-EVK Cortex-A53 Quad 1.8 GHz – AARCH64
i.MX8M Quad MCIMX8M-EVKB Cortex-A53 Quad 1.5 GHz – AARCH64
i.MX93 EVK i.MX93 Cortex-A55 – AARCH64

RISC-V

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

Platform System-on-chip Core Arch Proofs Proof config
Ariane Ariane (CVA6) RV64IMAC RISCV64
Banana Pi BPI-F3 SpacemiT K1 X60 RV64GCVB RISCV64
Cheshire Cheshire RV64IMAFDC RISCV64
HiFive Premier P550 ESWIN EIC7700X P550 RV64GC RISCV64
HiFive Unleashed Freedom U540 U54-MC, E51 RV64IMAC, RV64GC RISCV64
Microchip PolarFire Icicle Kit PolarFire SoC FPGA U54-MC, E51 RV64IMAC, RV64GC RISCV64
Pine64 Star64 StarFive JH7110 U74-MC, E24 RV64GBC, RV64IMAC, RV32IMAFBC RISCV64
QEMU RISC-V virt rv32, rv64 RV32GC, RV64IMAC N/A
Rocketchip Rocket RV64IMAFDC RISCV64
Rocketchip (zcu102) Rocket RV64IMAFDC RISCV64
Spike RV32GC, RV64IMAFDC N/A

x86

seL4 supports PC99-style Intel Architecture Platforms.

Platform Arch Virtualisation IOMMU Proofs Proof config
PC99 (32-bit) x86 VT-X VT-D - -
PC99 (64-bit) x64 VT-X VT-D yes X64

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.