Conference Description
Key Takeaways
- Annual international summit dedicated to the seL4 microkernel and formally verified software
- Three-day programme covering real-world applications, technical development, and research
- Designed for software engineers, researchers, and organisations working on high-assurance and safety-critical systems
- Industries represented include aerospace, defence, automotive, and critical infrastructure
- Held in Vancouver, Canada, with keynotes, technical sessions, and networking opportunities
Introduction
The seL4 Summit is the principal annual gathering for the global community working with the seL4 microkernel, widely regarded as the most rigorously verified operating system kernel in existence. The 2026 edition brings together developers, researchers, technology providers, and end users in Vancouver, Canada, to examine the latest advances in formally verified software and its deployment in security-sensitive and safety-critical environments. At a time when software supply chain integrity and system-level security face increasing scrutiny, the summit offers a timely forum for practitioners seeking to understand how mathematical proof can underpin trustworthy computing infrastructure.
About the seL4 Summit
The seL4 Summit serves as the central meeting point for everyone involved in the seL4 ecosystem, from kernel contributors and toolchain developers to organisations deploying seL4-based products in the field. The programme balances accessibility for newcomers with depth for experienced practitioners, offering high-level overviews alongside detailed technical sessions. This structure enables attendees to build foundational knowledge while also engaging with cutting-edge research and implementation challenges.
The 2026 summit spans three days. The opening day focuses on applications and perspectives, showcasing how seL4-based systems operate in production environments. The subsequent two days shift toward technical development, ongoing research, and community discussions, providing opportunities for deeper engagement with the kernel’s internals and supporting infrastructure.
Formal Verification and the seL4 Microkernel
The seL4 microkernel distinguishes itself through formal verification, a process that uses mathematical proof to demonstrate that the kernel’s implementation correctly matches its specification. This approach eliminates entire categories of software defects that conventional testing cannot guarantee to catch, including buffer overflows and privilege escalation vulnerabilities that have historically compromised operating system security.
For industries where failure carries severe consequences—aerospace systems, defence platforms, autonomous vehicles, and critical infrastructure—formal verification offers a path toward demonstrably correct software foundations. The seL4 kernel’s verified properties include functional correctness, integrity enforcement, and confidentiality guarantees, making it suitable for systems that must meet stringent certification requirements or operate in adversarial environments.
Primary Discussion Topics
Sessions at the summit address the full breadth of the seL4 ecosystem. Technical content covers kernel development, verification methodologies, and the tools and frameworks that support seL4-based system construction. Practical sessions examine real-world deployments, exploring how organisations have integrated seL4 into products and the engineering challenges they encountered along the way.
The programme also addresses ecosystem infrastructure, including development environments, debugging tools, and the languages used to build verified components. Research presentations highlight ongoing work to extend seL4’s capabilities and apply formal methods to adjacent software layers, reflecting the broader ambition to expand the boundaries of provably correct computing.
Who Should Attend
The summit is designed for software engineers and system architects building high-assurance platforms, security professionals evaluating trustworthy computing foundations, and researchers advancing the state of formal verification. Academic faculty and students working in operating systems, security, or formal methods will find relevant content, as will technology providers developing products for regulated industries.
Decision-makers from organisations in aerospace, defence, automotive, and critical infrastructure sectors can gain insight into how formally verified kernels address compliance requirements and reduce systemic risk. The event’s mix of introductory and advanced material ensures value for both those new to seL4 and those with established expertise.
Sponsors
The 2026 seL4 Summit is supported by Apple as Gold sponsor, Proofcraft at the Silver level, and UNSW (University of New South Wales) as Bronze sponsor. Riverside Research sponsors the conference dinner, while DornerWorks supports the morning and afternoon breaks.
Conclusion
As demand grows for software systems that can withstand sophisticated attacks and meet rigorous safety standards, the seL4 Summit provides a valuable opportunity to learn from those at the forefront of formally verified computing. The Vancouver gathering offers both technical depth and community connection for anyone working to build more trustworthy software foundations.