seL4 Summit 2026

The emergence of formally verified building blocks across the stack, from memory-safe languages to verified 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.

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.

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.

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.