Supported Platforms

Verification status

The seL4 proofs are only for specific platforms, as noted in the tables for x86 and ARM below, in the Status column, as follows:

Simulating seL4

Running seL4 in a simulator is a quick way to test it out and iteratively develop software. However, not that the feature support is limited by the simulator.

x86

We support PC99-style Intel Architecture Platforms.

Platform Arch Virtualisation IOMMU Status Contributed by Maintained by
PC99 (32-bit) x86 VT-X VT-D Unverified Data61 Data61
PC99 (64-bit) x64 VT-X VT-D Pending Data61 Data61

ARM

seL4 has support for select ARMv6, ARMv7 and ARMv8 Platforms.

Platform System-on-chip Core Arch Virtualisation IOMMU Status Contributed by Maintained by
KZM i.MX31 ARM11 v6 No No Unverified Data61 Data61
Arndale Exynos5 A15 v7A ARM HYP No Unverified Data61 No
BeagleBoard OMAP3 A8 v7A No No Unverified Data61 Data61
Beaglebone Black AM335x A8 v7A No No Unverified external Data61
Inforce IFC6410 Snapdragon S4 Pro APQ8064 krait (A15-like) v7A ARM HYP - Unverified Data61 No
Jetson TK1 (NVIDIA) Tegra K1 A15 v7-1A ARM HYP System MMU Unverified Data61 Data61
Odroid-X Exynos4412 A9 v7A No No Unverified Data61 Data61
Odroid-XU Exynos5 A15 v7A ARM HYP limited System MMU Unverified Data61 Data61
Sabre Lite i.MX6 A9 v7A No No Verified Data61 Data61
TK1 SOM (Colorado Engineering) Tegra K1 A15 v7-1A ARM HYP System MMU FC (without MMU) Data61 Data61
Zynq-7000 ZC706 Evaluation Kit Zynq 7000 A9 v7A No No Unverified Data61 Data61
Zynq ZCU102 Evaluation Kit Zynq !UltraScale+ MPSoC A53 v8A ARM HYP System MMU Unverified DornerWorks Data61
Jetson TX1 (NVIDIA) Tegra X1 Quad A57 v8A, aarch64 ARM HYP System MMU Unverified Data61 Data61
HiKey Kirin 620 A53 v8A, aarch32 & aarch64 ARM HYP - Unverified Data61 Data61
Raspberry Pi 3-b BCM2837 A53 v8A aarch64 ARM HYP - Unverified Data61 Data61

RISC-V

We currently provide a prototype support for the 64-bit RISC-V spike platform. See Simulating RISC-V. Multicore and the floating point unit (FPU) are not supported.

platform (board) status cotributed by maintained by
Spike Unverified Data61, Hesham Almatary Data61