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 |
|---|---|---|---|
| AARCH64 RPI3 | RPI3 | No | 10.1.0 |
| 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 |
| 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)
Experimental Branches
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.