Tools, Frameworks & Languages
Below is a list of available tools, frameworks, Software Development Kits (SDKs), and supported languages for seL4, either provided by the seL4 Foundation or provided by the seL4 community. Some are open source (potentially still in development), while others are commercial. If you would like an item to be added, please contact us at foundation@sel4.systems.
Development Kits & Component Frameworks
Microkit
Abstraction layer, SDK and tools that simplify development of statically architected seL4-based systems. Focus on high performance and simplicity.
In active development. Ready for use, but not all features and configurations supported yet. For mixed-criticality scheduling (MCS) kernel configurations only.
Use when feature set is sufficient, and kernel configuration and verification requirements are supported by Microkit for your use case.
CAmkES
Development and runtime component framework for microkernel-based embedded static systems. Eventually to be replaced by Microkit, but still supported. Currently more mature, and feature rich.
Use when features not yet supported by Microkit are needed for your project, or verification requirements are not met by the kernel configurations supported by Microkit.
sDDF
A verifiable seL4 device driver framework providing a set of interfaces, designs and tools for developing high-performance, encapsulated device drivers for seL4, developed at UNSW.
seL4 Dev Kit
An seL4 development kit aimed at helping complete beginners get started and evaluate seL4 for their needs, developed by Capgemini Engineering and funded by the National Cyber Security Centre (NCSC).
BriefCase
A model-based systems engineering environment that can build systems targeting seL4, based on AADL and OSATE, from the DARPA CASE program.
Operating Systems
LionsOS
Highly modular, adaptable, verifiable, high-performance OS for statically architected embedded/IoT/cyberphysical systems, developed at UNSW. Based on Microkit.
KOS
Kry10 Operating System (KOS) and Platform, designed for mission critical connected devices and integrated with the Erlang BEAM application environment, developed by Kry10.
Virtualisation
CAmkES VMM Library
Virtual Machine Monitor library on seL4 with CAmkES, with support for AArch32, AArch64, and x64.
Microkit VMM Library
Virtual Machine Monitor library on seL4 using Microkit, currently with support for AArch64 only. RISC-V support is in development.
VM Composer
A Secure Microkernel Virtual Machine (VM) Composer, a modelling tool to develop and deploy virtualised high-assurance systems using a drag-and-drop interface, developed by DornerWorks.
Language Support
C and Rust are the default languages on top of seL4, but other languages are supported, in particular for application-level components. seL4 as such is language agnostic. The main effort in using a new programming language on top of seL4 usually lies in providing functionality for a runtime environment and standard library.
C/C++
Comprehensive support for C, including musllibc bindings.
Limited support for C++ without standard library.
Rust
Comprehensive support, including async, for using the Rust
programming language on top of seL4 directly or in Microkit.
For no_std applications with and without alloc.
Pancake
Low-level, imperative language with a verified compiler, designed for implementing verifiable device drivers and other OS code.
MicroPython
Support for MicroPython, a slimmed down version of Python, intended for embedded use cases. Needs higher-level OS services, which are currently supported on LionsOS only.