seL4 Summit 2026 Abstracts

The emergence of formally verified building blocks across the stack, from memory-safe languages toverified microkernels like seL4, represents a hard-won foundation. But it raises a deeper challenge: local correctness does not translate to system reliability. Each component may behave exactly as proven, while the system as a whole remains unpredictable.

This talk introduces Software Understanding as a new discipline: the science of formally verifying that software-controlled systems perform correctly across normal, abnormal, and hostile conditions, and making that reasoning legible across the teams responsible for them. As critical infrastructure becomes increasingly autonomous and AI-driven, the gap between what we build and what we can reason about continues to widen. Closing that gap requires more than proof; it requires bringing mathematical rigor into the pace and complexity of real-world operations.

Drawing on lessons from national security and mission-critical systems, this talk examines what it will take to move formal methods from technical scripture to organizational discipline, and why verified microkernels like seL4 are not the end of the story, but the beginning.

For most of its history, formal methods has been a discipline of proof rather than product: rigorous, powerful, and largely confined to academia. That is changing rapidly. I'll argue that FM is finally ready to deliver secure, resilient systems in the real world, and that the obstacles left are largely self-inflicted: a history of over-promising, tools that are painful to use and barely interoperate, and a habit of staying in the lab rather than supporting customers through real, evolving deployments.

Drawing on systems we're building today for a wide range of government and commercial partners, I'll make the case that security is fundamentally an economic argument rather than a quest for perfection: the goal is to make attacking a system so costly that adversaries focus elsewhere. Reaching that at scale depends far less on stronger proofs than on ruthless attention to wider adoption: on meeting real customers in the messy, changing environments they actually deploy into.

Regardless of your views on AI, it is rapidly lowering the barrier to entry. I'll show — not just tell — what becomes possible when modern AI is combined with formal tools and seL4. This is a talk for anyone who wants formal methods to matter beyond academia.

The formal methods community has made great progress in the past two decades to mature mathematically-precise techniques in order to tackle real-world design and analysis problems. In areas as diverse as hardware design, finance, systems engineering, software development, and law, increasingly the question is not, “Why would you use formal methods?” but rather “Why wouldn’t you?” With the assistance of powerful generative artificial intelligence agents, the barriers to entry for the use of formal methods tools are falling fast -- even mathematicians are now using proof tools. In this talk, we will detail a number of leading-edge tools and techniques that are enabling formal methods to be successfully applied in a number of critical real-world domains. We will also highlight the application of practical formal methods in a number of current government-sponsored Science and Technology initiatives, such as DARPA's Resilient Software Systems effort. We will also describe the Software Understanding initiative, which combines the rigorous practice of constructing (forward understanding) and assessing (reverse understanding) software-controlled systems in order to verify their functionality, safety, security, and reliability. Finally, we will reflect on the impact that these advances in real-world formal verification can have on the seL4 ecosystem.

This talk will provide an overview of the seL4 microkernel and its ecosystem, as an introduction to anyone new to the community and to the seL4 summit, and as a refresher and update to existing players. The aim is that everyone is set to follow the rest of the event and contribute to discussions.

The talk will cover what seL4 is, why its formal verification and security properties make it a key platform for high-assurance systems, who is using and contributing to it across industry, academia, and government, and where it is being applied today. It will provide pointers to who to connect with and where to learn more.

The UK’s National Cyber Security Centre first started looking at seL4 and its formal security guarantees in 2016. Over the last ten years, we have worked on numerous projects with the goal of using seL4 to help us in our mission to make the UK the safest place to live and work online. We will talk about our early efforts understanding seL4’s security guarantees and how they map onto our assurance processes for security systems. From those early investigations, we will talk about how we view emerging technologies and how these considerations led us to invest in the seL4 ecosystem. Focussing on real world deployments of seL4, we’ll lift the curtain on several projects we’ve been working on over the last few years building products and systems based on seL4.

The aim for this talk will be to provide insight and feedback on the process of seL4 adoption, including views from industry on the design and deployment of real world products based on the technology. Finally we will talk about where we think seL4 based components fit in the landscape of secure system design and speculation on what the future might hold for seL4 and the NCSC.

As a step toward building safety certified systems on the seL4-based Kry10 OS (KOS) we have developed a Software Safety Manual for KOS. This safety manual provides procedures and guidelines for using KOS and its features to develop safety critical systems in such a way that they could be certified.

In general, such systems consist of some core functionality (e.g. run a machine) and some safety-related functionality (e.g. stop the machine if a person is too near). The safety-related functionality is “safety critical”, which means that the systems that implement it should be resistant to failure, even in the presence of known and unknown hazards. Software safety certification is concerned with providing assurance that the risk of these safety-related systems failing has been reduced to an acceptable level.

In a KOS system much of that assurance can be gained from the isolation provided by KOS and the underlying, formally verified, seL4 microkernel. Additional assurance is gained from KOS features such as process supervision, process start and restart, process supervision and monitoring, process resource management, etc. Our safety manual walks through the process of creating a safety-related system and then ensuring that the safety functionality is itself safe. The steps for doing this are: 1) develop the core functionality; 2) develop the safety-related functionality; 3) protect the safety-related functionality from hazards including: memory corruption, process corruption, faulty inputs, faulty outputs, etc.

In this presentation we will discuss and describe this process, illustrating with concrete examples how it can be applied to real working systems.

In an increasingly connected world, cybersecurity is no longer just a technical feature, it is a fundamental legal requirement for market access. The EU’s Cyber Resilience Act (CRA) is set to reshape how digital products are designed, developed, and maintained by introducing strict mandatory cybersecurity standards and incident reporting obligations for manufacturers. But beyond the dense regulatory text, what does this actually mean for your business?

Drawing on real-world testing and compliance experience at SafeShark, this session cuts through the legal jargon to deliver a clear, actionable overview of the CRA. We will explore the core requirements of the Act, how it impacts the entire lifecycle of hardware and software products, and the critical timelines you must meet ahead of the 2027 enforcement deadline. Whether you are a business leader, product manager, or developer, you will leave with a pragmatic understanding of how to navigate these new rules, avoid costly penalties, and ensure your connected devices are secure, compliant, and ready for the European market.

In this talk I will report on my contributions to add “Formal Verification” as a requirement to mitigate security risks in the new European Harmonised standards, in the context of the Cyber Resilience Act (CRA). Namely, I have submitted 3 contributions to the Operating System harmonised standard, and all three contributions have now been accepted. The standard is still in the finalisation process, but so far no changes have been requested on my contributions.

The Cyber Resilience Act (CRA) is a regulatory framework of the European Union (EU) for hardware and software products that are made available on the EU market. The CRAentered into force in December 2024 and will be fully applicable as of December 2027, with some provisions starting to apply earlier. During that time, the EU has commissioned European standardisation bodies (namely CEN, CENELEC, and ETSI) to define so-called “harmonised standards” for the CRA. Using a harmonised standard gives a “presumption of conformity”, meaning any product that follows the standard will be assumed by the authorities to comply with the CRA’s legal requirements.

For the CRA, the EU has requested the development of 41 harmonised standards, split into horizontal standards (which apply across all products) and vertical standards (product-specific). One of the vertical standards being developed is specific to Operating Systems (standard number EN-304-626). Each standard defines a list of requirements, and proposes a list of mitigations to address these requirements.

Before my contributions, Formal Verification did not appear at all in the OS standard (and most other standards). This had 2 major implications. Firstly, it meant that the standard was not pushing for what is today the demonstrated highest assurance for critical software, with practical and effective impact. For seL4, this meant that being formally verified would not differentiate it from other OSes with lower assurance, when it comes to being compliant with EU regulations. Secondly, it meant that the effort spent on formal verification would actually be penalised. Indeed, a formally verified product, to be compliant, would still require additional effort to produce lower assurance evidence, such as being checked for memory errors using a source code analysis tool, or being implemented in a memory safe language.

My contributions consist of 3 new mitigations where Formal Verification shall be used to establish: (1) functional correctness; (2) integrity; and (3) confidentiality. With these additions to the OS standard, the CRA will be more in-line with the state-of-the-art approach to cyber resiliency, and seL4’s unique differentiator can continue to be a key advantage for a more secure software world.

MIT Lincoln Laboratory and the Space Cyber-Resiliency group at Air Force Research Laboratory-Space Vehicles Directorate (AFRL/RV) have created a software platform called Cyber-Hardened Satellite Software (CHSS). “CHSS is a mission-agnostic spaceflight software platform whose functionality was inspired by NASA’s core Flight System but with an emphasis on cyber-resiliency. Most notably, CHSS offers security without sacrificing performance.”1 CHSS utilizes Magnetite, which is a secure OS built on top of the seL4 Microkernel. Magnetite and CHSS components are written in Rust, which provides memory safety and type safety at the OS and application level. This stack provides a safe and secure foundation to create cyber-resilient satellite systems.

Adoption of new technologies, especially ones such as CHSS which are a paradigm shift in the way things have been done for satellites, can be quite difficult. AFRL/RV recognized that adoption should be made incremental to have the fastest transition. DornerWorks is working on a Phase II SBIR from SPACEWERX that addresses this in 2 ways:

1. Update VM Composer to target CHSS systems to make system configuration much simpler.

2. Write a VMM in Rust for CHSS to allow a VM to host legacy software which can be incrementally ported to CHSS.

VM Composer is a GUI tool for defining virtualized systems on top of seL4. By adding CHSS awareness to the tool, the manual steps for system integrators and developers can be significantly reduced. VM Composer is a way to visualize a system and architect security appropriate for mission risk acceptance.

The VMM provides a way to run the entire legacy code in a sandbox. It can be adapted to communicate with the overall CHSS system and then each app that needs to be cyberhardened can be ported over to CHSS and removed from the VM, one-by-one. Most importantly, the developer has a fully functional system at each step, allowing for incremental launches and deployments as the software is hardened. It also allows for lower criticality software to remain in the VM for deployment.

This talk will give further background on CHSS, discuss the progress that has been made in the two major tasks, and further discuss the iterative porting process of legacy satellite flight software and/or mission software.

The Throwbot® 3 Robot by ReconRobotics is a ruggedized, throwable micro-robot designed for rapid and covert reconnaissance in high-risk and dynamic environments. It is used by law enforcement and military personnel for real-time intelligence gathering, situational awareness, and remote investigation under control of a remote operator. Their light weight makes them ideal for many forward situations, but also vulnerable to being commandeered, carried off, and dissected.

Building on past and current work this talk will explain how seL4 can be used to increase the security posture of the underlying platform, further harden the control path, and add additional protections against the exfiltration of sensitive data. Following this overview, a demonstration of the modified system using seL4 will be given.

The Robot Operating System (ROS) is widely adopted on various robotic platforms, including military robotic ground vehicles. However, it was not designed for performance and determinism requirements or for the safety and security required for the execution of critical missions. The Robotic Technology Kernel (RTK) is a ROS-based autonomy software library for S&T development that provides a set of common robotics capabilities across a variety of Army platforms. This RTK-over-ROS-over-Linux stack possesses the large resource overhead and attack surface manifested by Linux and its software applications such as ROS; hence an attacker may use a known vulnerability for Ubuntu to gain a footprint on the vehicle, causing disastrous consequences (e.g., crash). Unfortunately, unmanned ground vehicles, when running ROS, fundamentally lack the necessary security, resilience, and performance.

To tackle this challenge, Trusted ST is developing the Assured Robotics Embedded Systems and Applications in Ground Vehicles (ARSENAL) solution. The ARSENAL effort will result in a modular, open, and secure ROS2 stack (newer version of ROS that contains RTK) on military embedded platforms that will have the following capabilities.

• Enables multiple design and configuration options over the seL4 microkernel (as a separation kernel to provide software-level isolation) to support various platform resources and mission requirements (e.g., latency, space, throughput, etc.), which will significantly improve interoperability and configurability. ARSENAL can support the conventional ROS2 configuration with reduced attack surface (Option 1 with DDS and minimized Linux kernel on seL4), and minimized configuration (Option 2, DDS/ROS2 on seL4) to run mission applications with minimal platform resource requirements.
• Ports mission essential application modules over simplified DDS/ROS2 (Option 2) by leveraging ROS2/DDS interoperability and analyzing software dependencies, resource/performance requirements, and mission needs. The ported robotics application maintains mission critical functionalities (e.g., tele-operation) and eliminates non-mission critical functions (e.g., visualization) to reduce size and memory/latency overhead while fully leveraging DDS/ROS2 compatibility and supporting cross-platform, cross-controller capabilities.
• Provides strong security services and checks, including memory separation and process isolation, data flow monitor, intrusion detection, and policy enforcement to thwart known and unknown cyber vulnerabilities as applicable and needed in DoD use cases, including teleoperation, autonomy, and swarm.
• Enables secure inter- and intra-communication by providing cryptographic solutions on top of the open data transport layer (e.g., inter-process communication, or IPC, and data distribution service, or DDS). All data exchanges among multiple robotic applications within a platform and between external platforms can be encrypted with TLS to significantly increase the level of data and information protection.

We have performed design analyses and made design decisions; developed a proof-of-concept of running ROS2 in reduced OS (Option 1); and developed a proof-of-concept of running native ROS2 with DDS (Option 2). We will further develop and mature the technology, comprising four main thrusts: (1) completing the integration of DDS and ROS2 on top of seL4; (2) developing security capabilities; (3) upgrading software and tooling that includes transition from CAmkES to Microkit; and (4) performing capability demonstration.

The ARSENAL solution (1) takes advantage of open-source ROS2 and seL4 for cost-effective development and adoption, and (2) fully utilizes the deployed ROS2 stack in various UGVs for easy deployment and interoperability. ARSENAL will provide unprecedented, holistic security and resilience for Army UGVs, and therefore fundamentally improve the state of the art of the various autonomy stack and capabilities. Due to its open, modular, and standard-based design and implementation, the ARSENAL stack can be deployed on many unmanned systems to protect mission critical assets with minimal configuration changes.

We will present our seL4 experience and applications to build security and resilience for these unmanned systems in the real world, and therefore the talk proposal fits the scope of the seL4 Summit.

ABB develops protection and control systems for safety-critical infrastructure in energy and transportation sectors. These systems operate under hard real-time constraints, require security and safety assurances, and incorporate legacy software developed over decades by multiple teams across heterogeneous operating systems. Recently, regulatory requirements like the EU Cyber Resilience Act [1] demand timely and continuous software updates over long system lifetimes. This poses numerous challenges for the platform architecture and certification strategies.

The presentation reports on experiences gained while evaluating a mixed-criticality platform based on seL4 [2], [3]. The focus is on consolidating hard real-time, safety-critical protection and control functions with non-critical services on shared hardware, while preserving determinism and isolation. An architectural mechanism is also presented that enables software updates of non-safety-critical components without violating the isolation, timing, and trust assumptions of certified functions. This supports regulatory compliance while minimizing recertification effort. Based on this experience, the presentation discusses lessons learned, limitations, and open challenges encountered when implementing seL4 for such real-time, secured, and legacy-driven protection and control systems.

[1] Council of the European Union, “Regulation (EU) 2024/2847.” 2024. Available: https://eur-lex.europa.eu/eli/reg/2024/2847/oj

[2] G. Klein et al., “seL4: Formal verification of an OS kernel,” 2009.

[3] Z. Kocsis, M. Paturel, S. Isitha, T. Weibel, and G. Heiser, “The Sel4 Microkit,” 2023.

The demand for software-defined systems among businesses is growing rapidly. The software-defined paradigm has been known since the 1990s, originating in the telecommunications industry with software-defined radio. Since around 2021, innovation in the automotive industry has focused on implementing the software-defined vehicle paradigm. This led to the creation of COVESA, and in Europe, automakers and suppliers joined forces in the Eclipse Foundation for SDV. Other industries seeking to accelerate innovation in safety-critical systems—such as manufacturing, the defense industry, and aerospace—are now following this model.

Microkernels are well-suited as a central building block for implementing the Software-Defined Paradigm, as demonstrated annually at the seL4 Summit and reflected in over 275 million cars equipped with BlackBerry QNX.

To enable various industries to implement the Software-Defined Paradigm, Fraunhofer IESE is researching a reference architecture called: tSDX – trustworthy Software Defined X. The “tSDX” research project has been funded by the German Ministry of Research since May 2026 and initially aims to define an instantiable reference architecture with microkernels as its central building block. In a practical, application-oriented manner, requirements and architectural drivers from the defense industry, aviation, aerospace, and manufacturing are being gathered with the consortium. The reference architecture is intended to be vendor-neutral (microkernel-independent) and is currently still under development.

This presentation aims to convey initial insights and interim results. Furthermore, the presentation seeks to bridge the gap to practical application and present the needs and pain points of industrial applications to the participating microkernel experts.

seL4’s flagship proof is functional correctness, which states that the C code behaves according to its abstract specification. This talk introduces the next layer in the assurance stack– seL4’s security proofs. We will present an overview of what they are, how they are structured, and where they fit into past, present, and future work at Proofcraft.

The CIA triad of properties– confidentiality, integrity, and availability– is the foundation of information security, and the target of seL4’s security proofs. These proofs establish that seL4’s specification, and by extension its implementation, prevents an application running on top from: modifying data without authorisation (integrity); interfering with another application’s resource access (availability); and learning information without authorisation (confidentiality). Together, the three guarantee isolation between applications in critical systems, preventing attacks and bugs in non-critical components from propagating to critical ones.

As part of a broader push towards a full proof stack for seL4 on 64-bit Arm, we recently extended the security proofs to AArch64. Among other architectural differences, this introduced two objects that were new to seL4’s security proofs: VCPUs, which provide virtual CPUs to guest operating systems under a hypervisor, and FPUs, which enable perthread floating point operations. Unlike other objects in memory, the contents of VCPUs and FPUs are loaded into physical registers whose contents may persist between context switches. This introduces new complexity in a security context, and required novel proof techniques to accommodate them.

This talk will give an overview of the (systems) research and development activities at UNSW Sydney’s Trustworthy Systems (TS) group. It will provide the context for the other TS talks that follow, and will provide details of the activities not covered by separate talks, including:

• Microkit, driver framework and LionsOS progress
• performance analysis of the seL4 SMP kernel vs the multikernel
• re-establishing seL4’s worst-case execution time (WCET) analysis for the 64-bit MCS kernel on RISC-V
• establishing sound instruction-latency bounds for WCET analysis
• work on a clean model for IOMMU support
• ... and whatever exciting things that happened in the meantime.

Updates on verification work will be provided by Miki Tanaka and Rob Sison in their talks.

This talk will give an update on the past two years’ advances at Trustworthy Systems in (1) our ongoing efforts to verify time protection for seL4, as well as (2) our implementation in seL4 of new time-protected cross-domain communication mechanisms on RISC-V Cheshire. On the formal verification front, I will present our results so far, thanks to a crucial rethink of our approach to verifying a key aspect of time protection for seL4 down to its C implementation, which has eliminated the main cause of the project’s previously large number of breakages to seL4’s existing correctness proofs. On the OS kernel design and development front, I will present both legacy and hardware-supported implementation options we evaluated for seL4 to support cross-domain shared memory and notification mechanisms that ensure one-way communications are truly one way, without permitting any timing channels in either (but most importantly, the backwards) direction. I will also remark on where we stand and next steps forward to formalise and verify that time protection is enforced by these new mechanisms.

Pancake is a verification-friendly, imperative low-level language for systems programming, which the Trustworthy Systems group at UNSW has been working on to produce verified LionsOS components. Since first introduced in 2024 seL4 Summit, TS continued with Pancake development and Pancake is now mature enough for our systems engineers to take up and port various components originally written in C to Pancake.

In this talk, we report on various recent updates on Pancake and its roadmap, in the broader context of LionsOS. We’ll cover the progress and plans for the general Pancake language extensions and compiler improvements as well as verification of programs written in Pancake, in particular device drivers, both via interactive theorem proving and SMT-based tools.

We’ll highlight the SMT-based approach via Pancake-to-Viper transpiler as a way towards TS’s vision of making verified software the standard for security- and safety-critical systems, aiming to make software verification more scalable and less expensive.

While sDDF provides a framework for verification of new drivers with the Pancake language, and driver synthesis, the vast majority of current systems relies on proprietary hardware, and existing drivers written in C.

In our project with DORNERWORKS we were tasked with verifying an ethernet driver for a deployed system. The ethernet device was similar to Intel e100 hardware. Given the relatively new sDDF framework and Pancake language, and the tight project timeline and budget constraints, we decided to verify an already existing driver, with CN verification tool.

CN was developed by The REMS group at University of Cambridge, and significantly matured during the PROVERS project. CN targets the C language, and lets users specify properties for the functions.

We were able to verify both the driver and a device model reverse engineered from the Intel driver datasheet. We had to stub out the seL4 system calls, including minimal specifications.

We believe this contribution bridges the gap between legacy drivers, and the future where drivers are synthesised and guaranteed to be correct.

Device drivers are a major source of bugs in operating systems, making them a primary target for formal verification. However, many of these bugs come from violations of the device’s protocol or faults in the device’s design, which cannot be prevented without a formal model of the device’s protocol. Such a model would traditionally be derived from the device’s datasheet, but the accuracy of this is limited, as datasheets are often incorrect and/or incomplete.

In this talk, we discuss how we leverage our open-source RISC-V SoC, Serengeti, to extract formally verified specifications from devices’ Verilog implementations, simultaneously establishing the absence of device faults. We also cover aspects of our application of these specifications to the verification of sDDF device drivers written in Pancake, with the goal of establishing end-to-end correctness.

In prior work, we have verified the correctness of a C implementation of UDPv6 using AutoCorres2, a tool to facilitate the verification of C programs in Isabelle/HOL. To achieve high performance, it is common practice for implementations of such network layers to make repeated small mutations to heap state, using typed pointers with overlapping address ranges. This approach to network implementations presents additional challenges for the verification efforts.

In this talk, we describe some of these challenges and present our solutions. First, rather than showing direct refinement to a high-level specification, we prove important invariants at the level of the C specification—a monadic representation of the C code generated by AutoCorres2. Second, we analyze pointer aliasing manually. Third, we generalize some of our lemmas both to simplify proofs of the UDPv6 implementation but also to use them towards proving properties about other layer implementations. Fourth, we refactor code where appropriate, while preserving performance, to simplify our proofs. Finally, we describe how we use these invariants to show refinement.

The seL4 Microkit has a problem: composing systems becomes very difficult when working with modular code or large code bases. The Microkit Acacia tool (formerly SDFgen) solves this problem by offering a higher-level abstraction for generating Microkit system files, capable of inserting modules with minimal effort. Acacia has been used extensively as a component of LionsOS and the seL4 Device Driver Framework (sDDF), simplifying integrating systems with multiple driver subsystems or high-level LionsOS components like filesystems or the firewall. Recently, Acacia has been re-implemented in Python for greater ease of use.

This talk will introduce the community to Acacia with a focus on newly added features which simplify build-time configuration and specification of large systems. We will cover the basics, starting with simply connecting a few programs together, and then demonstrate how to add subsystems such as sDDF driver stacks. We will conclude with a tutorial demonstrating how to convert freestanding work into a Acacia subsystem for future reuse, giving an overview of the architecture of the tool.

In its current form, the initialization code of the seL4 kernel dictates the policy of how resources are discovered and what capabilities are created at boot time, making it hard to integrate into existing boot infrastructure. Wepropose to delegate this policy to a pre-boot component and introduce both an interface and mechanisms for pre-boot infrastructure to communicate resources to the kernel and userspace. Not only does this pave the way for booting seL4 in a multikernel configuration where not all the nodes use the same resources, it also provides a cleaner separation between verified and unverified code.

Contrary to the rest of the design of seL4, the boot code makes several policy decisions. On x86 for example, the kernel expects to be booted in protected mode. This is the case when loaded with GRUB. All modern server platforms have an EFI pre-boot environment, which leaves the CPU already in long mode (Intel-speak for 64bit mode). On Arm platforms the physical memory regions are extracted from a device tree at compile time. While device trees are the standard for embedded systems, Arm server platforms also use EFI, which provides a memorymapthatisonlyknownatruntime. Thingswillget even morecomplicated with partitioned multikernel configurations, where the resources of the nodes need to be disjoint, and the global memory map provided by the firmware does not have enough information for the kernel to create the right capabilities. In such a setting, there will also be shared frames that userspace components use to communicate between cores. These are resources that the kernel does not touch but should just be passing to userspace. Currently, the seL4 ecosystem does not have a mechanism to pass resources at addresses that are not statically known to userspace.

One could of course add support to the kernel for all these cases that currently are not covered. We however argue, that like any other policy, a microkernel should not make these decisions but offer a mechanism that is general enough to cover all potential use cases. We therefore propose to remove all code that decides which resources are used by the kernel and what capabilities are created from the initialization of the kernel. Instead, the kernel should be getting this information from a pre-boot environment that can be tailored to specific use cases. We therefore propose a boot protocol where the kernel expects to be handed a resource map. To cover the case of pre-boot allocated resources that need to be passed to userspace, we propose to add support for named resources to CapDL. A statically created specification can e.g., specify a specific slot in a CSpace to be populated with a capability to such a resource. The rootserver will then get a mapping from these names to CPointers from the kernel and can distribute the capabilities accordingly.

An additional benefit of this approach is that the clear interface between the verified kernel and the pre-boot interface makes it easier to specify what the state is that the kernel expects to be booted in. By shipping default pre-boot environments that recreate the current initialization code, the transition to making seL4 an even more versatile tool than it already is, can even be seamless.

seL4, the world’s first formally verified microkernel, has demonstrated exceptional reliability in security- and safety-critical systems. However, its use in large-scale, server-class environments remains underexplored, especially for dynamic workloads such as microservices.

In this talk, we present Carrels, a secure and high-performance platform for lightweight, dynamic applications on seL4. Carrels explores whether seL4 can serve as a practical foundation for microservice-style workloads, which require strong isolation together with dynamic deployment, destruction, and migration at runtime.

Carrels is built on LionsOS, a highly modular, high-performance seL4-based operating system designed with formal verification in mind. In Carrels, microservice applications are encapsulated in a prototype container abstraction: a secure isolation domain whose lifecycle can change dynamically. We implement this abstraction using LionsOS modules, demonstrating how a largely static seL4-based system can be extended into a semi-dynamic platform for dynamic applications.

We will present the design and implementation of Carrels, including its security model, container lifecycle management, and resource management. We will also share preliminary performance results, showing that Carrels can support microservice workloads with low overhead while preserving strong isolation guarantees, including small trusted computing base and fine-grained access control.

Riverside Research presents an seL4 prototype called SKMS: Single Kernel Multicore seL4. SKMS is a proof-of-concept implementation of a previously proposed multicore microkernel architecture [1] for seL4 microkernel on x86. The current POC implements three basic elements of seL4 functionality: memory isolation, remote system calls, and remote scheduling. Memory isolation puts usperspace processes into address spaces with no mappings to the seL4 kernel, remote system calls forward requests from these processes (loaded on other cores) over to the single kernel core, and remote scheduling allows the kernel scheduler to choose processes for the remote cores. A preliminary design idea for leveraging this architecture in “proving” a version of seL4 that can schedule processes across many cores is presented for community feedback.

[1] Scott Brookes and Stephen Taylor. 2016. Rethinking operating system design: asymmetric multiprocessing for security and performance. In Proceedings of the 2016 New Security Paradigms Workshop (NSPW '16). Association for Computing Machinery, New York, NY, USA, 68–79. https://doi.org/10.1145/3011883.3011886

Historically, open-source Virtual Machine Monitors (VMMs) built on seL4 have focused largely on Linux guest OS support. Booting a closed-source operating system like Windows on a custom x86-64 VMM introduces a unique set of development hurdles.

This talk details the engineering effort behind LionsOS to achieve a fully functional x86-64 VMMcapable of running modern Windows and desktop Linux distributions. We will explore the technical realities of this architectural leap, focusing on the distinct challenges encountered when virtualising Windows. Specifically contrasting the predictable boot process of Linux with the strict firmware assumptions and opaqueness of a Windows guest.

Beyond the boot sequence, we will unpack how we tackled these hurdles, detailing the low-level virtualisation and driver solutions required to make this work.

The talk will conclude with a live demonstration of LionsOS successfully booting into a functional Windows desktop environment.

The Collins Aerospace INSPECTA project (part of the DARPA PROVERS program) aims to provide a model-based development tool chain for seL4 with integrated formal methods. The High Assurance Modeling and Rapid engineering for embedded systems (HAMR) framework, whose development is led by researchers at Kansas State University, is a key part of the INSPECTA tool chain. HAMR supports modelbased development for seL4 via modeling in SysMLv2, code generation to C and Rust, and deployment to seL4 using Microkit and CAmKeS. Key themes of HAMR include component-based development, multiuse formal behavior contracts integrated across models and code that can be used for formal verification, automated testing, and run-time monitoring, and integration with the Collins INSPECTA assurance case framework. On the INSPECTA project, HAMR is being applied to increase the cyber-resiliency of several autonomy platforms, including the Collins Aerospace Rapid Edge mission system.

At the 2025 seL4 summit, I gave an overview of HAMR framework, with an emphasis on its new capabilities for SysMLv2 modeling, Rust code and contract generation, and integration of the Microkit framework for configuring seL4. That talk focused on specification and verification of individual components using component contracts. In this talk, I describe two new layers of capabilities that significantly improve the effectiveness and speed at which seL4-based systems can be developed using HAMR.

First, to improve support for reasoning about component integration and system level reasoning, HAMR model and code generation has been extended to support auto-generation of multiple forms of run-time monitoring including run-time checking of component contracts, system contracts, and checking of Mission Time Temporal Logic specifications using R2U2 framework. Several aspects of this work leverage new capabilities for “user-land” static scheduling of HAMR components (Microkit protection domains) recently added by UNSW to Microkit.

Second, I give an overview of an emerging agent-based engineering framework for HAMR that supports automated development of HAMR models, contracts, component application code, testing and verification, assurance, and reporting tasks. Several INSPECTA teams are collaborating on building out these capabilities. Our team’s contributions have included (a) integration of Model-Context-Protocol (MCP) support for a variety of HAMR modeling, coding, contract verification, and testing capabilities, (b) specification of HAMR process/workflow steps that agents follow to develop HAMR-based systems on seL4, (c) agent skills that support workflow steps, and (d) specification of human/agents interaction points to support design, property-specification and validation, and audits. I summarize my views of the benefits of model-based development and seL4 in the context of agentic development of high-assurance systems, and I describe how KSU contributions are integrating into the broader INSPECTA work on agentdevelopment. I present outcomes of experiments that we have carried out with this framework including the direction and interaction with the system monitoring capabilities listed above as applied to the INSPECTA Open Platform autonomy reference examples.

HAMR is available under an open-source license, and the project website includes an example repository and collection of videos, tutorials, and classroom lecture materials (also suited for workforce training).

While sel4 provides a sound foundation upon which to build, it remains the case that applications can be built that are on their own unsound, insecure and unsafe. The work to develop applications needs rigorous, accessible tool support in order to more quickly build and deploy assured software systems. For decades, formal methods have been acknowledged as a very powerful set of techniques with potential to significantly improve the speed and quality of software deployment but usually requiring the use of rare and often expensive skills to deploy effectively.

For this presentation, we used an open problem statement by Abrial [1] referred to as the ‘Steam Boiler’. The case study was implemented using a team of professional software engineers and commercially supported tools. The presentation will highlight how the Abrial informal specification was used as the basis for the development of a set of System Requirements using structured English and how formalism can be introduced through software requirements, design and code and used as the basis for automatic, independent formal verification. The exploration of desired properties at the requirements level is explored formally. The final aspect discussed is the potential for formal verification of the Executable Object Code exploiting a formalised Instruction Set Architecture in the same graph language used by the sel4 project.

Indeed, the sel4 graph language is also used, at least partially, in automatic verification of source code against design and in design against requirements. The possible claims for certification credit are also discussed. While the example sector is nuclear, we have used a more accessible and more widely understood software standard from the aerospace sector, DO-178C [2], as amended through use of DO-333 [2], the formal methods supplement. A summary of the claims will be provided, including limitations and how tool qualification using DO-330 [4] can be used to support certification. Finally, metrics are presented, including the hours of effort expended on development, verification and an example is given on how quickly changes can be incorporated showing just how agile the techniques are and the consequent impact on time to market could be.

[1] Abrial, J-R.: Steam-Boiler Control Specification Problem. In: Abrial, J-R., Borger, E., Langmaack, H.: (eds.) Formal Methods for Industrial Applications 1996, LNCS State-of-theArt Survey, pp. 500–509. Springer, Heidelberg (1996).

[2] DO-178C: Software Considerations in Airborne Systems and Equipment Certification, Issue C, 13th December 2011.

[3] DO-333: Formal Methods Supplement to ED-12C/DO-178C and ED-109A/DO-278A, 13th December 2011

[4] DO-330: Software Tool Qualification Considerations, 13th December 2011.

seL4 gives user-level systems a great deal of control over hardware resources through capability-protected kernel abstractions. This is powerful, but it also means that performance depends heavily on how user-level resource management is designed.

In this talk, we use physical memory management as a case study. We show that the wrong design can make dynamic memory allocation expensive by placing capability-related operations and metadata bookkeeping directly on the allocation critical path.

We then present a different design: keep the fast path small, and move capability-heavy functions out of the critical path whenever it can be prepared ahead of time or handled asynchronously. We implement this idea in the seL4 library OS and compare it with baseline designs.

The results show that efficient dynamic memory management is practical on seL4, but only if the memory manager is designed to respect the cost structure of capability-based systems.

Performant networking is critical for many practical computer systems. Since 2022, the seL4 Device Driver Framework (sDDF) has included an Ethernet driver capable of strong performance without compromising on trustworthiness. Under LionsOS, the sDDF has been shown to be capable of supporting a variety of intensive use cases such as a firewall and webserver.

In this talk we will discuss ongoing modelling and analysis of the sDDF ethernet class using discrete-event simulation and practical benchmarks. We will present new observations on the dynamic properties of its radically simple design and explore the theoretical limits of the sDDF design philosophy.

seL4’s multicore story has long been built around SMP with a big kernel lock (BKL). For the low-core-count platforms where seL4 was traditionally deployed, this was a reasonable choice: syscall critical sections are short, and BKL was expected to scale well enough.

Our results suggest that this tradeoff should be revisited. Because seL4 syscalls are so cheap to begin with, the cost of in-kernel concurrency control becomes highly visible. We show that SMP with a BKL can add around 50% overhead to critical seL4 operations.

In this talk, we present both this evaluation and a multikernel alternative for seL4, i.e., running an independent kernel on each core. The multikernel design avoids in-kernel locking, delivers better scalability than SMP, and retains low syscall overhead as unicore.

We also discuss the broader implications of this design shift, including what it means for thread migration, resource management, and the overall programming model of seL4 systems.

seL4’s functional correctness proofs certify that the kernel’s C implementation is a refinement of its abstract specification. Binary verification refers to the process of certifying that the compiled kernel binary is a refinement of its C implementation, completing the kernel’s end-to-end functional correctness argument and providing assurance that the kernel’s security properties are satisfied all the way down to the binary level. In particular, binary verification enables us to remove the compiler from our trusted computing base, eliminating concerns about bugs in sophisticated compiler optimization passes or differences between the compiler’s C semantics and those used by the functional correctness proofs.

Binary verification for seL4 was originally achieved by Thomas Sewell et al. with the construction of a novel automatic binary verification toolchain. With funding from the seL4 Foundation, we have picked up where they left off to strengthen, extend, and generalize this toolchain. This poster will lay out the toolchain’s design and report on our objectives and results.

Last year, we presented our vision of using seL4 as a guest OS for Confidential Virtual Machines (CVMs), arguing that its microkernel architecture, small code size, and formal verification make it a superior alternative to monolithic guest OSes like Linux, which present a large attack surface even within a hardware-protected CVM. This year, we report on concrete progress. We have further reduced the Trusted Computing Base (TCB) within the CVM by replacing the previous EDK II/OVMF and GRUB 2 stack with qboot, a minimal bootloader. Additionally, we are currently implementing initial remote attestation support, which is a critical building block for establishing trust in a CVM’s software stack. The talk will conclude with a live demo showing seL4 booting as a confidential VM on AMD SEV-SNP.

VM Composer is a GUI tool that makes it incredibly simple to design and build complex virtualized architectures on top of the seL4 Microkernel. The tool acts like a diagramming tool, but allows for granular configuration of virtual machines, device servers, and virtual connections. The tool supports x86 and ARM platforms. It is split into a front-end GUI and a back-end CLI tool which performs code/config generation and image building. This allows the back-end to be used in CI/CD pipelines.

The poster will introduce the tool to Summit attendees and will allow us to discuss use cases and our feature roadmap.

The TCCoE and the seL4 Foundation maintain liaison. This poster offers an overview and update on TCCoE planned activities, especially but not exclusively related to seL4™. TCCoE purposes are limited to research and knowledge sharing, including not only education and training but also promotion. Our community has passed an inflection point in the maturation of techniques and tools enhancing capabilities and reducing costs to perform trustworthy-by-design development and verification, but awareness of this is not widespread.

The mission of the Trusted Computing Center of Excellence™ (TCCoE™) is to lower barriers to adoption and facilitate the principled development and deployment of trustworthy software-based systems. Thus, risk will be reduced, especially in areas vital to U.S. and allied national defense, intelligence, security, and critical infrastructure. Rigorous mathematical proof offers strong evidence of trustworthiness, so the TCCoE fosters adoption of formal methods, as well as other advanced techniques, plus components and systems developed or verified with them. A leading example is the open source seL4 microkernel. TCCoE goals include maturation of such technologies, stabilization of their software distributions, and expanding/training the user/developer base to provide much needed capabilities for the Nation.

Our strategic plan identifies 3 essential pillars of TCCoE products and services and our tactical plan outlines how to market them. These mutually supporting pillars, based on the foundation of those plans, directly support the essential pediment of membership and workforce development, and ultimately support the capstone of mission accomplishment. Their primary visible face will be a virtual design center; a stretch goal is physical design centers (maker spaces), hosting resources and facilitating shirt-sleeve interactions. Each activity is intended both to advance the TCCoE mission and to yield profits to subsidize other activities, ideally enabling the organization to be self-sustaining until its mission is accomplished.

The central pillar is a curated repo of code with strong evidence of trustworthiness, formal methods tools, reference/starter platform components, and education/training materials. It is being enhanced with a metadata-markup taxonomy, search capabilities, licensing options (unlimited|controlled distribution, open|closed source, free|paid), policy based admission and capability based access controls using strong crypto to enforce the principle of least privilege, and resilient distributed storage (“eating our own dog food”).

Another essential pillar is ensuring the ready availability of suitable platforms, lowering one of the high barriers to adoption or even assessment of formal methods or their artifacts, including especially seL4. While total “plug-and-play” would be an unreasonable expectation, something closer to that ideal is badly needed to facilitate and encourage exploration by potential adopters. TCCoE will integrate existing subsystems (e.g. Genode, seL4, CHERI) for reference/starter platforms and provide precise up-to-date instructions on using/configuring them to yield at least one open platform on which developers can base production designs.

Our initial target area in which to support application development by others is uncrewed vehicle systems. Training and education is the pillar in the long term most essential to TCCoE mission accomplishment, in the medium term offers opportunities for revenue supporting the organization, and in the short term promotes awareness of the TCCoE itself. Although several universities conduct formal methods research and most colleges offer courses teaching the fundamentals on which such methods are based, there do not appear to be any curricula designed specifically to prepare students for working with them. TCCoE urgently solicits assistance in gathering/developing a collection of materials at all levels to develop all segments of the software workforce through sharing with educational institutions and offering on-line and on-site classes.