This page documents tagged releases of the seL4 kernel and proofs, for documentation on the release process we follow see here.
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|
|TX2 support (Aarch64 only)||TX2||No||10.1.0|
|Support for more than 1 VM||ARM||No||10.1.0|
|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|
|Zynq UltraScale+ MPSoC||Xilinx ZCU102, ARMv8a, Cortex A53||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|
Master (verified kernel)
We occasionally pre-release experimental branches for community feedback and availability.
Mixed Criticality Support (MCS) / Realtime
As of seL4 version 11.0.0, this is now provided via the kernel configuration option
KernelIsMCS in CAmkES which should be set to
ON which switch the scheduler implementaiton and enable the MCS API.