- Devel - lists.sel4.systems

QSOE: QNX-inspired OS with dual-kernel architecture (custom kernel & seL4)
by Yuri Zaporozhets 23 Jun '26

23 Jun '26

Hi! This is my project which I recently announced: https://qsoe.net Interestingly, when working in the shell (mksh-derived), the subjective "feeling" is that QSOE/N (with Skimmer) is ~10 times faster than /L :) . Launching e.g. "time ls" command confirms this: 0.1s for QSOE/L (with seL4) vs. 0.01s for QSOE/N. The work continues. Now I'm working on a video controller support for my SiFive Unmatched; then, when the _real_ text-mode console is there, I'll return to active QSOE developments. -- Regards, Yuri

1 0

RFC: Enabling uROS on seL4
by HHN 22 Jun '26

22 Jun '26

Hi Everyone, I have recently been experimenting with porting uROS to seL4. uROS (micro-ROS) is a very minimal version of ROS (Robot Operating System) - a well known robotics middleware suite. I have implemented the micro-ROS examples <https://github.com/micro-ROS/micro-ROS-demos/tree/kilted/rclc> and the necessary system to run them on seL4 over here <https://github.com/Johan511/sel4_uros>. A high level explanation of the work can be found here <https://johan511.github.io/posts/2025-01-19-uros-on-sel4/>. I do not have any prior experience with Operating system development or with ROS, so any critiques are much appreciated. Thank you -- Hari Hara Naveen

2 2

seL4 developer hangout reminder
by Birgit Brecknell 22 Jun '26

22 Jun '26

Hi all A friendly reminder that the seL4 developer hangout is on again next week. Wed 24 Jun, 8:00 UTC For your local date and time please see https://sel4.systems/stay-informed.html#calendar Zoom link: https://unsw.zoom.us/j/82640784431 Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

libsel4 status
by Yanfeng Liu 02 Jun '26

02 Jun '26

Dear experts, It seems that currently libsel4 has many inlined functions thus user space code size is large. I am wondering if this is really necessary? If current libsel4 is not for production use, then it doesnt matter. Otherwise I am wondering if we need support size optimized config as well? I am hoping that libsel4 changes wont affect kernel verification? Regards, yf

3 4

seL4 developer hangout reminder
by Birgit Brecknell 25 May '26

25 May '26

Hi all A friendly reminder that the seL4 developer hangout is on again next week. Wed 27 May, 8:00 UTC For your local date and time please see https://sel4.systems/stay-informed.html#calendar Zoom link: https://unsw.zoom.us/j/82640784431 Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Question about ASpec → ExecSpec session dependency and shared-types design choice
by li-jun zhang 20 May '26

20 May '26

shared-types design choice Hi seL4 verification team, my name is Li-Jun Zhang, a PDH student form Nanjing University. I'm studying the structure of spec/ROOT and have a question about a design choice I'd like to understand before considering whether it's worth trying to change. The observation ASpec is declared in spec/ROOT as session ASpec in "abstract" = Word_Lib + sessions "HOL-Library" Lib ExecSpec ... Across the codebase there are nine direct imports "ExecSpec.X" from spec-side files, through five targets: | Imported ExecSpec theory | Importing spec-side theory | | --- | --- | | ExecSpec.MachineTypes | CKernel.Kernel_C, CSpec.Kernel_C, ExecSpec.MachineMonad | | ExecSpec.InvocationLabels_H | ASpec.ArchDecode_A, ASpec.Decode_A | | ExecSpec.Event_H | ASpec.Syscall_A, DSpec.Syscall_D | | ExecSpec.Arch_Structs_B | ASpec.Arch_Structs_A | | ExecSpec.ArchLabelFuns_H | ASpec.InvocationLabels_A | Combined with the sessions ExecSpec declaration, this means any Haskell prototype edit transitively invalidates ASpec and AInvs builds — even when the edit doesn't touch any of the five shared targets, because sessions ExecSpec causes ExecSpec's whole content to be source-re-executed inside ASpec's ML state. The skeleton file spec/design/skel/ARM/Arch_Structs_B.thy carries the comment (* Architecture-specific data types shared by spec and abstract. *) which suggests these targets are understood as cross-pillar shared, yet they physically live inside the Haskell-derived ExecSpec session. The comment dates back to commit 2a03e81 (the initial open-source release in 2014), and the sessions ExecSpec line has survived multiple subsequent ROOT reorganizations (e.g. the 2018 session-qualified-imports work and the 2020-10 new ROOT requirements reorg), so I assume the structure is intentional rather than incidental. The hypothetical change Suppose the closure of the five shared targets within ExecSpec (12 theories total: MachineTypes, MachineMonad, MachineOps, MachineExports, Platform, Kernel_Config, Setup_Locale, Event_H, ArchInvocationLabels_H, InvocationLabels_H, ArchLabelFuns_H, Arch_Structs_B) were moved into a base KernelTypes session, with ASpec and ExecSpec both reparented to + KernelTypes. Then: sessions ExecSpec could be removed from ASpec's ROOT entry. A Haskell-side edit that doesn't touch the 12 shared theories would no longer invalidate ASpec / AInvs. Type identity is preserved as long as the moved files keep global_naming ARM_H — the fully qualified names (ARM_H.arm_vspace_region_use, etc.) referenced by downstream are unchanged. My question Was an extraction of this kind considered when the current structure was designed (presumably pre-2014, given the comment dates from the initial release)? Are there constraints — generation-pipeline output paths, type-equality concerns beyond the global_naming trick, methodological coupling between Haskell-as-canonical-source and the abstract spec, downstream tooling that references the ExecSpec.X FQNs, or anything else — that make the current sessions ExecSpec structure the deliberate choice? I'd rather not pursue a refactor that's already been considered and rejected for a reason I'm not seeing. Pointers to prior discussion (mailing-list threads, design notes, PRs) would be very helpful. Thanks Li-Jun Zhang

2 2

seL4 developer hangout reminder
by Birgit Brecknell 11 May '26

11 May '26

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 12 May, 22:00 UTC For your local date and time please see https://sel4.systems/stay-informed.html#calendar Zoom link: https://unsw.zoom.us/j/82640784431 Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

seL4 developer hangout reminder
by Birgit Brecknell 24 Apr '26

24 Apr '26

Hi all A friendly reminder that the seL4 developer hangout is on again next week. Wed 29 Apr, 8:00 UTC For your local date and time please see https://sel4.systems/stay-informed.html#calendar Zoom link: https://unsw.zoom.us/j/82640784431 Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Last day to submit a talk proposal to the sel4 summit!
by June Andronick 21 Apr '26

21 Apr '26

It only requires an abstract describing your talk proposal. https://form.jotform.com/260147181364858 Looking forward to your submissions. Cheers, June

1 1

seL4 summit 2026: one week to go to submit a talk
by Birgit Brecknell 13 Apr '26

13 Apr '26

One week to go to submit a talk [0] for the seL4 Summit 2026 [1]! If you’d like to submit a talk, please upload an abstract of one page or less to the submission portal [2]. **Abstracts are due on 20 April 2026.** **NEW!** The 2026 edition of the seL4 summit will feature a **full first day** dedicated to **applications, overviews, and perspectives** on seL4-based systems and formally verified software in the real world. This will be followed by Days 2 and 3 focusing on more technical development, research, reports, and discussions. We are particularly keen to **welcome people who are new to seL4** or still developing their familiarity with the technology. The event will offer an **ideal opportunity to gain a high-level view of the landscape and ecosystem** of seL4 and its associated tools, frameworks and languages, as well as formally verified software in general, and to take stock of the latest updates. The seL4 Summit 2026 will be held 1 - 3 September 2026 at the Hyatt Regency Vancouver, Vancouver, Canada. The summit will be an in-person event. We’re looking forward to many exciting proposals! [0] https://sel4.systems/Summit/2026/cfp [1] https://sel4.systems/Summit/2026/ [2] https://form.jotform.com/260147181364858 Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0