- Devel - lists.sel4.systems

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

16 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

1 0

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

seL4 developer hangout reminder
by Birgit Brecknell 13 Apr '26

13 Apr '26

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 14 Apr, 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

New release of seL4, Microkit, CAmkES, capDL and Rust support
by Gerwin Klein 31 Mar '26

31 Mar '26

We're pleased to announce the release of - seL4 15.0.0: The seL4 microkernel https://docs.sel4.systems/releases/sel4/15.0.0 - Microkit 2.2.0: The seL4 Microkit for building static-architecture systems https://docs.sel4.systems/releases/microkit/2.2.0 - CAmkES 3.12.0: Component Architecture for microkernel-based Embedded Systems https://docs.sel4.systems/releases/camkes/camkes-3.12.0 - capDL 0.5.0: Tools for generating, parsing and loading capability distribution specifications https://docs.sel4.systems/releases/capdl/0.5.0 - rust-sel4 4.0.0: Rust support for seL4 userspace https://github.com/seL4/rust-sel4/releases/tag/v4.0.0 seL4 15.0.0 and the corresponding Rust support come with new features and will require updates if you are using the seL4 API directly. CAmkES and the capDL tool add domain schedules as a new feature and applications will need updates if they use the seL4 domain scheduler. The Microkit release should not require any update of user code compared to Microkit 2.1.0. Enjoy! Gerwin

1 0

seL4 developer hangout reminder
by Birgit Brecknell 30 Mar '26

30 Mar '26

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 1 Apr, 7: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 16 Mar '26

16 Mar '26

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 17 Mar, 21: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 02 Mar '26

02 Mar '26

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 4 Mar, 7: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