---

# Copyright 2020 seL4 Project a Series of LF Projects, LLC.

# SPDX-License-Identifier: CC-BY-SA-4.0

title: Tools, Frameworks & Languages

sub: '

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

<a title="[email protected]"

href="mailto:[email protected]">[email protected]</a>.

</p>'

layout: card

---

<div class="section-borders -mt-12 pt-0">

<h2 id="devkits" class="text-center my-16 text-3xl font-bold tracking-tight text-dark md:text-4xl">Development Kits &amp; Component Frameworks</h2>

<div class="grid grid-cols-1 lg:grid-cols-2 gap-y-24 gap-x-12 lg:gap-x-20 px-10 pt-8 pb-12 sm:pb-20">

{% include card_tool.html

title="Microkit"

icon="puzzle-piece"

type="Open Source"

foundation=true

link="https://docs.sel4.systems/projects/microkit"

body='<p>

Abstraction layer, SDK and tools that simplify development of statically

architected seL4-based systems. Focus on high performance and simplicity.

</p>

<p class="mt-2">

In active development. Ready for use, but not all features and

configurations supported yet. For mixed-criticality scheduling (MCS)

kernel configurations only.

</p>

<p class="mt-2">

Use when feature set is sufficient, and kernel configuration and

verification requirements are supported by Microkit for your use case.

</p>

'

%}

{% include card_tool.html

title="CAmkES"

icon="puzzle-piece"

type="Open Source"

foundation=true

link="https://docs.sel4.systems/projects/camkes/"

body='<p>

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.

</p>

<p class="mt-2">

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.

</p>'

%}

{% include card_tool.html

title="sDDF"

icon="puzzle-piece"

type="Open Source"

foundation=false

link="https://trustworthy.systems/projects/drivers"

body='<p>

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.

</p>'

%}

{% include card_tool.html

title="seL4 Dev Kit"

icon="book-open"

type="Open Source"

foundation=false

link="https://sel4devkit.github.io"

body='<p>

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).

</p>'

%}

{% include card_tool.html

icon="cog-6-tooth"

title="BriefCase"

type="Open Source"

foundation=false

class="lg:col-span-2 lg:w-3/4 lg:mx-auto"

link="https://github.com/loonwerks/BriefCASE-Tutorial"

body='<p>

A model-based systems engineering environment that can build systems

targeting seL4, based on AADL and OSATE, from the DARPA CASE program.

</p>'

%}

</div>

<div class="section-borders -mt-12 pt-0">

<h2 class="text-center my-16 text-3xl font-bold tracking-tight text-dark md:text-4xl">Operating Systems</h2>

<div class="grid grid-cols-1 md:grid-cols-2 gap-y-24 gap-x-12 lg:gap-x-20 px-10 pt-8 pb-12 sm:pb-20">

{% include card_tool.html

title="LionsOS"

icon="squares-plus"

type="Open Source"

foundation=false

link="https://trustworthy.systems/projects/LionsOS/"

body='<p>

Highly modular, adaptable, verifiable, high-performance OS for statically

architected embedded/IoT/cyberphysical systems, developed at UNSW.

Based on Microkit.

</p>'

%}

{% include card_tool.html

title="KOS"

icon="squares-plus"

type="Commercial"

foundation=false

link="https://www.kry10.com/#platform"

body='<p>

Kry10 Operating System (KOS) and Platform, designed for mission critical

connected devices and integrated with the Erlang BEAM application

environment, developed by Kry10.

</p>'

%}

{% include card_tool.html

title="Sculpt OS"

icon="squares-plus"

type="Open Source"

foundation=false

link="https://genodians.org/alex-ab/2025-11-02-sculpt-multi-kernel"

body='<p>

Sculpt is a general-purpose OS that combines Genode&#39;s

microkernel architecture, capability-based security, sandboxed

device drivers, and virtual machines in a novel operating system

for commodity PC hardware and the PinePhone. Sculpt is used as

day-to-day OS by the Genode developers. It has an (unofficial

and experimental) variant based on seL4.

</p>'

%}

</div>

<div class="section-borders -mt-12 pt-0">

<h2 id="virtualisation"

class="text-center my-16 text-3xl font-bold tracking-tight text-dark md:text-4xl">Virtualisation</h2>

<div class="grid grid-cols-1 lg:grid-cols-2 gap-y-24 gap-x-12 lg:gap-x-20 px-10 pt-8 pb-12 sm:pb-20">

{% include card_tool.html

title="CAmkES VMM Library"

icon="server-stack"

type="Open Source"

foundation=true

link="https://docs.sel4.systems/projects/camkes-vm/"

body='<p>

Virtual Machine Monitor library on seL4 with CAmkES, with support for AArch32, AArch64, and x64.

</p>

'

%}

{% include card_tool.html

title="Microkit VMM Library"

icon="server-stack"

type="Open Source"

foundation=false

link="https://github.com/au-ts/libvmm"

body='<p>

Virtual Machine Monitor library on seL4 using Microkit, currently with support for AArch64 only.

RISC-V support is in development.

</p>

'

%}

{% include card_tool.html

title="VM Composer"

icon="server-stack"

type="Commercial"

foundation=false

class="lg:mx-auto lg:w-4/5 lg:col-span-2"

link="https://www.dornerworks.com/vm-composer"

body='<p>

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.

</p>'

%}

</div>

<div class="section-borders -mt-12 pt-0">

<h2 id="languages"

class="text-center mt-16 mb-6 text-3xl font-bold tracking-tight text-dark md:text-4xl">Language Support</h2>

<p class="text-center mb-6 text-light leading-6 text-base sm:text-lg">

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.

</p>

<div class="grid grid-cols-1 md:grid-cols-2 mt-16 gap-y-24 gap-x-12 lg:gap-x-20 px-10 pt-8 pb-12 sm:pb-20">

{% include card_tool.html

title="C/C++"

icon="other/C"

type="Open Source"

foundation=true

link="https://docs.sel4.systems/Tutorials/"

body='<p>

Comprehensive support for C, including <code>musllibc</code> bindings.

Limited support for C++ without standard library.

</p>'

%}

{% include card_tool.html

title="Rust"

icon="other/rust-logo-blk"

type="Open Source"

foundation=true

link="https://github.com/seL4/rust-sel4"

body='<p>

Comprehensive support, including <code>async</code>, for using the Rust

programming language on top of seL4 directly or in Microkit.

For <code>no_std</code> applications with and without <code>alloc</code>.

</p>'

%}

{% include card_tool.html

title="Pancake"

icon="circle-stack"

type="Open Source"

foundation=false

link="https://trustworthy.systems/projects/pancake/"

body='<p>

Low-level, imperative language with a verified compiler, designed for

implementing verifiable device drivers and other OS code.

</p>'

%}

{% include card_tool.html

title="MicroPython"

icon="other/python-logo-only"

type="Open Source"

foundation=false

link="https://lionsos.org/docs/use/language_support/#micropython"

body='<p>

Support for <a href="https://micropython.org">MicroPython</a>, a slimmed

down version of Python, intended for embedded use cases. Needs

higher-level OS services, which are currently supported on LionsOS only.

</p>'

%}

{% include card_tool.html

title="Erlang and Elixir"

icon="other/Elixir"

type="Commercial"

foundation=false

link="https://www.kry10.com/resources"

class="md:col-span-2 md:w-2/3 md:mx-auto"

body='<p>

Commercial support by Kry10 for the

<a href="https://www.erlang.org">Erlang</a> and

<a href="https://elixir-lang.org">Elixir</a> languages on

<a href="https://www.kry10.com/#platform">KOS</a> on top of seL4.

</p>'

%}

</div>