seL4 releases

This page documents tagged releases of the seL4 kernel and proofs, for documentation on the release process we follow see here.

Landmark releases

This section documents the version at which specific features were introduced to seL4. For future features, see seL4 status. For other previous features, see the release notes below.

Verification Status carries the following definitions and refers to the version specified in the verification manifest tagged for that specific release.

  • No: As of this release, this feature is not verified.
  • FC: the functional correctness proofs are complete.
  • FCI: the integrity proofs are complete, in addition to functional correctness.
  • Yes: this feature has functional correctness, integrity and infoflow proofs completed, for verified platforms, as of this release.

For the verification status of all platforms, see Hardware.

Feature Hardware Verification status Available From
32-bit RISC-V architecture support RISC-V (Spike simulation target) No 10.0.0
64-bit RISC-V architecture support RISC-V (Spike simulation target) No 9.0.1
Meltdown mitigation x86 No 9.0.0
Spectre mitigation x86 No 9.0.0
Zynq UltraScale+ MPSoC Xilinx ZCU102, ARMv8a, Cortex A53 No 8.0.0
Multiboot2 support x86 No 8.0.0
CMake based build system all N/A 7.0.0
ARM 32-bit SMP Sabre No 6.0.0
ARMv7 32-bit FPU support ARM No 6.0.0
ARM 64-bit support Aarch64 No 5.0.0
64-bit x86 support x86_64 No 4.0.0
Raspberry Pi 3 support RPI3 No 4.0.0
ARM Hypervisor initial support ARM FC 3.2.0
First ARMv8 support HiKey No 3.1.0
NVIDIA Tegra K1 support TK1 No 3.0.1
Notification binding all Yes 2.0.0

Master (verified kernel)

seL4 9.0.1 (manual)

seL4 9.0.0 (manual)

seL4 8.0.0 (manual)

seL4 7.0.0 (manual)

seL4 6.0.0 (manual)

seL4 5.2.0 (manual)

seL4 5.1.0 (manual)

seL4 5.0.0 (manual)

seL4 4.0.0 (manual)

seL4 3.2.0 (manual)

seL4 3.1.0 (manual)

seL4 3.0.1 (manual)

seL4 3.0.0 (manual)

seL4 2.1.0 (manual)

seL4 2.0.0 (manual)

seL4 10.0.0 (manual)

Experimental Branches

We occasionally pre-release experimental branches for community feedback and availability.

Mixed Criticality Support (MCS) / Realtime

seL4 9.0.0-mcs (manual)

seL4 5.2.0-mcs (manual)

seL4 1.0.0-rt-dev (manual)

seL4 0.0.1-rt-dev (manual)