seL4 explained, the 10,000-line kernel with a million lines of proof

On 29 July 2009 a research team in Sydney eliminated the last sorry from an Isabelle/HOL development and produced something no one had produced before: a machine-checked mathematical proof that the C implementation of an operating-system kernel behaves exactly as its formal specification says it does, and does nothing else. The kernel was seL4. It was roughly 8,700 lines of C plus about 600 lines of assembler. The proof was around 200,000 lines of Isabelle. Seventeen years later, that proof base has grown past a million lines, the kernel has grown to somewhere between 10,000 and 16,000 lines depending on architecture, and no functional-correctness defect has ever been found in the verified code.

A kernel small enough to prove and fast enough to ship

That last sentence is the entire argument for seL4, and it is worth being precise about what it does and does not claim. It does not claim seL4 is unbreakable. It does not claim systems built on seL4 are secure. It claims that within a carefully enumerated set of assumptions, one specific component — the kernel, the part of the system that runs with full hardware privilege and that every other component must trust — has been proven not to deviate from its specification. Everything else about a system’s security remains the system designer’s problem. seL4’s contribution is that it removes one specific class of problem from the list, permanently, in a way that testing cannot.

What makes seL4 genuinely unusual is the second half of its tagline. High-assurance software has a reputation for being slow, and for good reason: the standard route to provable behaviour is to simplify, to remove optimisation, to make the code tractable rather than fast. seL4 refused that trade. Its inter-process communication path — the operation that dominates performance in any microkernel-based system, because every service call crosses an address-space boundary — runs at 367 cycles for a one-way call on an Armv7 Cortex-A9, 413 cycles on an Armv8 Cortex-A57, and 718 to 771 cycles on x86-64 Haswell and Skylake parts, according to the sel4bench data the Foundation regenerates continuously. Independent measurement published at EuroSys 2019 put seL4’s round-trip IPC at 396 cycles on a Skylake i7-6700K, against 2,717 cycles for Fiasco.OC and 8,157 cycles for Google’s Zircon — a factor of 6.9 and 20.6 respectively. The fast path that produces those numbers is inside the proof.

The combination is what has kept seL4 relevant long past the usual half-life of an academic kernel. It is now in mass production in a Chinese electric vehicle, running the mission computer of a Boeing helicopter that a DARPA red team could not compromise, underpinning a commercial fleet-management platform out of New Zealand, shipping inside a German satellite computer, and being pushed toward datacentre-scale core counts by a startup that joined the seL4 Foundation in March 2026. Apple has been a Foundation member since April 2024 and is the gold sponsor of the 2026 summit, though it has published nothing about what it does with the kernel.

The period since late 2024 has been the most productive in the project’s history for reasons that have little to do with marketing. DARPA’s PROVERS programme and Germany’s Cyberagentur are both paying for proof work at industrial scale, and the results have arrived on schedule: functional correctness on AArch64 in April 2024, integrity on AArch64 in April 2025, verified configurations extended from three Arm platforms to all twenty-two by November 2025, a verified dynamic domain scheduler in June 2026, and — the largest single milestone in years — the completed functional-correctness proof for the mixed-criticality (MCS) configuration on 64-bit RISC-V on 29 June 2026, shipped in seL4 16.0.0 a month later.

This article works through all of it: what the proofs establish, what they assume, where they do not apply, how the performance numbers should be read, what the ecosystem above the kernel now looks like, who is deploying it and who quietly stopped, and which questions the evidence still cannot settle. The kernel is small. The story around it is not.

From L3 to seL4, three decades of L4 lineage

seL4 is the third generation of a microkernel family that starts with Jochen Liedtke’s L3 in the early 1990s, and understanding that lineage explains most of seL4’s design decisions. Liedtke’s argument, made against the prevailing view that microkernels were inherently slow, was that Mach’s poor performance was an implementation failure rather than an architectural one. His demonstration was L3 and then L4, hand-written in assembly, with inter-process communication one to two orders of magnitude faster than Mach’s.

The numbers from that era still anchor the field. Liedtke’s original L4 on a 50 MHz i486 DX cost 250 cycles for a one-way IPC, about 5 microseconds. By 1997 on a 160 MHz Pentium it was down to 121 cycles, roughly 0.75 microseconds — the figure that survives in folklore as “about a hundred cycles”. L4Ka::Hazelnut on a Pentium II managed 273 cycles; on a Pentium 4 the deep pipeline pushed it to 2,000. OKL4 on an XScale 255 came in at 400 cycles. NOVA on a Core i7 Bloomfield hit 288. seL4 on Haswell in 2013 measured 301 cycles one-way, and on an ARM11 just 188.

The lesson Liedtke’s successors extracted was minimality as a design principle, stated as a rule: a concept belongs in the kernel only if moving it outside would prevent the implementation of required system functionality. Everything else goes into user mode. That rule is why seL4 is small enough to verify. It was not adopted for verifiability — it predates the verification effort by a decade — but it turned out to be the precondition for it.

The second-generation L4 kernels, developed through the late 1990s and 2000s at Karlsruhe, Dresden and the University of New South Wales, worked through the problems the first generation left open. Liedtke’s assembly implementations were unportable and unmaintainable, so later kernels moved to C and C++ and discovered that careful C could match hand-written assembly on the critical path. The original IPC design mixed synchronous and asynchronous semantics awkwardly. Resource management was ad hoc, with the kernel allocating memory from its own pool — a design that makes both isolation guarantees and worst-case execution time analysis impossible.

seL4’s answer to that last problem is the single most consequential departure from its ancestors. The kernel allocates no memory after boot. All kernel objects are created from user-supplied memory, tracked through capabilities to untyped memory regions, and the retype operation that converts untyped memory into a typed kernel object is itself a capability invocation. This puts memory allocation policy entirely in user space, makes resource exhaustion a local rather than global failure, and gives the verification effort a bounded state space to reason about.

The commercial track record of the family matters for credibility. Open Kernel Labs, founded in 2006 as a NICTA spinout by Steve Subar and Gernot Heiser, shipped OKL4 on more than two billion mobile handsets, and an L4-derived kernel has run in the security processors of Qualcomm cellular modems in enormous volume. General Dynamics acquired Open Kernel Labs in September 2012 and in July 2014 announced it would make seL4 available as open source — the moment seL4 stopped being a research artefact. It is worth being careful here: the billions-of-devices figure belongs to OKL4 and other L4 variants, not to seL4 itself. seL4’s own deployment count is far smaller and concentrated in high-assurance niches. Confusing the two overstates seL4’s footprint by several orders of magnitude, and the seL4 project’s own whitepaper is careful about the distinction even when secondary coverage is not.

The capability model that sets seL4 apart

seL4’s access-control mechanism is a capability system, and the choice has consequences that reach into every part of the design, including the proofs. A capability in seL4 is an unforgeable token that combines a reference to a kernel object with a set of access rights over it. There is no ambient authority. Invoking a capability is the only way to perform any operation on any system object, without exception, and a thread’s capabilities are held in kernel-managed storage the thread cannot write to directly.

The contrast with access-control lists is not cosmetic. In an ACL system, the question “may this operation proceed?” is answered by looking up the identity of the requester and consulting a policy attached to the object. That indirection produces the confused deputy problem: a privileged service performing work on behalf of a less privileged client uses its own identity for the check, and so performs operations the client could not have performed itself. Every setuid vulnerability in Unix history is a variant of this. In a capability system the authority travels with the request. A client that wants a service to write to a file hands the service a capability to that file; the service has no other write authority to exercise, so it cannot be tricked into using authority it was never given.

Three properties of seL4 capabilities are load-bearing for the security proofs. Delegation with attenuation: a capability can be copied to another thread, and the copy can be minted with a reduced rights set, so authority can be passed on but never amplified. Revocation: capabilities are held in a derivation tree, and revoking a capability recursively removes every capability derived from it, which is what makes reclaiming resources from a compromised component possible at all. Transparent interposition: because a capability is just a reference, a component can be handed a capability to a monitor that in turn holds the capability to the real object, and the component cannot tell the difference. That is the mechanism behind virtualization, auditing and reference monitors on seL4, and it requires no kernel support beyond the capability abstraction itself.

Capabilities live in CNodes — kernel objects that are arrays of capability slots. A thread’s CSpace is a graph of CNodes reachable from its root, addressed by a bit-string that the kernel resolves by walking the graph, guard bits and all. It is closer to a page-table walk than to a file-descriptor table, and it means the shape of a component’s authority is a data structure the system designer lays out explicitly rather than something the kernel infers.

The relationship between capabilities and the proofs runs both ways. The integrity theorem is stated in terms of an access-control policy derived from the capability graph. The proof shows that after any kernel event, the resulting state differs from the previous state only in ways the policy authorises — and, separately, that the policy itself is invariant, meaning authority cannot spread beyond what the static policy permits without an explicit Grant right. Without a capability model there would be nothing that precise to state. A theorem about an ACL system would have to quantify over identities, policies and the code of every privileged service.

The cost of all this is conceptual load on the developer. seL4’s API is deliberately primitive — the project’s own documentation calls it “the assembly language of operating systems” — and building a working system directly on it means designing the entire capability layout, the object allocation plan and the communication topology by hand. That is what the frameworks discussed later in this article exist to absorb.

Ten object types and a deliberately primitive API

The whole seL4 kernel exposes ten object types, and the list is short enough to state in full: untyped memory, CNodes, thread control blocks, scheduling contexts, endpoints, reply objects, notifications, frames, address-space objects (page tables and page directories, architecture-dependent), and interrupt objects. Everything a system does on seL4 is expressed as invocations on capabilities to instances of those ten types.

Untyped memory is the root of all allocation. A capability to an untyped region can be retyped into any other object type, or split into smaller untyped regions, and the derivation tree records the relationship so that revoking the parent reclaims everything derived from it. Because the kernel never allocates, the total memory a subsystem can consume is fixed by the untyped capabilities it holds — a hard bound established at design time rather than a policy enforced at runtime.

Endpoints carry synchronous IPC. A send blocks until a receiver is ready and a receive blocks until a sender is ready, and the message is copied once, directly between the two threads, with no kernel-side buffering. Short messages travel entirely in registers. Longer messages use a per-thread IPC buffer, and seL4 15.0.0 added optional thread-local IPC buffers to give designers more control over that memory. Capabilities can be transferred through an endpoint if the sending capability carries the Grant right, which is the mechanism by which authority is handed between components at runtime.

Notifications carry asynchronous signals and behave as arrays of binary semaphores. A signal sets a bit; a wait blocks until any bit is set and then returns and clears the word. This is the mechanism drivers use to deliver interrupt notifications to user-level handlers, and it is what the device-driver framework builds its lock-free queue signalling on top of.

Reply objects and scheduling contexts are the newer additions, introduced with the MCS configuration. A reply object makes the right to reply to a call an explicit, transferable capability rather than an implicit kernel-managed state, which allows a server to hand a request off to another server and let that one reply directly. A scheduling context is a capability to processor time, carrying a budget and a period: the thread may execute for at most the budget within each period, regardless of its priority. That single mechanism is what makes seL4’s mixed-criticality story work, and it is why a low-priority untrusted component cannot starve a critical one and a high-priority component cannot monopolise the CPU.

Thread control blocks hold register state, priority, fault handler and CSpace/VSpace roots. Frames are physical memory regions that can be mapped into an address space with specified permissions and cacheability. Interrupt objects — an IRQControl capability that mints IRQHandler capabilities for specific interrupt lines — put interrupt routing under capability control, so which component may receive which interrupt is a design-time decision expressed in the capability graph.

The consequence of this minimalism is that seL4 provides no file system, no network stack, no device drivers, no process abstraction and no shell. It is not an operating system. It is the isolation and communication substrate on which an operating system can be built, and the project is explicit that most engineers should never write directly against the kernel API. What the API buys in exchange for its austerity is a specification small enough to be stated formally and an implementation small enough to be proven against it. Every abstraction the kernel does not provide is an abstraction that does not have to be verified — and, more importantly, an abstraction whose failure cannot take down the entire system.

The refinement chain from abstract spec down to C

The core seL4 proof is a refinement chain, and the structure is worth understanding because almost every claim and every limitation of seL4’s assurance story follows from it.

At the top sits the abstract specification: a non-deterministic model of the seL4 API written in higher-order logic, expressed in a state monad. It says what each system call is permitted to do without committing to how. Where the kernel is free to choose — which thread to schedule, where in a CNode to place a capability — the abstract spec leaves the choice open. This is the document against which security properties are stated, and it is the level a system designer reasoning about seL4’s behaviour should be reading.

Below that is the executable, or design, specification. This was derived from a literate Haskell prototype of the kernel, mechanically translated into Isabelle/HOL by a purpose-built translator. It fixes the data structures and algorithms — the actual scheduler queues, the actual capability derivation tree layout — while still abstracting away C-level detail such as pointer arithmetic and machine-word sizes. Writing the kernel first in Haskell and then in C was a deliberate methodological choice: the Haskell prototype could be executed against a simulated machine to shake out design errors before either the C code or the proofs existed.

At the bottom is the C implementation, parsed into Isabelle by a C parser written by Michael Norrish and represented in Simpl, a deeply embedded imperative language for Isabelle/HOL, over a typed-heap memory model developed by Harvey Tuch and colleagues. This is the real kernel — the same source that compiles and runs.

The proofs establish two refinement steps and get the third by transitivity. Theorem one: the executable specification refines the abstract specification. Theorem two: the C implementation refines the executable specification. Therefore the C implementation refines the abstract specification. Refinement here means forward simulation: every behaviour the lower level can exhibit is a behaviour the upper level permits. The practical reading is that any property proven about the abstract specification, if it is a property preserved by refinement, holds of the running C code.

Discharging those steps required proving and maintaining a very large set of invariants — properties of kernel state that hold before and after every kernel entry and that the correctness argument depends on. The invariant proof for the abstract specification alone took roughly eight person-years of the eleven that were seL4-specific. Invariants are where the real difficulty lives: the individual refinement obligations are mechanical, but establishing that a given invariant is preserved by every one of the kernel’s operations, in every interleaving of preemption points, is not.

Two tools deserve mention because they generalise beyond seL4. AutoCorres, built by David Greenaway, June Andronick and Gerwin Klein, is a proof-producing tool that abstracts the C parser’s Simpl output into readable monadic Isabelle — lifting local variables, rewriting exceptions, strengthening types. Measured on seL4 it cut the mean size of function terms by 53 per cent and successfully type-strengthened 96 per cent of 535 functions. And crunch, a small Isabelle tool for lifting invariant-preservation proofs across large families of similar lemmas, which is the sort of infrastructure that only exists because someone had to do this at scale.

One more layer sits above the kernel proofs and is often overlooked. capDL is a specification language for describing a complete system’s capability distribution, paired with a proved-correct user-level initialiser. It closes part of the gap between “the kernel is verified” and “this system is configured the way its designer intended” — because a verified kernel booted into a badly designed capability graph provides no security at all.

Taking the compiler out of the trusted computing base

The 2009 proof established that seL4’s C code implements its specification. That leaves an obvious question: the processor does not execute C. The functional-correctness proof assumed the compiler and linker translated the verified C faithfully, which put GCC — several hundred thousand lines of unverified, actively-developed software with a documented history of miscompilation bugs — squarely inside the trusted computing base of the world’s most carefully verified kernel.

Translation validation removed it. The technique, published by Thomas Sewell, Magnus Myreen and Gerwin Klein at PLDI 2013, does not verify the compiler. It verifies the output, for this specific program, on this specific compilation. Both the proven C and the compiled binary are translated into a common intermediate graph language with three node types — basic blocks, conditionals and calls — and the equivalence of the two graphs is then discharged function by function by SMT solvers. The binary side of the translation uses the Cambridge formal ARM instruction-set model in HOL4 together with Myreen’s decompilation-into-logic, so the machine semantics being reasoned about are themselves a formal artefact rather than a hand-written model.

The results on the original Armv7 kernel are concrete. At GCC 4.5.1 with -O1, the binary contained 11,736 instructions across 260 decompiled functions, of which 234 were proved equivalent in a total of 59 minutes — covering every function previously verified at the C level plus most of the initialisation code. Two solvers were used together: Z3 for speed on small problems and SONOLAR, slower but stronger on bitvector and array theories, which solved everything put to it while Z3 timed out on the larger cases. At -O2 the picture degraded sharply: 145 functions proved, 18 outright failures, 62 aborted, and four hours twenty-three minutes of solver time. Loops are handled by an n-ary induction rule plus a restriction rule to bound iterations, which is where most of the difficulty concentrates.

Two findings from that work are more interesting than the headline. First, no genuine compiler bugs were found — only small mismatches between C semantics and what the compiler actually did, which is a mildly reassuring result about GCC and a strongly reassuring one about the method. Second, making the proof go through required changing the kernel source: an enum was widened to uint32_t to eliminate struct padding, an array loop was restructured, and one function with repeated switches was reworked because it made the SMT solver diverge. Verification is not a passive audit. It shapes the code.

The method was extended to 64-bit RISC-V in May 2021 by Matt Brecknell and Zoltan Kocsis, funded by HENSOLDT Cyber — the first 64-bit architecture to get binary verification for seL4, with the main engineering difficulty being state-space growth relative to 32-bit Arm. On AArch64 and x86-64, binary verification does not exist. A team deploying seL4 on an AArch64 part is trusting its compiler in a way a team on Armv7 or RV64 is not, and that difference is rarely reflected in how seL4’s assurance is described in marketing material.

Twenty-one machine-interface functions are left abstract and are not covered by the binary proofs at all. The C subset the verification handles also excludes several constructs a normal C programmer uses without thinking: taking the address of a local variable, calls through function pointers, goto, switch fall-through, unions, and expressions with unspecified evaluation order. The kernel is written to avoid them.

Integrity, confidentiality and what availability really covers

Functional correctness says the kernel matches its specification. It does not, by itself, say the specification is any good. The security theorems are the answer to that, and they are separate proofs with separate assumptions and separate coverage across architectures.

Integrity was proved by Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein and published at ITP 2011. The statement is a Hoare triple over the kernel entry point: given that the kernel’s invariants hold, that the capability graph is consistent with an access-control policy, and that the currently running thread belongs to the subject the policy names, then after any kernel event the resulting state differs from the prior state only in ways the policy authorises. In plain terms: no component can write to state it lacks write authority over. Alongside it sits authority confinement — the theorem that the policy relation is itself invariant across kernel calls, so authority cannot leak to another subject without an explicit Grant. The two together cost about 10,500 lines of Isabelle and ten person-months.

Both theorems assume the policy is well-formed: no subject holds total authority over another, and there are no Grant edges between mutually distrusting labels. That is a real constraint on system design, not a technicality. A system whose capability distribution does not satisfy it gets no integrity guarantee, and nothing in the kernel enforces well-formedness — it is the designer’s obligation, which is exactly why capDL and the verified initialiser matter.

Confidentiality is the harder theorem and carries the heavier assumptions. Toby Murray and colleagues proved intransitive non-interference for seL4 at the IEEE Symposium on Security and Privacy in 2013: after any number of transitions, what a partition can observe depends only on the scheduler state and on partitions the information-flow policy permits to influence it. This covers in-kernel storage channels — the kernel cannot be used as a conduit to move information between partitions that policy says must not communicate.

The assumption list is long and every item is a design constraint. The system must be correctly initialised with a well-formed policy. The kernel must run a static, partition-based round-robin domain schedule — a change made to the kernel specifically to enable this proof, because a dynamically scheduled kernel is not deterministic from a partition’s point of view. Only timer interrupts may be enabled; user partitions receive no asynchronous interrupt delivery, so drivers must poll memory-mapped registers. No synchronous IPC between partitions. Static communication topology. DMA disabled. Deterministic user-space execution. Partitions may observe global time, and the schedule is treated as public. The proof cost 27,756 lines of Isabelle over roughly 51 person-months.

That configuration is austere enough that few production systems match it exactly, and this is where the honest reading of seL4’s confidentiality story sits. The theorem is real and it is the strongest information-flow result for any kernel implementation. It also describes a specific, restrictive operating mode. Deployments that enable device interrupts, run dynamic schedules or permit cross-partition IPC — which is nearly all of them — are outside its scope. A significant caveat was eased on 1 June 2026, when Proofcraft delivered a verified dynamic, semi-static domain scheduler under RFC-20, shipped in seL4 15.0.0: the schedule no longer has to be compiled into the kernel and phase changes are now possible within the verified envelope.

Availability is the least discussed of the three and the most often misdescribed. It is bundled with the access-control proofs and it means that a subject cannot deprive another of resources it holds authority over — no unauthorised revocation, no unauthorised deletion, no unauthorised interference with another partition’s allocation under the domain schedule. It is a safety property, not a liveness or timeliness guarantee. Nothing in the availability theorem promises a deadline will be met. That assurance comes from worst-case execution time analysis and the MCS scheduling model, which are separate work entirely.

The assumptions, stated plainly

seL4’s project documentation maintains an explicit list of what the proofs assume, and reading it is the fastest way to calibrate expectations. The list is unusually candid for a security product, and the candour is itself part of the assurance argument: a proof whose assumptions are hidden is worth less than a proof whose assumptions are enumerated.

Assembly code. Roughly 340 lines of Arm assembly, with comparable amounts on other architectures, are assumed correct. They are not covered by the C proof and not covered by the binary proof. They handle kernel entry and exit, context switching and hardware register manipulation — precisely the code where a defect would be most consequential.

Hardware. The CPU and MMU are assumed to behave according to their specification, to be free of tampering, and to be operated within their physical envelope. Every hardware erratum, every fault-injection attack, every glitching technique and every case of a processor doing something its manual does not describe falls outside the proof. Given the rate at which speculative-execution and microarchitectural defects have been disclosed since 2018, this is not a small assumption.

Hardware management. Cache consistency, cache colouring and TLB management are assumed to be correctly implemented in assembly and to behave as advertised without affecting kernel semantics. Virtual-memory invariants are machine-checked, but the argument that the proof identified all the conditions those invariants need relies on informal reasoning.

Boot code. Roughly 1,200 lines of kernel initialisation code are excluded. The proof begins with the kernel already loaded and in a consistent initial state. Getting to that state — the bootloader, the early platform setup, the construction of the initial capability space — is unverified.

DMA. The proof assumes the CPU and MMU are the only devices that access memory directly. A DMA-capable device driven by an untrusted driver can write anywhere in physical memory unless an IOMMU or system MMU constrains it, and device address translation is not verified in any seL4 configuration. On most embedded Arm platforms there is no IOMMU to configure in the first place. In practice this means device drivers with DMA capability must be treated as trusted, or the hardware must provide translation that the system designer configures correctly and unverifiably.

Information side channels. For the confidentiality proofs, the assumption is that the binary-level hardware model captures all relevant channels. The documentation states outright that this is known to be false: timing channels are not covered.

Logic and tools. The consistency of higher-order logic’s axioms and the correctness of Isabelle’s LCF-style proof kernel are assumed. This is the weakest link in principle and the strongest in practice — Isabelle’s kernel is small, heavily scrutinised, and can export proof terms for independent re-checking.

Beyond that list, three exclusions apply across every verified configuration: device address translation (IOMMU and SMMU), debug, profiling and printing interfaces, and kernel startup. And the C and binary semantics both presume immutable program text, which rules out self-modifying code and, more subtly, means anything that rewrites kernel text at runtime is outside the model.

None of this undermines the proof. It bounds it. The correct way to use seL4 is to read this list as a specification of what the system designer still has to handle — and to notice that most of the items are things a conventional kernel does not address either, with the difference that a conventional kernel also does not address the things seL4 proves.

The verified configuration matrix, architecture by architecture

“seL4 is verified” is a statement about a specific kernel configuration on a specific architecture, and the differences across the matrix are large enough to change procurement decisions. The Foundation publishes the matrix, and it should be read directly before any claim is made in a safety case.

Verified properties by architecture, as of August 2026

The matrix is the single most important document for anyone building an assurance argument on seL4, and its unevenness is the point: the strongest configuration is 32-bit Arm, the newest is AArch64, and x86-64 has functional correctness and nothing else.

Armv7 AArch32 remains the most completely verified configuration. It is the only one with functional correctness, a verified fastpath, binary verification and both security theorems. It is also 32-bit, which increasingly disqualifies it from new designs.

AArch64 is where the momentum is. Functional correctness completed in April 2024, funded by the UK’s National Cyber Security Centre and executed by Proofcraft, and the integrity proof followed on 29 April 2025 — notable because it was the first seL4 security theorem to include hypervisor mode (EL2) and the floating-point unit. Every prior security proof covered a configuration without either. Confidentiality on AArch64 is in progress. Binary verification is not, so the compiler remains trusted on the architecture most new deployments target.

RISC-V RV64 is the most complete 64-bit story. Functional correctness landed in June 2020, translation validation to the binary in May 2021 (funded by HENSOLDT Cyber), integrity in July 2021 and confidentiality in December 2021 — a full sweep of the classic properties on a 64-bit architecture. It is also where the MCS functional-correctness proof was completed first, on 29 June 2026. The trade-off is that RV64 has no verified fastpath, which is visible in the benchmarks: 680 cycles for a one-way IPC call on a 1.5 GHz SiFive U54-MC, against 413 on a 1.9 GHz Cortex-A57.

x86-64 is the weakest verified configuration and the one most likely to be misrepresented. Functional correctness was completed on 30 July 2018 at the C level, explicitly excluding the fastpath, VT-x, VT-d, binary verification and all security theorems. Anyone planning an x86-64 seL4 deployment on the strength of “seL4 is formally verified” is relying on a proof that covers considerably less than the phrase implies. The point was underlined in seL4 16.0.0, which fixed a VM-escape defect in the x86-64 VMX restore path where a cooperating malicious VMM and guest could cause the kernel to jump to a user-controlled address on VM-entry failure, yielding arbitrary kernel-mode execution. That code is in an unverified configuration. The proof did not miss it; the proof was never applied to it.

From three verified platforms to all twenty-two

For most of seL4’s history, verification applied to a handful of specific boards. A verified configuration is a verified configuration — pinned to a platform’s memory layout, its interrupt controller, its cache geometry, its timer. Move to a different SoC and the proof did not automatically follow. That gap between “seL4 is verified” and “seL4 is verified on the board I am shipping” was, for years, the most practically limiting fact about the project.

It closed remarkably fast. At the seL4 Summit in Prague in September 2025, Gerwin Klein presented work titled after Guy Steele’s famous paper — “the next 700 verified seL4 platforms” — reporting that the proportion of supported Arm platforms with a verified configuration had gone from 13 per cent to 90 per cent in a single year, and, critically, that the marginal verification cost of adding a new platform had been driven to approximately zero. A twenty-third platform added during the work required no additional proof effort at all. seL4 14.0.0, released 25 November 2025, states that all Arm platforms supported by seL4 now have a verified configuration — twenty-two platforms, one hundred per cent.

The method was generalisation and automation rather than repetition. Instead of re-running platform-specific proofs, the work identified what platform parameters the proofs actually depend on, parameterised the proofs over them, and built the infrastructure to discharge the platform-specific obligations mechanically. This is proof engineering as software engineering: refactoring for reuse, then automating the residue.

The verified Arm list now covers hardware engineers actually buy. On AArch32: BeagleBoard and BeagleBone, Jetson TK1, Odroid-XU and XU4, Raspberry Pi 3B, Sabre Lite (i.MX6), Zynq ZC706, ZCU102 and ZCU106, and i.MX8M Mini. On AArch64: MaaXBoard, Odroid-C2 and C4, ROCKPro64, Raspberry Pi 4B and 5B, Rock3b, STM32MP25-EV1, TQMa8XQP, Jetson TX1 and TX2, Ultra96v2, ZCU102 and ZCU106, and the i.MX8M Mini, Plus and Quad plus the i.MX93 EVK. RISC-V verification remains anchored to the HiFive Unleashed; x86-64 to the generic PC99 configuration.

The ambition stated for DARPA’s PROVERS programme goes considerably further: extending verification to more than 10^12 configuration combinations. That number is not a count of boards. It is the combinatorial space of build options, feature flags, platform parameters and configuration choices that a real deployment selects from, and the goal is to make verification hold across that space rather than at a few pinned points within it. Whether it is achievable at that scale is an open question, but the 13-to-90-per-cent result in a year suggests the approach is not merely aspirational.

The practical consequence for engineering teams is straightforward and easy to miss: the answer to “is seL4 verified on my board?” changed from “probably not” to “on Arm, yes” between late 2024 and late 2025. Any evaluation done before that period is out of date on the single question most likely to have blocked adoption.

Mixed criticality and the first verified MCS kernel

The problem MCS solves is the one that pushes most embedded systems toward federated architectures with separate processors per function: how do you run a safety-critical component and an untrusted one on the same core without the untrusted one being able to affect the critical one’s timing?

The conventional answer is time and space partitioning — fixed slots, statically allocated, of the kind ARINC 653 specifies for avionics. It works and it is certifiable, and it wastes a great deal of processor time, because a slot reserved for a worst case that rarely occurs sits idle the rest of the time. On modern multi-function systems the waste compounds.

seL4’s answer is scheduling-context capabilities, published by Anna Lyons, Kent McLeod, Hesham Almatary and Gernot Heiser at EuroSys 2018. Processor time becomes a first-class object under capability control. A scheduling context carries a budget — how long a thread may run before preemption — and a period — how often that budget refreshes. A thread without a scheduling context capability cannot run at all. The pairing of budget and period bounds a component’s CPU consumption independently of its priority, which is the property that makes co-location safe: a high-priority thread that misbehaves exhausts its budget and stops, rather than starving everything below it.

Two further mechanisms complete the model. Passive servers hold no scheduling context of their own and run on the client’s, so a shared service cannot be used as a channel for stealing time — the client pays for the work it requests. And timeout faults give a designated handler control when a thread exhausts its budget, which is what makes recovery policies expressible rather than merely hoped for.

Verifying all this took a long time and the reason is structural. The Foundation describes MCS as “the largest new seL4 feature,” involving “wide-ranging changes to the kernel’s implementation,” and its refinement proof as “the largest and most central proof in the seL4 verification stack.” Scheduling touches everything. Making time a capability-controlled resource changes the kernel’s invariants, the shape of the scheduler, the semantics of IPC (reply objects exist because of it) and the structure of the refinement argument.

The work was led by Michael McInerney at Proofcraft, presented in progress at the 2022, 2024 and 2025 summits, and committed as a DARPA PROVERS deliverable on 2 December 2024. The framework work behind it was funded in part by a donation from XCalibyte in November 2023. On 29 June 2026 the functional-correctness proof for MCS seL4 was completed on 64-bit RISC-V — the first time any MCS configuration of seL4 had been verified — and reported in the seL4 16.0.0 release on 22 July 2026.

Two limits matter for anyone reading that milestone as a green light. The port to AArch64 is next, not done, and it is the architecture most production deployments target. And the MCS security proofs — integrity and confidentiality under the MCS configuration — do not exist on any architecture yet. A team running MCS on AArch64 today is running an unverified configuration of a feature whose verification exists only on a different architecture. That is still a materially better position than any competing kernel offers, and it is not the same as verified.

Worst-case execution time and the hard real-time claim

Formal correctness and timeliness are different properties, and a kernel can have one without the other. For hard real-time certification, the question is not whether the kernel behaves correctly but whether an upper bound on how long it takes can be established and trusted.

seL4 has one. Bernard Blackham, Yao Shi, Sudipta Chattopadhyay, Abhik Roychoudhury and Gernot Heiser, and later Thomas Sewell, Felix Kam and Heiser at RTAS 2016, produced a complete and sound worst-case execution time analysis of seL4 — the project’s claim, which has not been publicly contradicted, is that it remains the only such analysis for a protected-mode operating system. The output is a provable upper bound on the latency of every system call.

Getting there required changing the kernel. Two design decisions in classical L4 kernels are incompatible with bounded latency, and seL4 abandoned both.

Lazy scheduling was one of Liedtke’s original optimisations: when a thread blocks in IPC, leave it in the ready queue and let the scheduler clean up later. It saves queue manipulation on the hot path. It also means the scheduler’s execution time is bounded only by the total number of threads in the system, because it may have to skip an arbitrary number of blocked entries before finding a runnable one. For a WCET analysis, that is fatal. seL4 replaced it with an invariant-based scheme sometimes called Benno scheduling, where queue membership is maintained eagerly and the scheduler’s work is bounded.

Long-running operations were the other. Some kernel operations — recursive capability revocation being the canonical case, since it can walk an arbitrarily large derivation tree — cannot complete in bounded time. seL4 handles them with incremental consistency: the operation is broken into short sub-operations, each of which leaves kernel state consistent, with a preemption check between them. If an interrupt arrives, the kernel returns to user level with the operation partially complete and restartable. This bounds interrupt latency without requiring the kernel to be fully preemptible, which would have made the verification substantially harder.

The practical caveats bite hard. WCET analysis is architecture- and platform-specific, and the published sound analysis was done on Armv6 and Armv7-class hardware with relatively simple, analysable microarchitecture. On a modern out-of-order core with deep speculation, multiple cache levels, hardware prefetchers and shared interconnect, sound WCET bounds get much harder and much looser — a problem the whole real-time community faces, not one specific to seL4. Current work on WCET for the 64-bit RISC-V MCS kernel uses the Heptane analysis tool, and is part of the LionsOS verification roadmap rather than a completed result.

What the analysis buys is a prerequisite for certification rather than certification itself. A safety case for a hard real-time system needs a defensible bound on kernel latency, and seL4 can supply one on the platforms where the analysis has been done. That is not the same as being able to supply one on any platform a team might choose.

Reading the IPC numbers properly

seL4’s performance claim is narrow and specific: it is about inter-process communication cost, measured in processor cycles, on a single core, between address spaces. That metric matters more for a microkernel than for a monolithic kernel because in a microkernel-based system every service invocation — every file read, every network send, every driver interaction — crosses an address-space boundary. IPC cost is the tax on the entire architecture.

The Foundation publishes sel4bench results continuously, and the numbers below were generated on 22 July 2026 with the fastpath enabled. These are one-way costs in mean cycles.

On Armv7 Cortex-A9, i.MX6 Sabre at 1.0 GHz: IPC call 367, IPC reply 352, notify 1,022, IRQ invoke 771. On Armv8 Cortex-A57, Tegra X1 at 1.9 GHz: call 413, reply 426, notify 1,067, IRQ 885. On x86-64 Haswell i7-4770 at 3.4 GHz: call 771, reply 642, notify 1,490, IRQ 1,644. On Skylake i7-6700 at 3.4 GHz without Meltdown mitigation: call 718, reply 576, notify 759, IRQ 1,652. On RV64 SiFive U54-MC at 1.5 GHz: call 680, reply 719, notify 1,188, IRQ 800.

Round-trip cost is approximately call plus reply — around 719 cycles on the Sabre, 839 on the A57, 1,413 on Haswell, and 1,294 on Skylake without Meltdown mitigation. The MCS configuration costs slightly more on some operations and noticeably more on others: notify and IRQ invoke on RV64 under MCS jump to 3,948 and 3,609 cycles respectively, which is a large enough regression that anyone counting on RISC-V MCS notification performance should measure it themselves.

The headline comparative claim originates in Heiser and Elphinstone’s twenty-year retrospective on L4 microkernels in ACM TOCS in 2016: typical L4 implementations have IPC costs only 10 to 20 per cent above the hardware limit, where the hardware limit is defined as two mode switches, a page-table switch, and saving and restoring the addressing context and user-visible processor state. That definition is what gives the claim content — it is a statement about how little the kernel adds to what the processor unavoidably costs, not a vague assertion of speed.

The strongest independent comparison comes from Mi, Li, Yang, Wang and Chen’s SkyBridge paper at EuroSys 2019, which measured round-trip single-core IPC on a Skylake i7-6700K across three microkernels: seL4 at 396 cycles, Fiasco.OC at 2,717, and Zircon — the Fuchsia kernel — at 8,157. That is 6.9× and 20.6× slower than seL4 respectively. It is third-party data collected by researchers building a competing IPC mechanism, which makes it more credible than vendor benchmarking.

Two cautions. First, the 396-cycle SkyBridge figure and the roughly 986-cycle figure the LionsOS team uses as their x86 baseline are both “seL4 round-trip on Skylake-class hardware” and they differ by a factor of 2.5, because configuration and measurement harness differ. Do not mix figures across sources. Second, there is no rigorous published head-to-head against QNX or Linux. A frequently-cited mailing-list measurement suggesting QNX beats seL4 was taken inside VirtualBox and implies per-call costs of 12,000 to 50,000 cycles for seL4 — an order of magnitude away from native measurement — and Heiser rejected it on methodology. His counter-claim, that QNX IPC costs many thousands of cycles, is plausible and also unsourced. The honest position is that seL4’s advantage over other microkernels is well documented and its comparison against commercial RTOSes is not.

The fastpath, and why speed did not cost assurance

The reason seL4’s IPC numbers look the way they do is a fastpath: a hand-optimised code path taken when a set of conditions all hold, falling back to the general implementation when any of them does not.

The conditions are restrictive. The receiver must already be blocked waiting on the endpoint. The receiver must be immediately runnable under the current scheduling discipline, so that a direct switch does not violate priority. The message must fit in registers. There must be no capability transfer, no fault, no error condition. Every validity check must pass. If any condition fails, the slowpath handles it, correctly and more slowly.

The payoff is large. Bernard Blackham and Gernot Heiser measured it at APSys 2012 on an ARM11 core, running 160,000 ping-pong iterations of a zero-length one-way IPC: the slowpath cost 1,776 cycles; the original fastpath 308; a carefully hand-optimised C fastpath 200 cycles. Their paper’s actual finding, and the one that matters for this article’s argument, is that an assembly implementation of the same fastpath also measured 200 cycles. Careful C matched hand-written assembly. There was no performance reason to leave the hot path outside the verified language.

Four mechanisms produce the speed. Register-based transfer: short messages travel entirely in physical registers, never touching memory. Single copy: at most one copy, sender to receiver, with no kernel-side buffering — the kernel does not have a message queue for the fast case because there is nothing to queue. Direct process switch: the kernel identifies the runnable partner and switches to it without invoking the scheduler, running it on the sender’s remaining time slice. Minimal validation: the checks are ordered so that the common case exits early.

The point that deserves emphasis is that the C fastpath is inside the functional-correctness proof. It is machine-checked to refine the abstract specification. The assembly variant Blackham and Heiser wrote for comparison is not verified and is not used. This inverts the usual expectation about high-assurance software: the performance-critical path is not an unverified escape hatch bolted onto a verified core. It is verified. Whatever else is true of seL4’s assurance story, the speed and the proof cover the same code.

The fastpath is not uniformly available, and this is where the matrix matters again. RV64 and x86-64 have no verified fastpath at all, which explains why RV64’s 680-cycle IPC call on a 1.5 GHz part compares unfavourably with AArch64’s 413 cycles at 1.9 GHz once clock rates are accounted for. seL4 13.0.0 added signal and VM-fault fastpaths on AArch64, extending the technique beyond plain IPC. On Armv7 and AArch64 the fastpath is verified; elsewhere the performance the benchmarks show and the assurance the proofs provide are not describing the same configuration, which is a subtlety that vanishes from most summaries of seL4’s capabilities.

Timing channels, the hole the proofs leave open

The single most important limitation of seL4’s assurance is that the confidentiality proof does not cover timing channels, and the project says so explicitly.

The reason is structural rather than an oversight. The information-flow proof reasons about the kernel’s state as the ISA defines it: registers, memory, architectural state. Microarchitectural state — cache lines, TLB entries, branch predictor history, prefetcher state, store buffers — sits below that abstraction and does not appear in the model. Two partitions that the proof shows cannot exchange a single bit through kernel storage can still communicate at measurable rates by modulating shared cache occupancy and observing each other’s execution time. The documentation’s own wording on the assumption that the hardware model captures all relevant channels is that “we know this not to be the case.”

Spectre and Meltdown in 2018 turned this from an academic concern into a practical one. Those attacks work precisely by using microarchitectural state to observe things the architectural model says are unobservable, and no proof stated over the architectural model can rule them out. seL4’s response was not to claim the proofs covered it. It was to treat timing channels as a separate research problem requiring new mechanisms and, eventually, new proofs.

The measurements make the scale concrete. Qian Ge, Yuval Yarom, Tom Chothia and Gernot Heiser’s EuroSys 2019 paper measured a last-level cache channel through the shared kernel at 0.79 bits per 2 milliseconds — roughly 395 bits per second between partitions that the information-flow policy prohibited from communicating. A cache-flush channel on Arm carried 1.4 bits. An interrupt-based channel carried 0.9 bits per timeslice. None of these are theoretical; all were measured on real hardware running a correctly configured seL4 system with the confidentiality proof’s guarantees nominally in force.

Four hundred bits per second is more than enough to exfiltrate a cryptographic key from a partition designed to protect it. For most seL4 use cases — a flight controller isolated from a camera subsystem, a vehicle’s safety functions isolated from infotainment — a low-bandwidth channel is a manageable risk, because the attacker’s goal is usually control rather than covert data extraction. For cross-domain solutions handling classified data at different levels, which is one of seL4’s flagship applications, a 400-bit-per-second channel is a serious finding.

The kernel is also not the only sharing point. Cores sharing a last-level cache, memory controllers, interconnects and DRAM banks all provide channels that no operating system can partition, because the hardware does not expose the controls. Ge and colleagues are explicit that interconnects and buses are fundamentally unpartitionable with current hardware. Some channels are closable by software; some require hardware that does not exist in mainstream processors.

There is one more piece of intellectual honesty in the seL4 literature worth noting. The 2013 confidentiality proof models time coarsely, treating the passage of time as something partitions can observe and treating the schedule as public. That is not an accident of formalisation; it is an acknowledgement that the proof deliberately does not attempt to reason about timing, and that a proof which did would need a fundamentally different model of the machine.

Time protection as a first-class operating-system abstraction

The seL4 group’s response to timing channels is an argument that operating systems have been missing an abstraction. Memory protection is universal and well understood. Time protection — preventing interference through the timing of shared resources — has no equivalent, and Ge, Yarom, Chothia and Heiser’s EuroSys 2019 paper, which won best paper, argues it should.

The mechanisms are concrete. Spatially partition physically-indexed state through cache colouring: allocate cache sets to partitions so they cannot evict each other’s lines. On Haswell this yielded 8 colours for L2 and 32 for the last-level cache. Temporally partition virtually-indexed on-core state by flushing it on domain switch: on Arm, L1 data and instruction caches, the TLB and the branch predictor; on x86, invpcid, indirect branch control, and a manual L1 flush performed by loading a buffer, because x86 provides no L1 flush instruction. Clone the kernel: give each domain its own copy of the kernel image, so that no kernel text, data or stack is shared and the kernel itself stops being a channel. Pad the domain switch to its worst-case latency deterministically, so the switch duration carries no information. Partition interrupts by binding IRQ handler capabilities to a kernel instance.

The costs are modest and were measured. Domain switch with time protection costs around 30 microseconds on x86 and 27 to 31 on Arm — about 0.3 per cent of a 10-millisecond timeslice. IPC changed by between −1 and +1 per cent on x86 but rose 13 to 15 per cent on Arm, because the extra kernel mappings thrash a two-way L2 TLB. Splash-2 benchmarks at 50 per cent cache colours slowed by 2.76 per cent on average and 10.96 per cent worst case on x86, and 0.75 and 6.73 per cent on Arm. Padding added half a per cent. Worst-case full-hierarchy flush latencies are the ugly numbers: 520 microseconds on x86 and 1,150 on Arm, against 27 and 45 for L1 alone.

The channel results are what justify the effort. The last-level cache channel through the shared kernel dropped from 0.79 bits per 2 ms to 0.6 millibits. The Arm cache-flush channel went from 1.4 bits to immeasurable. The interrupt channel fell from 0.9 bits per timeslice to 0.5 millibits. A cross-core last-level-cache side channel against an ElGamal implementation was eliminated. One residual channel of about 50 millibits survived, through the x86 L2 data prefetcher, whose state cannot be flushed by any available instruction.

Whether time protection can be proved is the harder question. Heiser, Klein and Murray argued at HotOS 2019 that it can, by modelling the advance of time as a deterministic but unspecified function over an abstract microarchitectural state, which reduces timing reasoning to storage-channel reasoning given constant-time domain switches. The catch is that this requires an augmented ISA — a hardware-software contract in which every shared microarchitectural resource is either partitionable or flushable. Mainstream processors do not satisfy it. Bandwidth is not partitionable, hyperthreading shares state that cannot be separated, and the prefetcher residual is exactly the kind of gap the contract would have to close.

Progress since then is real but incomplete. Robert Sison and colleagues published a machine-checked Isabelle formalisation of time protection at FM 2023, casting it as a dynamic, observer-relative intransitive nonleakage property and demonstrating that conventional information-flow theories are insufficient for it. On the hardware side, a fence.t instruction — a single instruction that resets on-core temporal state — was developed with ETH Zurich’s PULP group and won best paper at DATE 2021, with a formal verification of an implementation done with PlanV. Work continues at UNSW under Cyberagentur’s PISTIs-V project, restarted in January 2025, with several 2025 honours theses on address bounding and cross-domain notification. The Foundation’s whitepaper states plainly that time protection is not currently covered by the proofs and calls it a major unsolved research problem. That is the accurate status as of August 2026.

Microkit and the retreat from CAmkES

The seL4 API is too low-level to build systems against directly, and for a decade the standard answer was CAmkES — the Component Architecture for Microkernel-based Embedded Systems. CAmkES gives you an architecture description language for components, interfaces and connectors, and a generator that emits the glue code and the capability distribution. It works, it is still maintained and released in lockstep with the kernel, and a great deal of production seL4 work rests on it, including the DARPA HACMS mission computer and much of the defence ecosystem’s tooling.

It is also being superseded, and the reasons are stated bluntly in the seL4 community’s own literature: too complex, too static in the wrong ways, and maintenance-intensive. CAmkES generates a lot of code, its abstractions are numerous, and it never had a distributable SDK, which means getting started required building the world.

seL4 Microkit is the replacement, and the design philosophy is subtraction. It was developed by Ben Leslie’s Breakaway Consulting under a grant from Australia’s Department of Defence with Trustworthy Systems as partner, adopted as an official Foundation project on 20 November 2023, and given its first Foundation release as version 1.3.0 on 1 July 2024. The current release is 2.3.0, shipped alongside seL4 16.0.0 in July 2026.

Microkit has four abstractions and that is the entire model. A protection domain is a single thread of control in a fixed address space, with its own capability space, scheduling context and notification object. A channel connects exactly two protection domains. A memory region is a memory range mappable into one or more domains with specified permissions and caching. A protected procedure call is a synchronous call carrying up to 64 words, permitted only toward higher-priority domains — a restriction that makes deadlock structurally impossible rather than a thing to be careful about.

The limits are deliberately tight: at most 63 protection domains per system, 63 channels per domain, priorities from 0 to 254. Each domain has up to four entry points — init, notified, an optional protected for handling incoming calls, and fault for supervising children and virtual machines. The whole system is described in a single XML system description file listing domains, memory regions, mappings, channels, interrupts and virtual machines, and the Microkit tool turns that plus the compiled domain binaries into one bootable image. The SDK ships prebuilt kernel images per board, libmicrokit.a, a loader and monitor, examples and a manual, for Linux and macOS on both x86-64 and AArch64.

Microkit 2.3.0’s additions show where the framework is heading: IOMMU on by default on x86-64, virtual machine stop and start, capability sharing so a domain can be granted access to specific thread control blocks and scheduling contexts (which enables user-space schedulers), seL4 domain-scheduler support, per-domain FPU control, hardware debug on most x86-64 and AArch64 platforms, and experimental Viper verification integration.

Microkit is also being verified, and the approach is different from the kernel’s. Rather than interactive theorem proving, the team built a push-button tool called Gordian that translates the specification through Haskell and Python into SMT-LIB2 and discharges it with Z3, exploiting Microkit’s atomic-execution guarantee to avoid concurrency reasoning entirely. Functional correctness of six core libmicrokit functions and correctness of system initialisation via capDL generation are done, and the whole verification runs in about twenty seconds on a desktop. Outstanding: the end-to-end proof chain, MCS support and 64-bit support — the published report covers a non-MCS 32-bit configuration.

LionsOS and the claim that verified systems outrun Linux

Microkit gives you a way to structure a system. LionsOS is an argument about what that system should look like, and it comes with the most aggressive performance claim in the seL4 ecosystem: that a statically-architected, use-case-specific operating system on a verified microkernel beats Linux on throughput, latency and CPU cost at the same time.

LionsOS is built by Trustworthy Systems at UNSW Sydney, led by Gernot Heiser, funded by Germany’s Cyberagentur, DARPA PROVERS through the INSPECTA team, and the UNSW John Lions Fund. It is BSD-licensed. The first release, 0.1.0, appeared on 16 April 2024; the current tagged release is 0.3.0 from 25 March 2025, adding file-system support and metaprogramming tooling. The project states plainly that it is not expected to be stable yet, and the git main branch is well ahead of the tagged releases.

The design philosophy is called radical simplicity and rests on four principles. Strict separation of concerns: one purpose per module, with policy fully contained inside a module rather than smeared across the system. Least privilege, enforced by the capability layout rather than by convention. Design for verification: narrow interfaces, sequential single-threaded event-driven code, because that is what current verification technology can handle. And use-case-specific policies instead of general-purpose ones — the observation that a general-purpose OS spends enormous complexity on being adequate for every workload, and a system that only has to serve one workload can be both simpler and faster.

The performance results, from the team’s paper published in January 2025 and revised in May, were measured on an Avnet MaaXBoard (NXP i.MX8MQ, four Cortex-A53 at 1 GHz, on-chip gigabit NIC) and an Intel Xeon W-1250 with a 10-gigabit Intel X550, hyperthreading and turbo disabled.

On Arm at 1 Gb/s, single core, UDP echo: LionsOS saturates the full gigabit with roughly 10 per cent CPU headroom remaining, while Linux plateaus around 600 Mb/s with the core maxed out. LionsOS uses just over half the CPU of Linux for the same load. With SMP, LionsOS handles full load with just over one core; Linux cannot handle full load even at its maximum of 1.4 cores.

On x86 at 10 Gb/s, single core: LionsOS sustains applied load up to about 6 Gb/s and peaks near 7 Gb/s, with CPU saturating around 4 Gb/s, while Linux collapses from 3.5 Gb/s down to under 2 Gb/s at maximum applied load. Round-trip latency is the more striking result: LionsOS stays under 200 microseconds until load exceeds 6 Gb/s; Linux sits at roughly 1,000 microseconds flat across the entire range — half to a full order of magnitude worse.

The team also ran an experiment that directly tests whether IPC cost is load-bearing, by artificially padding seL4’s IPC to simulate other kernels using the SkyBridge measurements. Against a 986-cycle seL4 baseline, adding 865 cycles per call to simulate Fiasco.OC measurably reduced throughput, and adding 3,585 to simulate Zircon dropped throughput to about two-thirds of seL4’s. The performance of the kernel’s IPC path shows up directly in application-level throughput, which is the empirical justification for caring about cycle counts at all.

Code size is the other half of the argument. The i.MX8 gigabit Ethernet driver is 569 lines in LionsOS against 4,775 in Linux — a factor of 8.4. The x86 ixgbe 10-gigabit driver is 668 lines against 3,019, a factor of 4.5. The serial driver is 249 lines. The team notes, pointedly, that the first driver written to the LionsOS model was implemented by a second-year undergraduate less than eighteen months after she wrote her first program.

Two demonstrators show the model working. The “Kitty” point-of-sale system combines native drivers for serial, timer, Ethernet and I²C, Python business logic on MicroPython, lwIP networking, NFS storage, and a Linux driver VM for graphics — roughly 2,100 lines of trusted code alongside 66,000 lines of untrusted libraries that cannot break isolation. And the LionsOS web server serves sel4.systems in production, with 3,545 lines of trusted code across thirteen modules averaging 270 lines each, against 62,356 lines of untrusted code and MicroPython’s own 402,554. A runtime policy swap — replacing a bandwidth-monitoring transmit policy with a bandwidth-limiting one — takes 17 microseconds.

The first commercial adoption of LionsOS was announced in January 2026.

Drivers, sDDF and the 569-line Ethernet controller

The reason LionsOS drivers are an order of magnitude smaller than Linux drivers is the seL4 Device Driver Framework, and the mechanism is worth understanding because it is the clearest example of what architectural discipline buys in a microkernel system.

A Linux driver is large because it does many things: it handles the device, it multiplexes between clients, it manages DMA buffers, it implements policy about queueing and buffering, it deals with cache coherence, and it lives inside the kernel where a defect is fatal. sDDF splits all of that apart. A driver in sDDF is a single-threaded schedulable entity that talks to one device and does nothing else. Multiplexing between clients, address translation, cache management and traffic shaping all move into separate components called virtualisers. Policy moves out of the driver entirely.

Data movement is zero-copy through bounded single-producer single-consumer lock-free queues in shared memory, with notification via seL4 notification objects — the signalling protocol having been model-checked rather than argued about. Memory is split into three strictly separated kinds of region: data regions holding DMA buffers, metadata regions holding the queues, and control regions. The design decision that does the most work is that drivers have no access to the data region at all. A driver hands the device a buffer address and gets a completion; it never reads or writes payload. A compromised driver therefore cannot read the data flowing through it, which is a property no monolithic driver model can offer.

Transmit and receive paths are fully separate, with four queues per Ethernet path — active and free queues in each direction. Three strategies exist for receive data regions, trading isolation against overhead: a single global region mapped per client (lowest overhead), a shared read-only region, or explicit copier components giving full isolation at the cost of a copy.

The performance figures track LionsOS’s. On a single Arm core with a gigabit NIC, sDDF saturates the link at about 65 per cent CPU utilisation, while Linux maxes out the core at roughly 500 Mb/s applied load. The example Ethernet driver is under 600 lines against roughly 5,000 for the Linux driver for the same silicon.

Device coverage has grown steadily through releases 0.2 in October 2022 to 0.6.0 in March 2025. Native drivers exist for serial, timer, clock, pin multiplexing, I²C, SPI, Ethernet, SDHC block storage and NFC card readers, with a subset available on x86 and RISC-V, and Rust drivers now supported. For device classes where writing a native driver is impractical — GPU, sound, video capture — the framework uses a Linux driver VM: a virtualised Linux instance whose only job is to run the vendor driver, exposed to the rest of the system behind an sDDF interface. This is the pragmatic escape hatch that makes the model deployable, and it is honest about the trade: the Linux VM is untrusted, contained, and its failure degrades one device class rather than the system.

A related effort deserves mention. Pancake is a verification-friendly systems programming language built on the CakeML verified compiler stack, developed at UNSW. Performance is within 15 to 20 per cent of C, most MaaXBoard drivers have been rewritten in it, and a libmicrokit rewrite is under way. Device-interface specifications combine Pancake driver code with Verilog device models and HOL4 specifications — the I²C driver is complete with the Verilog finite state machine done and the HOL4 equivalence proof in progress, SPI next, Ethernet after. The ambition is drivers that are verified against a formal model of the device, which is the piece the seL4 assurance story has always been missing at the bottom.

Virtualization and the legacy-software problem

Nobody rewrites a working system from scratch to move it onto a verified kernel. The path that has actually produced seL4 deployments is virtualization first, decomposition afterwards, and it is the single most important adoption pattern in the project’s history.

The kernel supports hardware virtualization on Arm v7 and v8 hypervisor mode, and on x86 with Intel VT-x and EPT plus an HPET capable of MSI delivery. Multiple heterogeneous virtual machines can run concurrently. seL4 13.0.0 added GICv3 virtualization. The kernel provides the mechanisms — vCPU objects, second-stage translation, fault forwarding — and the virtual machine monitor runs in user space as an ordinary seL4 component, which means the VMM is not part of the trusted computing base in the way a conventional hypervisor is. A compromised VMM can destroy its own guests and nothing else.

Two VMM implementations matter. The CAmkES VM, built on libsel4vm and libsel4vmmplatsupport, is the mature option, static in configuration and used in the defence-oriented deployments. libvmm is the Microkit-based successor used by LionsOS, supporting AArch64 across QEMU virt, MaaXBoard, i.MX8, Raspberry Pi 4 and ZCU102, plus x86-64 with VT-x, offering VirtIO console, network, block, GPU and sound devices, and explicitly in development rather than production-ready.

The virtualization overhead question has one good independent answer, from Martins and Pinto’s 2023 comparison of static-partitioning hypervisors on a Xilinx ZCU104 with four Cortex-A53 cores. For the seL4 CAmkES VMM: base virtualization overhead up to 7 per cent on MiBench workloads; interrupt latency about 9,400 nanoseconds against a 200-nanosecond bare-metal baseline, degrading to roughly 85,940 nanoseconds under interference; inter-VM notification latency about 18,000 nanoseconds; IPI latency 10,868 nanoseconds against 260 bare-metal. Trusted computing base: the microkernel at 14,569 lines of C and a 225 KiB binary, plus the CAmkES VMM at 20,932 lines of C and 19,291 of assembly in a 724 KiB binary — about 40,000 lines total.

Those interrupt-latency numbers made seL4 the worst of the four hypervisors compared, and the reason is important: the latency is in the user-level VMM’s interrupt handling, not in the kernel’s IPC path. It is the cost of the architectural decision to put the VMM outside the TCB. The study also predates cache colouring being available for seL4, which affects the interference figures. Read as a comparison of kernels it is misleading; read as a measurement of what the CAmkES VMM costs, it is the best data available.

The incremental cyber-retrofit pattern that DARPA HACMS demonstrated is the practical playbook. Step one: put the entire legacy system in a virtual machine on seL4, which changes nothing functionally and immediately means the legacy code no longer has full hardware privilege. Step two: split it into multiple VMs along trust boundaries, so compromising the camera subsystem does not reach the flight controller. Step three: extract the genuinely critical functions into native seL4 components with small, auditable implementations, leaving the bulk of the legacy code in a contained VM where its defects do not matter. Each step stands on its own and each ships on its own, which is why this pattern has produced deployments where “rewrite everything on a verified kernel” has not.

The kernel’s documentation contains one warning worth repeating: running a real-time operating system as a guest is a bad idea, because the guest RTOS has almost no control over when it actually executes. Time on seL4 belongs to whoever holds the scheduling-context capability.

Rust, Pancake and the languages growing around the kernel

seL4’s kernel is C and will remain C, for a reason that has nothing to do with preference: the proof is written against C, and rewriting the kernel in another language would mean rebuilding a million lines of Isabelle. That constraint does not extend upward. Everything above the kernel is a free choice, and the ecosystem’s language story has shifted substantially since 2022.

Rust support is now first-class and Foundation-managed. The rust-sel4 project provides a sel4 crate wrapping the API, sel4-sys for raw bindings, sel4-root-task for root-task runtimes, sel4-microkit for writing Microkit protection domains in Rust, plus custom rustc target specifications for seL4 user space and async support. Releases are pinned to kernel and Microkit versions in lockstep: version 5.0.0 pairs with seL4 16.0.0 and Microkit 2.3.0. The reasoning behind investing here is straightforward — memory safety in user-space components does not remove the need for isolation, but it substantially reduces the rate at which components need to rely on it.

DARPA PROVERS funds Rust-based verified application development on Microkit explicitly, with work at the University of Kansas and Kansas State’s SAnToS Lab, and John Hatcliff’s keynote at the 2025 summit in Prague covered the HAMR model-based framework targeting Microkit and Rust. Google’s KataOS — the Project Sparrow work open-sourced in October 2022, written mostly in Rust on seL4 for ambient machine-learning devices — was an early demonstration of the approach, though Google is no longer a listed Foundation member and KataOS activity has lapsed.

Pancake is the more interesting long-term bet. It is a small systems language on the CakeML verified compiler stack, which means code compiled by it comes with a proof relating the binary to the source semantics — the same property translation validation gives seL4’s C, but by construction rather than per-compilation. Performance lands within 15 to 20 per cent of C, which is the right side of the line for driver code. Most MaaXBoard drivers have been rewritten in it and a libmicrokit rewrite is under way. The device-interface work pairs Pancake drivers with Verilog models of the device and HOL4 specifications, aiming at drivers verified against the hardware they drive.

Two more pieces of the language story. Viper integration is experimental in Microkit 2.3.0, and at the 2025 summit UNSW’s Jingyao Zhou presented an Ethernet driver verified via Pancake through a Viper transpiler. And Elixir and Erlang on the BEAM virtual machine are supported by Kry10’s commercial platform — an unusual choice for embedded work that makes sense given the platform’s focus on resilient, self-healing device fleets, where BEAM’s supervision trees map naturally onto a system designed around component restart.

The pattern across all of it: the kernel stays in verified C, the components move to memory-safe or verified languages, and the frameworks absorb the capability plumbing. Nobody in the seL4 ecosystem argues that C is a good language for application code. The argument is that for ten thousand lines with a million lines of proof attached, the language matters less than the proof.

Proof engineering as an industrial discipline

The most transferable thing seL4 produced is not the kernel. It is the finding that large formal proofs behave like large software and need the same engineering practices, a position Gerwin Klein argued at FM 2014 under the title “Proof Engineering Considered Essential.” At the time the proof base was around 400,000 lines. It is now past a million.

The doctrine is that proofs are code: they need version control, modularity, refactoring, regression testing, continuous integration, cost estimation and team scalability. That sounds obvious until you consider that the mathematics community’s model of a proof is a document written once and read thereafter, and that most formal-methods research treats proof construction as the end of the story rather than the beginning of a maintenance obligation lasting decades.

The maintenance numbers from the seL4 team’s own measurements are the most useful data anyone has published on this. A local, low-level code change requires re-verification effort roughly proportional to the size of the change. A new, largely independent feature such as an added system call: under one person-week. A large cross-cutting feature — the addition of interrupts and Arm page tables, roughly 37 per cent new code — took one and a half to two person-years to re-verify. A fundamental change to an existing feature, specifically the reply capability rework, cost about one person-year, or 17 per cent of the original proof effort.

One asymmetry in that data deserves attention because it explains why the economics improve over time: there is one class of otherwise frequent code change that stops occurring after a kernel is verified — implementation bug fixes. A conventional kernel’s change history is dominated by them. seL4’s is not, because they were eliminated once.

There is also a predictive cost model. Daniel Matichuk, Toby Murray, June Andronick and colleagues found at ICSE 2015 a consistent quadratic relationship between the size of a property’s formal statement and the final size of its proof, measured across 15,018 lemmas and roughly 215,000 lines of Isabelle spanning seL4 and the two largest Archive of Formal Proofs entries. Combined with the earlier finding of a strong linear relationship between proof effort and proof size, this gives something formal-methods projects have historically lacked entirely: the ability to estimate verification cost before starting. The practical implication is that keeping specifications small pays quadratically.

The tooling built to make this work is substantial and much of it outlived its original purpose. lib/ holds proof libraries for machine words, the non-deterministic state monad and verification condition generators. crunch lifts invariant-preservation proofs across large families of similar lemmas. Eisbach, a language for writing Isabelle proof methods, was developed for seL4 and is now part of Isabelle proper. The C parser, AutoCorres, the assembly refinement framework and the Haskell translator all exist because someone needed them at scale.

Continuous integration runs the proofs across AArch32, AArch32-hyp, AArch64, RV64 and x86-64, in configurations with and without the domain scheduler, and across the verified-platform matrix. Most proof sessions fit in 4 GB of RAM; the C refinement proof needs around 16 GB, and sessions parallelise across cores. This is why a kernel change can be evaluated for proof impact in hours rather than months.

The institutional history is the fragile part. The proof work moved from NICTA to CSIRO’s Data61 to Proofcraft, a company founded on 14 April 2021 by June Andronick as CEO and Gerwin Klein as CTO after Data61 dismantled the Trustworthy Systems group. Proofcraft now performs most seL4 proof engineering under contract to the UK’s NCSC, DARPA and Germany’s Cyberagentur. The world’s deepest concentration of operating-system proof expertise sits in one small company, which is a considerable single point of failure for a technology whose entire value proposition is assurance.

The economics of verification, per line and per year

The standing objection to formal verification is cost. seL4 is the only project with enough data to answer it, and the numbers do not support the objection as strongly as the objection assumes.

The original verification cost approximately twenty person-years of proof effort, split into about nine person-years building frameworks and tools — reusable, and largely reused since — and eleven person-years of seL4-specific work. Within that eleven, the first refinement step including its invariants took roughly eight person-years and the second about three. Designing, implementing and testing the kernel itself took 2.2 person-years, meaning verification cost roughly five to nine times as much as construction depending on how the tooling investment is amortised.

Expressed per line, Gernot Heiser’s figure is under 400 US dollars per line of code, or about 1.4 person-years per thousand lines. The comparisons are what make it interesting. The unverified Pistachio microkernel cost only two to three times less per line than verified seL4, while making no assurance claims whatsoever. A Green Hills high-assurance kernel in the EAL6 class was estimated at around 1,000 dollars per line through design and certification — more expensive than seL4’s proof, for a weaker guarantee. And the Cogent work that followed, applied to a file system rather than a kernel, achieved 0.6 person-years per thousand lines, roughly 60 per cent cheaper than seL4’s rate.

That last figure matters more than the historical one. The cost of verification is falling, because the tooling, the libraries, the proof-engineering practices and the trained people now exist. The twenty person-years seL4 spent included inventing the discipline. Nobody has to do that again.

The 2024-to-2026 period demonstrates the point. The platform verification work took Arm coverage from 13 per cent to 90 per cent in a single year and drove the marginal cost of a new platform to approximately zero. That is not a linear improvement in productivity; it is a change in what the unit of work is. Rather than verifying platforms, the team verified a parameterisation and then instantiated it.

There is also an ongoing cost nobody advertises. The proof base must be maintained against a kernel that keeps changing — four major releases between July 2024 and July 2026, each with new platforms, new features and breaking API changes. Every one of those changes has a proof cost, and the measured figures earlier in this article are the basis for budgeting it. Verification is not a one-time expenditure that produces a permanently verified artefact. It is a continuing obligation, and the reason seL4’s proofs are still valid is that someone has been paid to keep them valid for seventeen years.

The funding structure that pays for it is worth noting in an economic discussion because it is unusual. Almost none of this is commercially self-funding. DARPA, the UK’s NCSC, Germany’s Cyberagentur and the Australian public purse have carried the proof work, with Foundation membership fees — bounded by the published schedule at something in the low hundreds of thousands of Swiss francs annually — covering coordination rather than research. seL4’s economics work because governments have decided that verified systems software is a public good. That is a durable position while the geopolitics favour it and a fragile one if they do not.

HACMS, the Little Bird and the red team that failed

The single most persuasive piece of evidence for seL4 is not a proof. It is a red-team result from a DARPA programme, and it is worth reconstructing carefully because it is frequently repeated in a garbled form.

HACMS — High-Assurance Cyber Military Systems — ran from roughly 2012 to 2017 under DARPA, founded by programme manager Kathleen Fisher and continued by John Launchbury and Ray Richards. Trade reporting at the time of the solicitation put the budget at 60 million US dollars over four and a half years in three eighteen-month phases across five technical areas; DARPA’s own retrospective gives no budget figure. More than a hundred people were involved across DARPA, the Air Force Research Laboratory and the performers.

The seL4 team’s project within it was SMACCM — Secure Mathematically-Assured Composition of Control Models, funded at 18 million dollars over four and a half years, led by Rockwell Collins with NICTA’s Trustworthy Systems group, Galois, Boeing and the University of Minnesota. The research vehicle was a 3D Robotics Iris+ quadcopter, the SMACCMcopter, whose flight computer ran the eChronos RTOS with rewritten flight code and whose mission board ran seL4 hosting a virtualised Linux plus native seL4 components. DARPA’s figure is that roughly 80,000 of the quadcopter’s 100,000 lines of code were rewritten using formal methods.

The demonstration that mattered was on Boeing’s Unmanned Little Bird, an optionally-piloted autonomous helicopter with separate flight-control and mission processors. The retrofit followed the incremental pattern: virtualise the legacy mission software under seL4, split it into multiple VMs, then convert the critical functions to native seL4 components.

In 2013, before the retrofit, a DARPA red team fully compromised the aircraft. DARPA’s own account is that the team gained complete system access and could have crashed the helicopter or diverted it anywhere it chose.

After the retrofit, the red team was given six weeks and white-box conditions — access to all source code and documentation, access to all external communications, and, critically, root access inside the camera virtual machine, deliberately granted to simulate a successful compromise of the legacy software. The goal was to break out of that VM and affect anything else. Every attempt failed. Quanta Magazine dates the six-week engagement to summer 2015. A separate documented event, reported in Communications of the ACM, was an in-flight test in February 2017 with a safety pilot aboard, in which the aircraft was attacked mid-flight by rogue camera software and a virus delivered on a compromised USB stick: subsystems were compromised, safe flight was never affected, and test pilots reported no performance degradation. DARPA states the Little Bird “remains uncompromised to date.”

That result is qualitatively different from a proof and complements it. A proof says the kernel matches its specification. A red team with source code, six weeks and root inside the perimeter says the system architecture built on that kernel actually confines a real attacker with real advantages. Very few security claims in any field come with that kind of evidence.

The programme’s reach extended beyond aviation. Ground work used the TARDEC GVR-Bot as a research platform and transitioned to the AMAS autonomous mobility system on a Heavy Equipment Transporter — the autonomous convoy truck that appears in DARPA’s summaries — and DARPA states the tooling also transitioned to satellite systems. In August 2021 the SMACCMcopter resisted attack at a DEF CON drone-security challenge. In December 2023 HACMS received a “Game Changer” award from DARPA leadership. Its successors were CASE, on cyber-assured systems engineering with Collins Aerospace, and PROVERS, which funds much of the seL4 proof work described in this article.

Two caveats for accuracy. The programme’s end date is given as 2017 by the seL4 Foundation and “approximately 2012 to 2018” by Fisher’s own page. And the relationship between the summer 2015 six-week engagement and the February 2017 in-flight test is not documented anywhere I could verify — they appear to be separate exercises, but no source states this explicitly.

Automotive adoption and the NIO mass-production milestone

For most of its life seL4’s deployments were in aerospace, defence and research. That changed with automotive, and the case that matters is NIO, the Chinese electric-vehicle maker, which is the only organisation to have taken an seL4-based operating system into volume production in a consumer product.

NIO joined the seL4 Foundation as a Premium Member on 18 June 2021 — the top tier at 100,000 Swiss francs annually, which comes with a guaranteed Governing Board seat, currently held by Qiyan Wang. Yanyan Shen of NIO sits on the Technical Steering Committee. NIO announced its SkyOS vehicle operating system on 24 November 2023 and formally launched it at the NIO IN event on 27 July 2024. SkyOS is a family; the seL4-based member is SkyOS-M, and it is in mass production in the ONVO L60, NIO’s mainstream sub-brand SUV. NIO cites inter-component communication latency below one millisecond. The companion in-house autonomous-driving chip, the 5-nanometre NX9031, taped out by mid-2024 and shipped first in the ET9 with deliveries from the first quarter of 2025. SkyOS received a “Global NEV Innovation Technology” award in September 2025.

Why automotive is the natural market is worth spelling out. A modern vehicle consolidates dozens of previously separate electronic control units onto a handful of high-performance compute platforms, which means safety-critical functions now share silicon with infotainment, connectivity and third-party applications. The regulatory framework — ISO 26262 with its ASIL levels, and ISO/SAE 21434 for cybersecurity — demands that the safety-critical side be protected from the rest. The conventional solution is a certified hypervisor plus a certified RTOS plus Linux or Android for the rich functions. seL4 with MCS offers the same architecture with a stronger isolation argument and better processor utilisation, and it offers it under an open-source licence with no per-unit royalty, which in an industry with automotive margins is not a minor consideration.

The rest of the automotive story is more cautionary. Li Auto joined as a Premium Member on 23 June 2021 for autonomous-driving platform work, Horizon Robotics joined Premium the same day, and Lotus Cars joined on 18 August 2021. None appear on the Foundation’s current member roster. The Autoware Foundation joined as an Associate member on 22 March 2023 to build an autonomous-driving stack over seL4. And Ghost Autonomy — formerly Ghost Locomotion, an seL4 Foundation founding member that donated to the Foundation in August 2021 — ceased operations on 3 April 2024 after raising roughly 220 million dollars including 5 million from the OpenAI Startup Fund about five months before shutdown, with around a hundred employees at the end.

The membership absences need care. The Foundation has been updating its roster since the December 2025 move to Swiss incorporation, and no departure announcements exist for any of these companies, so some absences may be administrative lag rather than exits. What can be said is that the automotive interest that arrived in 2021 has consolidated: one Premium member in production, several early enthusiasts no longer visible, and one high-profile failure that had nothing to do with the kernel.

Even the NIO relationship has a documentary gap worth flagging. NIO states SkyOS is seL4-based and the Foundation lists SkyOS-M in the ONVO L60, but NIO’s own July 2024 launch materials do not name seL4, and whether the refreshed ONVO L60 launched on 11 June 2026 carries SkyOS-M is not something I could confirm.

Defence, space and the high-assurance vendor layer

seL4’s commercial ecosystem is thin, specialised and heavily weighted toward defence, which is what one would expect of a technology whose value is assurance rather than features.

Collins Aerospace, part of RTX, is the most substantial industrial participant. RTX joined the Foundation on 4 March 2021, holds a Governing Board seat through David Hardin, and its team carries HACMS and CASE experience directly. Collins leads the seL4 effort under DARPA PROVERS, directed by Darren Cofer, and has sponsored the seL4 Summit annually since 2023.

DornerWorks, a Michigan engineering firm, is a founding Foundation member and an Endorsed Service Provider since February 2021. Its product VM Composer is a modelling tool for building seL4-based virtual machine systems, positioned as the approachable route in. Robbie VanVossen of DornerWorks co-chairs the 2026 summit programme committee. DornerWorks also publishes the ecosystem’s only substantial material on seL4 for medical devices, which should be read as vendor advocacy: no shipping seL4 medical product has been publicly identified.

HENSOLDT Cyber in Germany was a founding member and the first company with an endorsed seL4 product. Its TRENTOS operating system runs on seL4 atop the company’s MiG-V RISC-V processor, and HENSOLDT funded the RV64 binary verification announced on 5 May 2021 — a direct case of a commercial user paying for a proof that benefits everyone. In April 2022 it partnered with Beyond Gravity, the former RUAG Space, to put TRENTOS on the Lynx satellite computer. HENSOLDT Cyber does not appear on the Foundation’s current member roster, no departure was announced, and its TRENTOS-G product pages remain live. Its current status is genuinely unclear and worth direct confirmation before relying on it.

Cog Systems, another founding member with a board seat, built the D4 Secure and Aegis Secure product lines. Riverside Research acquired it in March 2025 and joined the Foundation as an Associate member on 19 January 2026, continuing the high-assurance virtualization work.

Kry10, a New Zealand company led by former Xbox and XNA executive Boyd Multerer, sells KOS — a commercial seL4 platform for managing fleets of mission-critical connected devices, with signed updates, live upgrade, self-healing supervision, and support for C, Rust and Elixir on the BEAM virtual machine. It raised a 6 million New Zealand dollar pre-Series A from investors including Folklore Ventures and a fund with reported intelligence-agency links, holds three Technical Steering Committee seats, and its Chief Scientist Martin Dehnel-Wild keynotes the 2026 summit. Kry10 publishes no cycle-level performance figures.

Other participants fill in the picture. Penten in Canberra builds secure communications and AI for Australian Defence. Skykraft, also Canberra, operates a space-based VHF air-traffic-management constellation. MEP joined in April 2025 with SureVoice Solid, a voice-control system for air-traffic and maritime communications sold on continuous availability. Neutrality joined in March 2026 with the Atoll hypervisor. Gapfruit in Switzerland joined in June 2026. Breakaway Consulting built Microkit. Proofcraft does the proofs. Galois, a HACMS performer, joined in 2023 after acquiring Adventium Labs.

Two absences are conspicuous. General Dynamics, which acquired Open Kernel Labs in 2012 and announced seL4’s open-sourcing in July 2014, is not a Foundation member. And Apple, a General Member since 29 April 2024, Silver sponsor in 2024 and Gold sponsor of the 2026 summit, with Lucy Fletcher co-chairing the programme committee, has published nothing whatsoever about using seL4 in any product. The seL4 whitepaper’s statement that an L4-derived kernel runs in the secure enclave of recent iOS devices refers to L4-embedded, not seL4, and conflating the two is the most common factual error in coverage of this topic.

Multikernel ambitions and seL4 on big iron

seL4’s verification story has a shape that reflects when it was built: single core, or at most a small number of tightly-coupled cores under a big lock. Multiprocessor support exists on x86-64, Armv7, Armv8 and RISC-V, and it works, and it is not verified. The design is explicitly a big-lock kernel intended for a handful of cores sharing an L2 cache, with the documentation stating outright that it is not meant to scale to many cores.

For most of seL4’s target market this is acceptable. Embedded and automotive platforms have four to eight cores, and the isolation properties that matter most are between components rather than across a large socket. For anything resembling a datacentre it is disqualifying, and closing that gap is where the current architectural work is concentrated.

The approach is a static multikernel: rather than one kernel instance managing all cores with concurrency inside the kernel, run one independent kernel instance per core, each with its own memory and its own capability space, communicating through explicit, controlled channels. The verification advantage is decisive — a single-core kernel proof mostly carries over, because each instance is doing what the verified kernel already does, and the concurrency reasoning moves to a much smaller and more tractable interaction model between instances rather than being smeared through every kernel operation.

Gerwin Klein and Corey Lewis presented the roadmap at the 2024 summit: one kernel per core, a fully concurrent model of their interaction, and maximal reuse of existing proofs. Germany’s Cyberagentur joined the Foundation on 20 January 2025 and funds Proofcraft and Kry10 to extend the proofs to a static multikernel configuration, as one of five projects under its trustworthy-IT programme. A related project, Dyvercon, covering cyber-physical systems, reported progress at a Cyberagentur milestone summit on 28 April 2026. seL4 14.0.0 added software-generated interrupt support specifically for Arm multikernel configurations.

The commercial expression of this is Neutrality, which joined the Foundation on 13 March 2026 with a product called the Atoll hypervisor — a static multikernel seL4 configuration explicitly targeting hundreds of CPU cores for datacentre and defence hosting. David Cock, formerly of the seL4 group and later ETH Zurich, presented it at the 2025 summit under the title “seL4 on Big Iron.” The proposition is a hypervisor whose isolation properties rest on a verified kernel at a scale where the conventional answer is KVM or Xen with a trusted computing base measured in millions of lines.

It is early. The static multikernel proofs do not exist yet, Atoll is a young product from a young company, and the hard questions about many-core seL4 — shared last-level cache, memory bandwidth contention, cross-socket interconnect, all of which are precisely the resources Ge and colleagues identified as unpartitionable — are the same questions time protection has not solved on a single socket. The architectural direction is sound and the verification path is credible. Nothing has been delivered yet.

Certification, compliance and an argument now happening in public

seL4 is not certified against any scheme. Not Common Criteria, not DO-178C, not IEC 61508, not ISO 26262. For a technology sold on assurance in industries governed by certification, this is either the most interesting thing about it or the largest obstacle to adopting it, depending on who is being asked.

The Foundation’s argument is that the proofs exceed what the schemes require. The Common Criteria case is the cleanest. Formal methods appear in the Common Criteria development-assurance class only from EAL 6 upward, and even EAL 7 — the highest level, achieved by a handful of products ever — requires a formal security-policy model, a formal functional specification and a formal design specification with formal correspondence between them, but only an informal mapping down to the implementation. seL4’s response is direct: it has a formal proof all the way to the implementation and, on Armv7 and RV64, to the binary. On that specific dimension, seL4’s evidence genuinely is stronger than EAL 7 demands.

Similar arguments are made elsewhere. ISO 26262 recommends formal verification for ASIL-C and ASIL-D but defines it modestly as proving correctness against a specification in formal notation, so seL4’s assurance is described as considerably stronger than the highest automotive risk level requires. For DO-178C Level A, seL4 asserts its proofs provide the required evidence with the strength of mathematical proof — with the explicit caveat that Isabelle/HOL has not been qualified as a DO-178C tool, which is not a small gap in an aerospace certification argument.

The counter-argument, which certification authorities make and which is not unreasonable, is that certification is not only about the strength of correctness evidence. It is about process, traceability, configuration management, independent review, tool qualification and the auditability of the whole development. A proof is one form of evidence within that framework, not a replacement for it. A safety case cannot cite a theorem and stop, and the gap between “we have a proof” and “we have a certifiable artefact” is filled with documentation work that nobody has done for seL4 in general — it has to be done per product, by the product’s developer.

The seL4 ecosystem’s own position on this has visibly shifted. For years the message was that formal proof made certification largely beside the point. The 2026 summit in Vancouver is running a panel titled “Certification, Compliance and Policies: enabler or barrier to innovation?” with Collins Aerospace, Thales, SafeShark, Atalanta and the UK Defence Science and Technology Laboratory. Whatever conclusion that panel reaches, convening it is an admission that the certification question is not settled by pointing at a proof — and that the customers who most want verified software are exactly the ones who cannot buy uncertified software.

The commonly cited fact-sheet figures are worth reproducing with their caveats. The Foundation’s fact sheet gives roughly 1.3 million lines of proof, functional correctness completed in 2009, properties comprising functional correctness, binary correctness, integrity and confidentiality, positioning “beyond CC EAL7, ISO 26262 ASIL-D and DO-178C Level A,” and zero violations of the verified properties since 2009. Every one of those is defensible. Every one is also a claim about specific configurations on specific architectures, and the matrix earlier in this article is what determines whether it applies to the system a given team is building.

Competitors measured on their own assurance terms

seL4 is usually compared against other microkernels, which flatters it. The comparison that matters commercially is against the certified real-time operating systems that currently hold the high-assurance market, and on their chosen metric — certification against recognised schemes — seL4 loses.

Assurance claims of seL4 and its principal alternatives

The table shows the actual competitive shape: seL4 has the strongest correctness evidence and the weakest paperwork, while the incumbents have certifications, deployment scale and supply-chain relationships that seL4 cannot match.

The most instructive comparison is Green Hills INTEGRITY-178B, the only operating system ever certified against the NSA’s Separation Kernel Protection Profile at EAL 6+, achieved in 2008 with a second certification in 2011. That is a stronger procurement position than seL4 has, and a weaker technical one: SKPP certification does not include a machine-checked proof that the implementation matches its specification. It also cost, by the estimate cited earlier, around a thousand dollars per line — more than seL4’s proof.

QNX is the commercial reality check. It has ISO 26262 ASIL D, IEC 61508 SIL 3, IEC 62304 Class C and Common Criteria EAL 4+, and it announced in October 2024 that it runs in more than 255 million vehicles, up 80 million since 2020. It has no functional-correctness proof and does not need one to win automotive business, because it has certifications, a support organisation, tooling and two decades of field history. seL4’s automotive footprint is one manufacturer’s sub-brand SUV.

ProvenCore is the closest philosophical competitor: a French secure OS with a claimed EAL 7 certification and formal proofs of isolation using a non-Isabelle toolchain. If the EAL 7 claim holds, it occupies a position seL4 does not — formally proven and certified at the highest level — though its proof scope is isolation properties rather than full functional correctness, and I could not confirm the certification date or scheme from primary sources.

The academic alternatives illustrate what seL4 got right. CertiKOS proved a concurrent kernel in Coq, a genuine advance seL4 has not matched, at roughly five times seL4’s IPC cost. Hyperkernel demonstrated push-button SMT verification of an xv6-derived kernel by constraining the interface to stay decidable. Muen proves absence of runtime errors in SPARK/Ada — a real result and a much weaker one than what seL4 claims. And the honest baseline seL4 actually competes against in most procurements is Linux plus a hypervisor, where assurance exists only at the hypervisor layer and the twenty-million-line kernel above it is simply accepted. seL4’s answer to that is to run Linux as a guest, which is what every successful deployment has done.

The Foundation, the Swiss move and the churn nobody announced

seL4’s governance history is a case study in what it takes to keep a research artefact alive after the research funding ends, and it has had one genuine crisis.

The seL4 Foundation launched on 7 April 2020 under the Linux Foundation, with founding members CSIRO’s Data61, Cog Systems, DornerWorks, Ghost Locomotion, HENSOLDT Cyber and UNSW Sydney. Gernot Heiser chaired the founding board alongside June Andronick, Gerwin Klein, John Launchbury of Galois, Sascha Kegreiß of HENSOLDT Cyber and Daniel Potts of Cog Systems. The stated purpose was to pool funding from organisations that individually could not sustain the proof work — Heiser’s framing at the time was that no single company could fund it alone. The seL4 trademark was registered in the United States and elsewhere on 11 April 2022, and June Andronick became part-time CEO on 9 June 2021.

On 17 December 2025 the Foundation left the Linux Foundation and became an independent Swiss non-profit association under the legal name “seL4 International.” The rationale given was neutrality and Switzerland’s established framework for international non-profits, citing RISC-V International as precedent. Purpose, principles and internal structure were stated to be unchanged. For a project whose funders now include the American, British, German and Australian governments, and whose largest paying member is a Chinese automaker, jurisdictional neutrality is not an abstract concern.

Governance is split between a Governing Board — brand, funds and outreach — and a Technical Steering Committee chaired by Gerwin Klein, which decides technical direction. The board seats the three founders, one representative per Premium member and one elected by the General members as a class; the current board is Heiser as chair, Andronick as CEO and Treasurer, Klein, David Hardin of RTX and Qiyan Wang of NIO. The TSC is dominated by Proofcraft, Kry10 and UNSW, with NIO represented.

The fee schedule is published: Premium at 100,000 Swiss francs annually with a guaranteed board seat; General from 2,500 francs for organisations under 21 employees up to 35,000 for those over 5,000; Associate free for non-profits, open-source projects and government entities, without voting rights.

The membership roster is the part that repays close reading. There is currently one Premium member: NIO. Ten General members: Apple, DornerWorks, Gapfruit, Kry10, MEP, Neutrality, Penten, Proofcraft, RTX and Skykraft. Twelve Associate members including the UK’s NCSC, Germany’s Cyberagentur, Fraunhofer AISEC, ETH Zurich, TU Munich, Kansas State, the University of Kansas, Riverside Research, the Autoware Foundation and UNSW.

Now the absences. Organisations that publicly announced joining and do not appear on the current roster include Google (August 2022), Li Auto and Horizon Robotics (both Premium, June 2021), Jump Trading (Premium, June 2021), Lotus Cars, Xcalibyte, Second State, the Technology Innovation Institute, LatticeX, SpacemiT, Galois, and both founding members HENSOLDT Cyber and Cog Systems — the latter now folded into Riverside Research, and Ghost Autonomy defunct. No exit announcements exist for any of them. The Foundation has been updating the roster since the Swiss transition, so some absences may be administrative. But four Premium members announced in 2021 and one remaining in 2026 is a pattern, and it suggests the 2021 wave of interest — particularly from Chinese automotive and from Google — did not convert into sustained commitment.

The annual summit is the ecosystem’s centre of gravity: Munich 2022, Minneapolis 2023, Sydney 2024, Prague 2025, and Vancouver on 1–3 September 2026 with a new three-day format opening on applications, co-chaired by Robbie VanVossen of DornerWorks and Lucy Fletcher of Apple, keynoted by Anjana Rajan of Atalanta — formerly the White House Assistant National Cyber Director — and Martin Dehnel-Wild of Kry10, with Apple as gold sponsor.

Who pays for the proofs

Follow the money and seL4’s institutional position becomes clear: it is publicly funded critical infrastructure with a small commercial layer on top, and its trajectory depends on government decisions rather than market ones.

The Australian origin is also the cautionary tale. Verification began at NICTA, the government-funded ICT centre of excellence, and continued at CSIRO’s Data61. On 21 May 2021 Data61 dismantled the Trustworthy Systems group as part of a restructure toward artificial intelligence — 100 million Australian dollars over four years across five growth areas plus 50 million for a national AI centre — with up to seventy staff at risk. CSIRO’s position was that formal methods was “a mature area… now well supported outside the organisation.” Heiser called it “a sad day for Australian computer science.” UNSW provided undisclosed bridge funding to keep about a dozen people employed to the end of that year, and the group now exists as Trustworthy Systems at UNSW Sydney. The country that produced the world’s first verified OS kernel came within one budget decision of losing the team that built it.

The United Kingdom stepped in. The National Cyber Security Centre joined the Foundation on 2 February 2022 and funds research at both UNSW and Proofcraft, publicly announced for UNSW in June 2022. NCSC money delivered the AArch64 functional-correctness proof in April 2024 and the AArch64 integrity proof in April 2025 — the latter the first seL4 security theorem covering hypervisor mode and the FPU. NCSC also funded the project’s new website in April 2025 and its new documentation site in July 2025. No amounts have ever been disclosed.

Germany is now the second major funder. Cyberagentur, the Federal Agency for Disruptive Innovation in Cybersecurity, joined on 20 January 2025 and launched five research projects under its trustworthy-IT programme, one funding Proofcraft and Kry10 to extend seL4’s proofs to a static multikernel configuration, and another, Dyvercon, covering cyber-physical systems. The 2025 summit keynote from Cyberagentur was titled “Formally verified IT – Germany’s next cybersecurity paradigm,” which is about as explicit a statement of national strategy as one gets. Amounts undisclosed.

The United States funds through DARPA. PROVERS — Pipelined Reasoning of Verifiers Enabling Robust Systems — runs 42 months across three phases under programme manager Xenofon Koutsoukos, building on the PEARLS work on applying machine learning to proof generation and repair. On 2 December 2024 Proofcraft was announced as part of PROVERS alongside Collins Aerospace (leading, under Darren Cofer), UNSW Sydney, DornerWorks, Carnegie Mellon, the University of Kansas and Kansas State. The committed deliverables were automated platform-port verification, an architectural split of the proofs, and completion of the MCS functional-correctness proof — all three of which have since been delivered or substantially advanced. PROVERS also funds Rust-based verified application development on Microkit and AI-assisted proof repair. No dollar figure for the seL4 portion has been published; the only PROVERS award amount found publicly is 6 million dollars to BAE Systems FAST Labs, announced 4 December 2024, with no stated seL4 connection.

Smaller contributions matter more than their size suggests. HENSOLDT Cyber funded RV64 binary verification. XCalibyte donated in November 2023 to fund the MCS proof framework. The Foundation itself funded the automated proof checks that extended verification across six platforms in January 2024. This is the pooled-funding model working as designed: a company needs a specific proof, pays for it, and the result is public.

The structural risk is concentration. Proofcraft does most of the proof work, and its funders are three national security agencies and a defence prime. Government research priorities change — Australia’s did, abruptly, in 2021. The Foundation’s own revenue, bounded by the published fee schedule at roughly 150,000 to 450,000 Swiss francs annually before sponsorship, covers coordination rather than research. seL4’s proofs are maintained because four governments currently believe verified systems software is worth paying for. That belief is the actual dependency.

Risks, limits and failure modes a proof cannot cover

Any honest assessment of seL4 has to separate what the proof rules out from what it does not, because the gap is where every real seL4 deployment will fail if it fails.

The kernel is not the system. A verified kernel in a badly designed system provides nothing. If the capability distribution grants a component more authority than it needs, the integrity theorem holds and the system is still insecure — because the theorem says the kernel enforces the policy, not that the policy is right. This is the most common way seL4 deployments will go wrong, and the mitigations are capDL, the verified initialiser, and Microkit’s constrained system description, all of which reduce but do not eliminate the designer’s ability to specify something unsafe.

The trusted components are unverified. Every system has components whose failure is fatal regardless of isolation: the VMM if it manages a critical guest, a DMA-capable driver, a cryptographic service, the initialisation code. LionsOS’s web server has 3,545 lines of trusted code. Kitty has around 2,100. Those lines carry ordinary software risk, and they are where an attacker will look.

DMA is the sharpest hardware gap. The proof assumes only the CPU and MMU access memory directly. A DMA-capable device driven by compromised code writes anywhere in physical memory, and device address translation is not verified in any seL4 configuration. Many embedded Arm platforms have no IOMMU at all. Microkit 2.3.0 enabling x86-64 IOMMU by default is progress; it is not a proof.

Timing channels remain open, at measured rates around 400 bits per second through the shared kernel before time protection, with a residual through the x86 prefetcher that no software can close, and interconnects and buses fundamentally unpartitionable on current hardware.

Unverified configurations are where the defects are. The x86-64 VM-escape fixed in seL4 16.0.0 — where a cooperating malicious VMM and guest could make the kernel jump to a user-controlled address, yielding arbitrary kernel-mode execution — is the cleanest illustration. It was real, it was serious, and it was in code the proofs never covered. seL4 16.0.0 also fixed an AArch32 kernel crash on cache maintenance against unmapped frames and a register leak across context switch in Arm hypervisor mode. The proof’s coverage boundary is the interesting attack surface, and it is documented, which means attackers can read it too.

Multicore is unverified. SMP works and is not covered by any proof. The static multikernel that would fix this does not exist yet.

MCS is verified on exactly one architecture — RISC-V, as of June 2026 — and its security theorems exist nowhere. Teams building mixed-criticality systems on AArch64 today are in unverified territory.

Compiler trust varies by architecture. Binary verification exists on Armv7 and RV64. On AArch64 and x86-64, GCC is inside the trusted computing base, and the proof chain stops at C.

Hardware assumptions are load-bearing and increasingly strained. Every proof assumes the processor behaves as specified. The disclosure rate for speculative-execution and microarchitectural defects since 2018 makes that an assumption worth restating rather than accepting quietly.

The people risk is real. The expertise to maintain a million lines of Isabelle against an evolving kernel is concentrated in one small company and one university group, and Australia demonstrated in 2021 how quickly institutional support can evaporate.

And ecosystem maturity lags the kernel by a wide margin. LionsOS is at 0.3.0 and describes itself as not stable. libvmm is not production-ready. Microkit had breaking changes in its last three releases. The kernel has had four major releases with breaking API changes in two years. The verified part of the stack is the mature part, and everything a product actually needs sits above it in software that is moving fast.

Practical steps for teams evaluating seL4

For an engineering organisation considering seL4, the decisions that matter are architectural and they come in a fairly strict order.

Establish first whether isolation is your actual problem. seL4’s value is strong isolation with a proof attached and low-overhead communication across isolation boundaries. If the requirement is a rich application platform, broad driver support or fast time-to-first-demo, seL4 is the wrong tool and Linux with a hypervisor will get further faster. If the requirement is that a specific critical function cannot be affected by anything else on the platform, and that claim has to survive hostile review, seL4 is the strongest available answer.

Then pick the architecture, and pick it against the verification matrix rather than the marketing. This is the decision most likely to be made wrong. AArch64 has functional correctness and integrity but no binary verification and no MCS. RV64 has everything including MCS functional correctness but no verified fastpath. x86-64 has functional correctness at the C level and nothing else. Armv7 has the most complete coverage and is 32-bit. Read the verified-configurations page directly and confirm your specific board appears on it — since seL4 14.0.0 every supported Arm platform does, which is a recent enough change that older evaluations got this wrong.

Choose the framework by system shape. Static architecture with a fixed set of components: Microkit, which is where all current investment is going and which has an SDK you can download. Existing CAmkES codebase or dependence on the defence tooling built around it: CAmkES, still maintained. Want a substantially complete system rather than a construction kit: LionsOS if you can tolerate a 0.3.0 release, or Kry10’s KOS if you want commercial support and fleet management. Building a hypervisor product at datacentre core counts: watch Neutrality’s Atoll and the multikernel proof work, but do not plan a 2026 ship date on it.

Design the capability graph before writing code, and treat it as the security architecture rather than an implementation detail. Enumerate every component, what authority it needs, what it can reach if compromised, and which components are trusted. Then check the trusted set is small enough to review by hand. If it is not, the architecture is wrong and no amount of kernel verification will fix it.

Plan the legacy path as virtualization first. The HACMS pattern is the proven route: everything in a VM, then split along trust boundaries, then extract critical functions to native components. Each step ships independently. Attempting a clean-slate rewrite is how seL4 projects die.

Benchmark on your own hardware and your own workload. The published IPC figures are real and they are microbenchmarks. What matters is end-to-end behaviour with your drivers, your message sizes and your scheduling parameters — and sel4bench exists to be run rather than cited. Pay particular attention to the MCS configuration’s costs if you need it; notify and IRQ costs on RV64 under MCS are several times the non-MCS figures.

Get the assumptions into your safety case explicitly. Enumerate DMA, IOMMU availability, the assembly and boot code, the compiler trust status for your architecture, timing channels, and the multicore situation. A safety case that cites “formally verified kernel” without the assumption list is not a safety case, and a reviewer who knows seL4 will say so.

Engage the ecosystem early. DornerWorks, Proofcraft, Kry10, Breakaway and UNSW are the Endorsed Service Providers and the Foundation maintains the list. The mailing lists are active and the developers answer questions. The annual summit is small enough that attending it means meeting most of the people who wrote the code.

Licensing, availability and the real cost of entry

seL4’s commercial terms are unusually simple and worth stating precisely, because “open source” covers conditions that differ sharply from one project to the next and procurement departments need the specifics.

The kernel is licensed under GPLv2. That licence covers the kernel itself. It does not extend to user-space components running on top of it, because they interact with the kernel through system calls rather than by linking against it — the same boundary that has always allowed proprietary applications on Linux. In practice this means a company can ship proprietary components on seL4 without licence obligations on that code, while any modifications to the kernel itself are subject to GPLv2’s terms. The verification proofs in the l4v repository carry their own licensing, and the library code, tools and frameworks around the kernel vary: Microkit, LionsOS and sDDF are BSD-style, which is the permissive end.

There are no per-unit royalties, no licence fees, and no runtime charges. This is a genuine differentiator against every certified RTOS seL4 competes with, where per-device royalties or seat licences are standard and where certification artefacts are typically sold separately at significant cost. For a high-volume automotive or IoT product, the royalty difference alone can dominate the engineering cost comparison. It is also part of why the seL4 Foundation exists: with no licence revenue, the development and proof maintenance have to be funded by membership and grants rather than by sales.

The trademark is separately protected. seL4® was registered in the United States and other jurisdictions on 11 April 2022, and the Foundation maintains trademark and endorsement policies governing how the name can be used. The endorsement scheme matters commercially — an Endorsed Service Provider or endorsed product has been reviewed by the Foundation, and HENSOLDT Cyber’s TRENTOS was the first endorsed product, in August 2021.

Getting the code costs nothing and takes minutes. The kernel is on GitHub. The Microkit SDK ships as a download for Linux and macOS on x86-64 and AArch64, containing prebuilt kernel images per supported board, the static library, loader and monitor binaries, examples and the manual. The tutorials run on QEMU, so evaluation needs no hardware at all. Documentation lives at docs.sel4.systems, rebuilt in July 2025 with NCSC funding, and the reference manual is a single PDF.

The real cost of entry is not money. It is the engineering time to internalise a capability-based design model that has no analogue in the systems most developers have worked on. There is no process abstraction to reason about, no ambient authority, no dynamic allocation, no file system, no shell. A team that has built Linux products will spend weeks before its mental model matches the machine. The frameworks reduce this substantially — Microkit’s four abstractions are learnable in a day — but they do not remove it, and the most common cause of a stalled seL4 evaluation is underestimating this rather than hitting a technical wall.

Support is available commercially. Proofcraft for verification, DornerWorks and Breakaway for engineering, Kry10 for a supported platform product, UNSW for research collaboration — the Foundation maintains the Endorsed Service Provider list. For an organisation that needs someone accountable, the layer exists; it is small, and its capacity is finite.

Privacy, data handling and the regulatory angle

seL4 is not a privacy technology and its documentation makes no privacy claims, but the isolation properties it provides map onto data-protection obligations in ways that are becoming commercially relevant, and the mapping is worth making explicit because vendors are starting to make it loosely.

The connection runs through data minimisation and purpose limitation, which under the GDPR and comparable regimes require that personal data be accessible only for the purposes it was collected for. In a conventional system, enforcement is a matter of application logic and operating-system access control, both of which sit on a kernel that any privileged defect can subvert. On seL4, “this component cannot read that data” can be a property of the capability graph rather than a property of correct behaviour by the code, and on the architectures where the confidentiality theorem applies, it can be a proved property of the kernel’s enforcement.

The sDDF design shows what that buys concretely. Drivers in the seL4 Device Driver Framework have no access to the data region at all — a network driver moves buffer addresses and never reads payload. A compromised network driver on a conventional system reads every packet. On sDDF it reads none, because it was never given a capability to the data. That is a structural privacy property rather than a policy one, and it is the kind of argument that survives an audit.

The regulatory environment is moving toward demanding this sort of evidence. The EU Cyber Resilience Act imposes security requirements on products with digital elements, including obligations around vulnerability handling and secure-by-design development. ISO/SAE 21434 governs automotive cybersecurity engineering. IEC 62443 covers industrial control. None of these mandate formal verification, and none of them currently give explicit credit for it, but all of them require developers to justify their security architecture with evidence — and a machine-checked proof plus a documented assumption list is stronger evidence than a test report.

Three limits keep this from being a straightforward selling point. Timing channels leak. A measured 400-bit-per-second channel through the shared kernel before time protection is applied is enough to extract a key or a small dataset, and no privacy claim should be made about a system where cross-partition timing channels have not been addressed. Trusted components see everything they are given. A verified kernel does not prevent an application from mishandling data it legitimately holds, and most privacy failures are of exactly this kind. And the confidentiality theorem’s configuration is restrictive — static schedule, no cross-partition IPC, DMA disabled — so a system using it as a compliance argument must actually be in that configuration, which most are not.

The defensible position is narrower and still useful. seL4 lets a system designer make enforceable, architecturally visible statements about which components can reach which data, and on some configurations those statements are backed by proof rather than by review. That is not compliance. It is the substrate a compliance argument can be built on, and it is more than any conventional kernel offers.

What working on a verified kernel does to engineering practice

The professional effect of seL4 on the people who build with it is a smaller story than the technical one and a more transferable one, because the practices it forces have started spreading to projects with no formal verification at all.

Design becomes explicit and front-loaded. On seL4 there is no way to defer the question of what authority a component holds, because the component cannot run until its capability space exists. The system’s trust architecture has to be written down — as a capDL specification, or a Microkit system description, or CAmkES ADL — before anything executes. Engineers accustomed to discovering their architecture through implementation find this uncomfortable and then, generally, find that the resulting systems are easier to reason about. The Microkit XML file is a security architecture document that is also the build input, which means it cannot drift out of date.

Small becomes a hard requirement rather than a preference. The measured relationship between specification size and proof size is quadratic, so on the verified parts of the stack, complexity is punished superlinearly. That discipline propagates upward even where proofs are absent: the LionsOS principle that policy must be fully contained in one module, and that modules should be single-threaded and event-driven, exists because that is what verification tools can handle. The 569-line Ethernet driver against Linux’s 4,775 is not a compression trick. It is what happens when multiplexing, policy, buffer management and cache handling are removed from the driver and placed in components that only do those things.

Failure analysis changes shape. In a monolithic system, the question after a defect is “what could this have affected?” and the answer is usually “anything.” On seL4 the answer is bounded by the capability graph, and it is bounded by construction rather than by investigation. This is what makes the incremental retrofit pattern work at all: a team can put legacy code in a VM and make a defensible statement about the blast radius on day one, without understanding the legacy code.

Testing does not go away. This is the most common misunderstanding. The kernel’s verification removes one class of defect from one component. The trusted components above it, the configuration, the drivers, the hardware interaction and the system’s actual behaviour under load all need the same testing any other system needs. What changes is that testing no longer has to carry the weight of establishing kernel correctness, which is the part testing was always worst at, because kernel defects are rare, state-dependent and catastrophic.

And the proof becomes a maintenance obligation rather than an achievement. Teams that contribute kernel changes learn quickly that a patch is not done when it works; it is done when the proofs go through, which the continuous integration infrastructure will tell them within hours. That feedback loop — where correctness is checked mechanically on every change, at the same cadence as compilation — is arguably seL4’s most exportable idea, and it does not require a million lines of Isabelle to adopt in weaker forms.

Scenarios and the questions the evidence cannot settle

Three trajectories are consistent with the evidence as of August 2026, and the difference between them turns on things that are genuinely undetermined.

The most likely path is continued deepening in high-assurance niches. The verification work is funded through the PROVERS and Cyberagentur programmes for the next several years, and the deliverables have arrived on time. MCS lands on AArch64. Confidentiality completes on AArch64. The static multikernel proofs progress. LionsOS reaches a stable release and picks up a handful of commercial adopters after the first in January 2026. Automotive, defence, satellite and industrial-control deployments accumulate one at a time. seL4 stays technically unmatched and commercially small — the kernel that everyone in high assurance knows about and a few hundred organisations actually ship.

The bullish case runs through regulation and one more automotive win. If ISO 21434, the EU Cyber Resilience Act and equivalent regimes start requiring evidence that current practice cannot supply, the value of a machine-checked proof rises sharply relative to a certification package. A second volume automotive adopter alongside NIO would change the ecosystem’s economics materially, because automotive volume funds tooling, support organisations and driver ecosystems in a way defence contracts do not. Apple’s Foundation membership and 2026 gold sponsorship is the wildcard: if Apple ships seL4 at consumer scale, everything about the project’s position changes overnight — and there is no public evidence that it will.

The bearish case is not technical. The proofs are sound and the performance is real. The risks are the funding concentration in three national agencies plus one defence prime, the expertise concentration in one small company and one university group, the pattern of Premium members joining in 2021 and quietly disappearing by 2026, and the possibility that the ecosystem above the kernel never matures enough to make adoption economic for anyone without a defence budget. seL4 could remain permanently excellent and permanently marginal. Australia’s 2021 decision showed how fast institutional support can vanish.

Several questions the current evidence cannot settle are worth stating as questions rather than guesses.

Can time protection be proved on real hardware? The theory exists, the mechanisms are measured, the formalisation was demonstrated at FM 2023 — and the augmented ISA it requires is not satisfied by any mainstream processor, with the x86 prefetcher residual as the concrete counterexample. This may require hardware that vendors have no commercial reason to build.

Will verification scale to the trillion configuration combinations PROVERS targets? Going from 13 to 90 per cent of Arm platforms in a year suggests the approach generalises. Whether it reaches the full combinatorial space of build options is unproven.

Does Apple use seL4 in a shipping product? Gold sponsorship and a summit programme co-chair is real commitment. Nothing has been published about a product.

What happened to the 2021 membership cohort? Google, Li Auto, Horizon Robotics, Jump Trading, TII and SpacemiT all announced and are all absent, with no exit announcements and a roster mid-migration. Administrative lag and strategic retreat look identical from outside.

Can seL4’s assurance argument be made certifiable at reasonable cost? The 2026 summit panel on certification suggests the ecosystem now considers this an open question rather than a solved one, and it is the question most likely to determine whether seL4 wins business in aerospace and automotive at scale.

And does the record hold? Seventeen years, zero functional-correctness defects in verified code. That is the strongest empirical claim in systems software and the one that would be most damaging to lose. Nothing about a proof guarantees it continues — only that if it breaks, the break will be in an assumption rather than in the reasoning, and the assumption list is published for anyone who wants to look for it.

Questions engineers and buyers ask about seL4

Author:
Jan Bielik
CEO & Founder of Webiano Digital & Marketing Agency

This article is an original analysis supported by the sources cited below

The seL4 Microkernel Official project home, source of the “world’s most highly assured and fastest operating system kernel” positioning and the index to all verification and performance material.

seL4 Proofs Authoritative statement of what the seL4 proofs establish, covering functional correctness, binary correctness, integrity, availability, confidentiality and capDL initialisation.

seL4 Proof Assumptions The project’s own enumerated list of proof assumptions, including the excluded assembly and boot code, DMA, cache and TLB management, and the acknowledged gap on timing channels.

seL4 Verified Configurations Per-architecture matrix of which properties are proved on which platforms, and the exclusions that apply to every verified configuration.

The seL4 Microkernel: An Introduction Gernot Heiser’s Foundation whitepaper, source of the capability model description, the MCS design rationale, the IPC comparisons against Fiasco.OC, Zircon and CertiKOS, and the statement that time protection is not covered by the proofs.

seL4 Frequently Asked Questions Current kernel source and binary sizes per architecture, IPC performance answers, and the official positions on virtualization, SMP and MCS.

seL4 History Project timeline from the 2004 start of L4.verified through the 29 July 2009 completion of the functional correctness proof, the 2014 open-sourcing and the 2020 Foundation launch.

seL4 and Certification The Foundation’s argument comparing its proofs against Common Criteria EAL levels, ISO 26262 ASIL-D and DO-178C Level A, including the caveat on Isabelle/HOL tool qualification.

seL4 Performance Continuously regenerated sel4bench results for IPC call, IPC reply, notify and IRQ invoke across Armv7, Armv8, x86-64 and RV64, in default and MCS configurations.

seL4 16.0.0 Release Notes The July 2026 release, recording the MCS RISC-V verification milestone, Raspberry Pi 5 and Cortex-A76 support, and the x86-64 VM-escape security fix.

seL4 15.0.0 Release Notes The March 2026 release introducing runtime domain-schedule configuration under RFC-20 and optional thread-local IPC buffers.

seL4 14.0.0 Release Notes The November 2025 release stating that all Arm platforms supported by seL4 now have a verified configuration.

seL4 Supported Hardware Full platform matrix across Arm, x86 and RISC-V, with per-platform verification status.

seL4 Microkit User Manual Reference for protection domains, channels, memory regions, protected procedure calls, system description file syntax and the framework’s hard limits.

seL4: formal verification of an OS kernel Klein et al., SOSP 2009 — the original functional correctness result, with the 8,700-line C kernel and the refinement chain from abstract specification to C.

Comprehensive Formal Verification of an OS Microkernel Klein et al., ACM TOCS 2014 — the consolidated account of the proof stack, effort figures and proof maintenance costs.

seL4: Formal Verification of an Operating-System Kernel Communications of the ACM version of the 2009 result, the most accessible primary account of the proof method.

seL4 Enforces Integrity Sewell et al., ITP 2011 — the integrity and authority confinement theorems, their well-formedness assumptions, and the 10,500-line proof cost.

seL4: from General Purpose to a Proof of Information Flow Enforcement Murray et al., IEEE Symposium on Security and Privacy 2013 — the intransitive non-interference proof and its full list of configuration restrictions.

Translation Validation for a Verified OS Kernel Sewell, Myreen and Klein, PLDI 2013 — the graph-language method, SMT solver results at -O1 and -O2, and the removal of the compiler from the trusted computing base.

Time Protection: The Missing OS Abstraction Ge, Yarom, Chothia and Heiser, EuroSys 2019 — cache colouring, kernel cloning, flush latencies, overhead measurements and the measured channel bandwidths before and after mitigation.

Can We Prove Time Protection? Heiser, Klein and Murray, HotOS 2019 — the augmented ISA hardware-software contract required to make timing channels provable, and why mainstream processors do not satisfy it.

Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems Sison et al., FM 2023 — the machine-checked Isabelle formalisation of time protection as an observer-relative intransitive nonleakage property.

L4 Microkernels: The Lessons from 20 Years of Research and Deployment Heiser and Elphinstone, ACM TOCS 2016 — the origin of the “10 to 20 per cent above the hardware limit” claim and the historical IPC cycle counts from L3 onward.

Correct, Fast, Maintainable — Choose Any Three! Blackham and Heiser, APSys 2012 — the fastpath measurements showing carefully written C matching hand-written assembly at 200 cycles.

Fast, Secure, Adaptable: LionsOS Design, Implementation and Performance Heiser et al. — the LionsOS design principles, the networking benchmarks against Linux on Arm and x86, driver code-size comparisons and the IPC-sensitivity experiment.

seL4 Device Driver Framework sDDF architecture, the strict separation of data, metadata and control regions, supported device classes and the throughput and CPU-utilisation results against Linux.

LionsOS documentation Current LionsOS documentation, release status and the published short-term and long-term roadmap.

Time Protection project Trustworthy Systems’ status page for verified time protection, the RISC-V fence.t instruction work and current Cyberagentur-funded activity.

DARPA HACMS case study DARPA’s own account of the High-Assurance Cyber Military Systems programme, the Unmanned Little Bird red-team results and the transition to convoy trucks and satellites.

Formally Verified Software in the Real World Communications of the ACM account of the HACMS retrofit, the white-box red-team conditions and the February 2017 in-flight attack on the Little Bird.

Formal Verification Creates Hacker-Proof Code Quanta Magazine’s reporting on the six-week Little Bird red-team engagement and the wider formal-methods programme.

SMACCM project Trustworthy Systems’ record of the 18-million-dollar SMACCM project, its partners, the SMACCMcopter and the ground-vehicle transition platforms.

DARPA PROVERS Programme description for Pipelined Reasoning of Verifiers Enabling Robust Systems, the funding vehicle behind the platform, MCS and Rust verification work.

Proofcraft news 2026 Primary record of the 29 June 2026 MCS RISC-V functional correctness milestone and the 1 June 2026 verified dynamic domain scheduler.

Proofcraft news 2025 Primary record of the April 2025 AArch64 integrity proof, the Cyberagentur multikernel funding and the Arm platform coverage results.

seL4 news Dated Foundation announcements covering releases, verification milestones, membership changes and the December 2025 transition to Swiss incorporation.

The seL4 Foundation Governance structure, the Governing Board and Technical Steering Committee, and the Foundation’s status as the Swiss association seL4 International.

seL4 Summit 2025 abstracts Talk abstracts including the platform verification coverage results, binary verification deep dive and the Atoll multikernel hypervisor.

RISC-V International and seL4 Foundation announce new security milestone The May 2021 announcement of binary verification for seL4 on 64-bit RISC-V, funded by HENSOLDT Cyber.

SkyBridge: Fast and Secure Inter-Process Communication for Microkernels Mi et al., EuroSys 2019 — independent round-trip IPC measurements placing seL4 at 396 cycles against Fiasco.OC at 2,717 and Zircon at 8,157.

Verified software can and will be cheaper than buggy stuff Gernot Heiser’s cost analysis, source of the sub-400-dollar-per-line figure and the comparison against unverified and EAL6-class alternatives.

Shedding Light on Static Partitioning Hypervisors for Arm-based Mixed-Criticality Systems Martins and Pinto — independent measurement of seL4 CAmkES VMM virtualization overhead, interrupt latency and trusted computing base size against Jailhouse, Xen and Bao.

Data61 dismantles research group behind seL4 secure OS Reporting on the May 2021 CSIRO restructure that disbanded Trustworthy Systems and the UNSW funding that preserved the team.

NCSC joins the seL4 Foundation The UK National Cyber Security Centre’s February 2022 announcement of membership and its funding of proof work at UNSW and Proofcraft.

NIO IN 2024: chip, SkyOS, phone and more Reporting on NIO’s July 2024 launch of the SkyOS vehicle operating system and the in-house 5-nanometre NX9031 autonomous driving chip.

Riverside Research acquires Cog Systems The March 2025 acquisition of founding Foundation member Cog Systems and the continuation of its high-assurance virtualization work.

seL4 use cases The Foundation’s own list of deployed seL4-based products, including SkyOS-M in the ONVO L60, Kry10 KOS, MEP SureVoice Solid and Neutrality’s Atoll.

l4v proof repository The Isabelle/HOL proof source, containing the abstract and executable specifications, the refinement and invariant proofs, the C parser, AutoCorres and the assembly refinement framework.

This article was prepared with the assistance of artificial intelligence tools. The content underwent expert human review, and Webiano Digital & Marketing Agency assumes editorial responsibility for its final version and publication.