Verified Configurations

This page describes which architecture/platform/configuration combinations of seL4 have verified properties, which configurations possess which properties, and how to obtain an seL4 version for a specified configuration. For an overview of these properties and their explanations, please see the verification page on the seL4 website. The Frequently Asked Questions also as a section on the formal verification of seL4.

The formal proofs for seL4 are hosted at https://github.com/seL4/l4v. They are written in the Isabelle/HOL theorem prover. See the README file in the l4v repository for build and setup instructions if you want to run and check the proofs against a specific version and configuration of seL4.

Examining and Building Verified Configurations

Current verified configurations can be found in seL4 sources in the configs folder:

cd configs/
ls *_verified.cmake
# AARCH64_bcm2711_verified.cmake    ARM_exynos5410_verified.cmake
# AARCH64_hikey_verified.cmake      ARM_exynos5422_verified.cmake
# AARCH64_odroidc2_verified.cmake   ARM_hikey_verified.cmake
# AARCH64_odroidc4_verified.cmake   ARM_imx8mm_verified.cmake
# AARCH64_verified.cmake            ARM_tk1_verified.cmake
# AARCH64_zynqmp_verified.cmake     ARM_verified.cmake
# ARM_HYP_exynos5410_verified.cmake ARM_zynq7000_verified.cmake
# ARM_HYP_exynos5_verified.cmake    ARM_zynqmp_verified.cmake
# ARM_HYP_verified.cmake            RISCV64_MCS_verified.cmake
# ARM_MCS_verified.cmake            RISCV64_verified.cmake
# ARM_exynos4_verified.cmake        X64_verified.cmake

To obtain specific source code and build for a given configuration (e.g. ARM) in a build directory:

mkdir build
cd build
cmake -P ../config/ARM_verified.cmake

Notably kernel.elf is the kernel binary, and kernel_all_pp.c is the kernel source code after preprocessing, which is used as the basis for verification efforts.

Also see standalone seL4 builds for general guidelines on generating an seL4 binary and build system information from an existing configuration.

Available Verified Configurations

Unverified Features

At present, none of our verified configurations take into account address translation for devices (System MMU or IOMMU), debug/profiling interfaces, or the kernel startup at boot.

The proofs for RISCV64_MCS/ARM_MCS (mixed-criticality extensions to real-time seL4 features), as well as security proofs for AARCH64 are in progress. Refer to the roadmap for status and upcoming features.

ARM Sabre Lite

ARM Exynos 4

ARM Exynos 5

ARM Hikey

ARM TK1

ARM Zynq7000

ARM ZynqMP

ARM IMX8MM-EVK

ARM_HYP TK1

ARM_HYP Exynos5

ARM_MCS

AARCH64

AARCH64 RPI4

AARCH64 Hikey

AARCH64 Odroid C2

AARCH64 Odroid C4

AARCH64 ZynqMP

RISCV64

RISCV64_MCS

X64