Call for Presentations

The seL4 Summit aims at gathering the seL4 community to learn, share, and connect:

• learn about the seL4 technology, its latest progress, use, successes, challenges, plans;
• share exciting seL4 development, research, experience, applications in the real world;
• connect with other seL4 developers, users, providers, supporters, potential partners, and enthusiasts.

The seL4 Summit covers the complete seL4 ecosystem, consisting of the verified microkernel, as well as all seL4-related technology, tools, infrastructure, products, projects, and people.

The seL4 Summit 2026 will be in Vancouver, Canada.

The Program Committee solicits proposals on any seL4-related topic, or any topic related to verified software that would be relevant to the seL4 community, in particular on the following themes:

• visions, lessons-learned, roadmaps for verified software deployments
• use-cases, deployments, experiences
• walk-throughs and demos of tools, frameworks, systems
• early work, crazy ideas, out-of-the-box thinking
• technical progress, updates, breakthroughs

The format can be a regular talk, short talk, poster, or a walk-through/demo.

The topics of interest include any of the below, where “seL4” relates to the kernel itself or any tool, framework, language, components, or system related to seL4 or verified software:

• seL4 experience reports
  • experience with deploying seL4 in the field, in commercial/deployed products
  • experience with teaching seL4
  • experience with seL4 in certification schemes and application of industry standards
  • experience with “building a business case for using a verified kernel”
  • experience with porting software from other OSes
• seL4 and assurance
  • application-level verification leveraging seL4 proofs
  • correctness, spatial separation, temporal separation, and real-time proofs
  • formalised interface between or composition of kernel-level proofs and user-level proofs
  • verification engineering at scale, scaling verification productivity
  • security/safety impact/assurance/certification for an seL4-based system
• seL4 on-going and planned R&D, mature or early stage
  • seL4 research efforts
  • seL4 development efforts
  • work-in-progress seL4 development
  • student work on seL4
  • new/missing/next-gen kernel mechanisms
  • seL4-related roadmaps: what you plan to work on and when
  • seL4 grand challenges
  • OS frameworks and services
  • seL4 userland with programming language support beyond C
  • high performance systems based on seL4: pushing the boundaries
  • early work/new ideas/initial experiments with seL4
• seL4 and hardware
  • ports to new hardware platforms or architectures
  • multicore systems
  • virtualisation
  • new/proposed hardware features or architectures, which could also enable or broaden the scope of formal reasoning (e.g. about time protection)
  • seL4 in embedded processors on FPGAs, and impact of assured separation
  • IOMMU solutions for various hardware architectures and impact for seL4
  • device driver development, porting, reuse, frameworks, verification