---

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

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

title: The seL4 Microkernel

layout: plain

extra-script-src:

- js/[email protected]

redirect_from: /home.pml

---

<div class="w-full bg-darkblue py-6">

<div class="text-[#74ba6e] mx-4 text-center font-semibold text-base sm:text-xl lg:text-2xl">

The world's most highly assured and fastest operating system kernel

</div>

<div class="bg-darkblue">

<div id="the_div" class="relative w-full h-[18rem] sm:h-[22rem] overflow-hidden z-0">

<div id="callgraph" class="absolute h-[35rem] w-full pointer-events-none sm:pointer-events-auto sm:cursor-zoom-in "></div>

<img src="images/seL4-short.svg" alt="seL4 logo"

class="absolute w-[300px] sm:w-[400px] top-20 md:top-24 left-[calc(50%-150px)] sm:left-[calc(50%-200px)] opacity-60 cursor-default">

<img src="images/seL4-short.svg" alt="hidden seL4 logo" aria-hidden="true"

class="absolute w-[300px] sm:w-[400px] top-20 md:top-24 left-[calc(50%-150px)] sm:left-[calc(50%-200px)] opacity-60 cursor-default [mix-blend-mode:_color-dodge]">

</div>

<div class="w-full bg-darkblue py-6">

<div class="grid grid-cols-1 sm:grid-cols-2 mt-4 mb-3 gap-8 px-4 mx-auto w-2/3 sm:w-[30rem] md:w-[40rem] place-items-center">

<a href="About/" class="button-on-dark text-sm-base h-10 w-full sm:w-52 md:w-60">Learn more about seL4</a>

<a href="https://docs.sel4.systems" class="button-on-dark text-sm-base h-10 w-full sm:w-52 md:w-60">Start developing</a>

</div>

<div class="lg:px-6">

{%

include feature.html

h2="Award-winning technology backed by ground-breaking research"

text="

<p>

seL4 is both the world's most highly assured and the world's fastest

operating system kernel. Its uniqueness lies in the formal mathematical

proof that it behaves exactly as specified, enforcing strong security

boundaries for applications running on top of it while maintaining the

high performance that deployed systems need.

</p>

<p>

seL4 is grounded in research breakthroughs across multiple science

disciplines. These breakthroughs have been recognised by international

acclaimed awards, from the MIT Technology Review Award, to the ACM Hall

of Fame Award, the ACM Software Systems Award, the DARPA Game changer

award, and more.

</p>"

link="Research/"

img="images/award.jpeg"

alt="ACM SIGOPS award plaque"

%}

{%

include feature.html

right=true

h2="Protecting critical systems around the globe"

text="

<p>

seL4 protects critical systems from software failures and

cyber-attacks. It allows non-critical functionality to run securely

alongside critical payloads by enforcing strong isolation and controlled

communication.

</p>

<p>

seL4 is used in a wide range of critical sectors, from automotive,

aerospace and IoT to data distribution, military and intelligence. It

has been successfully retrofitted into complex critical systems and has

demonstrably prevented cyber-attacks. Government organisations on

several continents have funded further development of seL4 and its

ecosystem.

</p>"

link="use.html"

img="images/cpu.jpg"

alt="Conceptualised image of a CPU on a motherboard"

%}

{%

include feature.html

up=true

h2="Supported by commercial service providers"

text="

<p>

seL4 is the leading choice for building highly reliable

software. Commercial support is available to help you build or migrate

your product to run on seL4 and benefit from its unparalleled security.

</p>

<p>

A number of Trusted Service Providers have been endorsed by the seL4

Foundation for their expertise and experience in systems and/or formal

verification at various levels: kernel, kernel platform ports,

user-level Operating Systems components, and applications.

</p>

"

link="Services/"

img="images/providers.jpg"

alt="Image of a team at a table shaking hands"

%}

{%

include feature.html

right=true

up=true

h2="Backed by an Open Source Foundation"

text="

<p>

seL4 is open source, supported by the seL4 Foundation, an open,

transparent and neutral organisation. The seL4 Foundation&apos;s goal is

to ensure that seL4 continues to be the most highly-assured

operating-system technology, readily deployable with a diverse and

stable ecosystem of supporting services and products.

</p>

<p>

seL4 is free to use; its maintenance and development cost are

funded by the seL4 Foundation memberships.

</p>"

link="Foundation/"

img="images/foundation-logo-3d.png"

alt="seL4 Foundation logo in 3D"

%}

{%

include feature.html

up=true

h2="Contributions from a strong ecosystem"

text="

<p>

seL4 and its related technologies receive contributions from developers

around the world.

</p>

<p>

The microkernel code itself evolves through a tightly controlled

process, safeguarded by the Foundation's Technical bodies, to preserve

its security, high assurance, and mathematical proofs.

</p>

<p>

Frameworks, tools and components that run on top of seL4 can use seL4&apos;s

formally verified protection mechanisms and are therefore easier to

assess for correctness. This means they can evolve more rapidly and

accept community contributions at a higher pace, increasing the ease of

adoption of seL4.

</p>"

link="Contribute/"

img="images/world.jpg"

alt="image representing the earth surrounded with telecommunication connections"

%}

{%

include feature.html

right=true

up=true

h2="Annual gathering at the seL4 Summit"

text="

<p>

The seL4 Summit is the annual international conference on the seL4

microkernel and all seL4-related technology, tools, infrastructure,

products, projects, and people.

</p>

<p>

It brings together the entire seL4 community to learn about the

seL4 technology, its latest advances, uses, successes, challenges and

plans. The event showcases exciting seL4 development, research, real

world applications and experiences, offering an opportunity to connect

with other seL4 developers, users, providers, customers, supporters,

potential partners and enthusiasts.

</p>"

link="Summit/2025/index.html"

img="images/summit-talk-gernot-with-audience.jpg"

alt="Gernot Heiser presenting at the seL4 Summit 2022"

%}

{%

include feature.html

up=true

h2="Development Roadmap"

text="

<p>

With an active, public development roadmap, seL4 continues to solidify its

position as the leading secure operating system and the industry

standard for verified software. Evolution drives every level of the

seL4 ecosystem:

</p>

<p>

seL4 itself is expanding its support for an increasing range

of platforms, architectures, configurations and features.

</p>

<p>

The ecosystem is expanding with the development of frameworks,

tools, components and language support to facilitate the production of

seL4-based systems.

</p>

<p>

The formal proofs, which make seL4 unique, evolve alongside seL4.

They are constantly maintained, improved, and kept in

lock-step with the seL4 code.

</p>"

link="roadmap.html"

img="images/roadmap.jpg"

alt="Roadmap markers on an abstract path with a blue background"

%}

{%

include feature.html

right=true

up=true

h2="Documentation and learning material"

text="

<p>

Eager to learn how to use and build on seL4 or its related frameworks

and tools like Microkit, CAmkES, and Rust language support?

</p>

<p>

Explore the wide range of learning material for seL4, from hands-on

tutorials and comprehensive documentation to research articles and

university courses.

</p>"

link="Learn/index.html"

button="Get started"

img="images/documentation.jpg"

alt="concept image of learning material on a computer screen"

%}

{% capture news %}

<div class="flow-root">

<ul class="-mb-8">

{% assign items = site.news-items | reverse %}

{%- for news_item in items limit: 3 -%}

{%- assign date = news_item.date | date: "%e %b %Y" -%}

{%- assign year = date | date: "%Y" -%}

{%- assign default_anchor = news_item.date | date: "%m-%d" -%}

{%- assign anchor = news_item.anchor | default: default_anchor -%}

{%- assign this_year = "now" | date: "%Y" -%}

{%- if this_year == year -%}

{%- assign year_ext = "#" -%}

{%- else -%}

{%- assign year_ext = year | append: "#" -%}

{%- endif -%}

{%- assign item_link = "/news/" | append: year_ext | append: anchor | relative_url -%}

<li>

<div class="relative pb-8">

{% unless forloop.last %}

<span class="absolute left-6 top-5 -ml-px h-full w-0.5 bg-slate-200 dark:bg-slate-600"

aria-hidden="true"></span>

{% endunless %}

<div class="relative flex items-start space-x-3">

<div class="relative">

<a href="{{ item_link }}">

<div class="-mt-3 p-2 bg-slate-200 dark:bg-slate-600 rounded-full">

{%- svg _icons/megaphone.svg class="block h-8 w-8" -%}

</div>

</a>

</div>

<div class="min-w-0 flex-1">

<div>

<div class="text-sm">

<a href="{{ item_link }}" class="font-medium text-dark hover:underline">{{news_item.title}}&nbsp;&rightarrow;</a>

</div>

<p class="mt-0.5 text-sm text-gray-500 dark:text-gray-600">{{date}}</p>

</div>

<div class="mt-2 text-sm text-gray-700 dark:text-gray-500 line-clamp-2">

{{news_item.content}}

</div>

</div>

</div>

</div>

</li>

{%- endfor -%}

</ul>

{% endcapture %}

{%

include feature.html

up=true

h2="Latest News"

text=news

link="news/"

button="More news"

img="images/newspaper.jpg"

alt="a stack of newspapers"

%}

{% include logo-cloud.html %}

<script type="module">

function remtopx(rem) {

return rem * parseFloat(getComputedStyle(document.documentElement).fontSize);

}

const callgraph = document.getElementById('callgraph');

const Graph = ForceGraph3D()(callgraph)

.height(remtopx(35))

.backgroundColor('#030020')

.warmupTicks(40)

.cooldownTicks(500)

.jsonUrl('js/callgraph.json')

.nodeLabel('id')

.nodeRelSize(2)

.nodeResolution(12)

.nodeOpacity(1)

.nodeColor(node => node.name.length < 30 ? '#66FF00' : 'white')

.linkWidth(0.5)

.linkColor(_ => '#707080')

.linkOpacity(0.9)

.cameraPosition( { z: 850, y: 0, x: 0 }, { z: 0, y: -90, x: 0 } )

.enableNodeDrag(false)

.enableNavigationControls(true)

.showNavInfo(false);

addEventListener("resize", _ => {

const el = document.getElementById('the_div');

Graph.width(el.offsetWidth);

});

</script>