# Latest **URL:** https://sel4.discourse.group/latest.md [Latest](https://sel4.discourse.group/latest.md) · [Categories](https://sel4.discourse.group/categories.md) · [Tags](https://sel4.discourse.group/tags.md) --- ## [Welcome to Discourse](https://sel4.discourse.group/t/welcome-to-discourse/7)
**Author:** [@system](https://sel4.discourse.group/u/system)\ **Replies:** 0\ **Last updated:** [January 2, 2019, 6:04pm UTC](https://sel4.discourse.group/t/welcome-to-discourse/7 "2019-01-02T18:04:10Z")
seL4 is the world’s first operating-system kernel with an end-to-end proof of implementation correctness and is an excellent base to build high-assurance systems. This site is for members of the seL4 community, including… --- ## [Vm\_minimal example on ZCU-102 board](https://sel4.discourse.group/t/vm-minimal-example-on-zcu-102-board/1081)
**Author:** [@matteoz](https://sel4.discourse.group/u/matteoz)\ **Replies:** 0\ **Last updated:** [September 22, 2026, 4:19pm UTC](https://sel4.discourse.group/t/vm-minimal-example-on-zcu-102-board/1081 "2026-09-22T16:19:16Z")
Hi everyone, I’m trying to test seL4 with CAmkES on a ZCU-102 board by Xilinx and I’m stuck trying to boot the vm\_minimal example. I followed the steps provided here, but when I try to boot it on the hardware, the load… --- ## [The Australian National University joins seL4 Foundation](https://sel4.discourse.group/t/the-australian-national-university-joins-sel4-foundation/1080)
**Author:** [@bbrcknl](https://sel4.discourse.group/u/bbrcknl)\ **Replies:** 0\ **Last updated:** [September 17, 2026, 10:03pm UTC](https://sel4.discourse.group/t/the-australian-national-university-joins-sel4-foundation/1080 "2026-09-17T22:03:23Z")
The seL4 Foundation is pleased to welcome the Australian National University (ANU) as an Associate Member. ANU’s School of Computing has a longstanding connection to seL4, and ANU researchers have contributed to seL4’s o… --- ## [The videos and slides of the seL4 Summit 2026 are available online](https://sel4.discourse.group/t/the-videos-and-slides-of-the-sel4-summit-2026-are-available-online/1078)
**Author:** [@bbrcknl](https://sel4.discourse.group/u/bbrcknl)\ **Replies:** 0\ **Last updated:** [September 16, 2026, 7:24am UTC](https://sel4.discourse.group/t/the-videos-and-slides-of-the-sel4-summit-2026-are-available-online/1078 "2026-09-16T07:24:57Z")
Videos of the seL4 Summit 2026 are now available on the seL4 YouTube channel! Links, slides, and posters can be found on the summit Program and Abstracts pages. Thanks to all the speakers for making the seL4 Summit 2026 … --- ## [seL4 security proofs now complete on AArch64](https://sel4.discourse.group/t/sel4-security-proofs-now-complete-on-aarch64/1074)
**Author:** [@june.andronick](https://sel4.discourse.group/u/june.andronick)\ **Replies:** 0\ **Last updated:** [August 24, 2026, 10:55am UTC](https://sel4.discourse.group/t/sel4-security-proofs-now-complete-on-aarch64/1074 "2026-08-24T10:55:25Z")
The verification of seL4 on the 64-bit Arm architecture has reached another milestone. After completing the proofs of functional correctness and integrity, Proofcraft has now established the proof that seL4 enforces conf… --- ## [Thank you UNSW Sydney, bronze sponsor of the seL4 Summit 2026](https://sel4.discourse.group/t/thank-you-unsw-sydney-bronze-sponsor-of-the-sel4-summit-2026/1073)
**Author:** [@bbrcknl](https://sel4.discourse.group/u/bbrcknl)\ **Replies:** 0\ **Last updated:** [August 16, 2026, 11:50pm UTC](https://sel4.discourse.group/t/thank-you-unsw-sydney-bronze-sponsor-of-the-sel4-summit-2026/1073 "2026-08-16T23:50:28Z")
The seL4 Foundation thanks UNSW Sydney for becoming a Bronze sponsor of the seL4 Summit 2026. seL4 was created by the Trustworthy Systems (TS) team, which is now part of the UNSW, a founding member of the seL4 Foundatio… --- ## [Thank you DornerWorks, sponsor of the seL4 Summit 2026 AM & PM Break](https://sel4.discourse.group/t/thank-you-dornerworks-sponsor-of-the-sel4-summit-2026-am-pm-break/1072)
**Author:** [@bbrcknl](https://sel4.discourse.group/u/bbrcknl)\ **Replies:** 0\ **Last updated:** [August 13, 2026, 11:08pm UTC](https://sel4.discourse.group/t/thank-you-dornerworks-sponsor-of-the-sel4-summit-2026-am-pm-break/1072 "2026-08-13T23:08:09Z")
The seL4 Foundation thanks DornerWorks, sponsor of the seL4 Summit 2026 AM & PM Break. DornerWorks is an embedded technology partner, a founding member of the seL4 Foundation, and one of its endorsed service providers. … --- ## [Happy seL4 day 2026!](https://sel4.discourse.group/t/happy-sel4-day-2026/1071)
**Author:** [@bbrcknl](https://sel4.discourse.group/u/bbrcknl)\ **Replies:** 0\ **Last updated:** [July 29, 2026, 4:47am UTC](https://sel4.discourse.group/t/happy-sel4-day-2026/1071 "2026-07-29T04:47:44Z")
On July 29, 2009, the last “sorry” of the seL4 functional correctness proof was eliminated. A “sorry” is an assumed theorem lacking a complete proof. “0 sorries” meant there was nothing left to prove: the project was fin… --- ## [One week left to get the early-bird registration at the seL4 summit!](https://sel4.discourse.group/t/one-week-left-to-get-the-early-bird-registration-at-the-sel4-summit/1070)
**Author:** [@bbrcknl](https://sel4.discourse.group/u/bbrcknl)\ **Replies:** 0\ **Last updated:** [July 23, 2026, 9:30pm UTC](https://sel4.discourse.group/t/one-week-left-to-get-the-early-bird-registration-at-the-sel4-summit/1070 "2026-07-23T21:30:36Z")
1 week left to get the early-bird registration at the seL4 summit! A friendly reminder that the early bird cut-off date is 31 July 2026. Tickets include: Participation in the 3-day conference, including talks, keyno… --- ## [July 2026 Releases of seL4, Microkit, CAmkES, capDL, and Rust support](https://sel4.discourse.group/t/july-2026-releases-of-sel4-microkit-camkes-capdl-and-rust-support/1069)
**Author:** [@gerwin.klein](https://sel4.discourse.group/u/gerwin.klein)\ **Replies:** 0\ **Last updated:** [July 23, 2026, 2:04am UTC](https://sel4.discourse.group/t/july-2026-releases-of-sel4-microkit-camkes-capdl-and-rust-support/1069 "2026-07-23T02:04:32Z")
We’re pleased to announce the release of seL4 16.0.0: The seL4 microkernel Microkit 2.3.0: The seL4 Microkit for building static-architecture systems CAmkES 3.13.0: Component Architecture for microkernel-based Embedded… --- ## [Panellists for seL4 Summit 2026 announced](https://sel4.discourse.group/t/panellists-for-sel4-summit-2026-announced/1068)
**Author:** [@bbrcknl](https://sel4.discourse.group/u/bbrcknl)\ **Replies:** 0\ **Last updated:** [July 22, 2026, 5:06am UTC](https://sel4.discourse.group/t/panellists-for-sel4-summit-2026-announced/1068 "2026-07-22T05:06:12Z")
We are very fortunate to welcome five industry leaders to participate at the seL4 Summit 2026, in a session on Certification, Compliance and Policies: enabler or barrier to innovation?: Darren Cofer, Peter Davies, Jonath… --- ## [Two weeks left to get the early-bird registration at the seL4 summit!](https://sel4.discourse.group/t/two-weeks-left-to-get-the-early-bird-registration-at-the-sel4-summit/1067)
**Author:** [@bbrcknl](https://sel4.discourse.group/u/bbrcknl)\ **Replies:** 0\ **Last updated:** [July 17, 2026, 12:25am UTC](https://sel4.discourse.group/t/two-weeks-left-to-get-the-early-bird-registration-at-the-sel4-summit/1067 "2026-07-17T00:25:30Z")
2 weeks left to get the early-bird registration at the seL4 summit! A friendly reminder that the early bird cut-off date is 31 July 2026. Tickets include: Participation in the 3-day conference, including talks, keyn… --- ## [seL4 summit 2026 sponsorship opportunities closing soon](https://sel4.discourse.group/t/sel4-summit-2026-sponsorship-opportunities-closing-soon/1066)
**Author:** [@bbrcknl](https://sel4.discourse.group/u/bbrcknl)\ **Replies:** 0\ **Last updated:** [July 15, 2026, 6:37am UTC](https://sel4.discourse.group/t/sel4-summit-2026-sponsorship-opportunities-closing-soon/1066 "2026-07-15T06:37:22Z")
The seL4 Summit is the annual international summit on the seL4 microkernel, the world’s most highly assured OS kernel, as well as on all seL4-related technology, tools, infrastructure, products, projects, and people. T… --- ## [Refinement proof of the CapDL initialiser?](https://sel4.discourse.group/t/refinement-proof-of-the-capdl-initialiser/1065)
**Author:** [@Whatever314](https://sel4.discourse.group/u/Whatever314)\ **Replies:** 0\ **Last updated:** [July 15, 2026, 2:32am UTC](https://sel4.discourse.group/t/refinement-proof-of-the-capdl-initialiser/1065 "2026-07-15T02:32:59Z")
Hello everyone: I noticed an abstract specification of the CapDL initialiser in the SysInit proofs, however i could not find a refinement proof between the abstract specification and the provided c implementation in seL… --- ## [Reasoning about a sequentially-verified C component inside an seL4 partition — confinement vs. a more structured model?](https://sel4.discourse.group/t/reasoning-about-a-sequentially-verified-c-component-inside-an-sel4-partition-confinement-vs-a-more-structured-model/1060)
**Author:** [@Fikoko](https://sel4.discourse.group/u/Fikoko)\ **Replies:** 7\ **Last updated:** [July 13, 2026, 11:55am UTC](https://sel4.discourse.group/t/reasoning-about-a-sequentially-verified-c-component-inside-an-sel4-partition-confinement-vs-a-more-structured-model/1060 "2026-07-13T11:55:34Z")
Hello — I come at this from the formal-verification-of-C side and I’m still finding my feet with seL4, so a pointer from people who reason about the proof guarantees properly would be very welcome. I maintain a formally… --- ## [3 weeks before the early-bird deadline for the seL4 summit](https://sel4.discourse.group/t/3-weeks-before-the-early-bird-deadline-for-the-sel4-summit/1063)
**Author:** [@june.andronick](https://sel4.discourse.group/u/june.andronick)\ **Replies:** 0\ **Last updated:** [July 10, 2026, 9:43am UTC](https://sel4.discourse.group/t/3-weeks-before-the-early-bird-deadline-for-the-sel4-summit/1063 "2026-07-10T09:43:48Z")
Don’t forget to register to the seL4 summit! Only 3 weeks left to benefit from the early-bird fee: See you in Vancouver :slight\_smile: --- ## [The seL4 Summit 2026 Program and Abstracts](https://sel4.discourse.group/t/the-sel4-summit-2026-program-and-abstracts/1062)
**Author:** [@bbrcknl](https://sel4.discourse.group/u/bbrcknl)\ **Replies:** 0\ **Last updated:** [July 1, 2026, 6:20am UTC](https://sel4.discourse.group/t/the-sel4-summit-2026-program-and-abstracts/1062 "2026-07-01T06:20:25Z")
The program of the seL4 Summit 2026 is now available! The 2026 edition of the seL4 summit features a full first day dedicated to high-level overviews and perspectives, followed by Days 2 and 3 focusing on more technical… --- ## [Gapfruit joins the seL4 Foundation](https://sel4.discourse.group/t/gapfruit-joins-the-sel4-foundation/1056)
**Author:** [@bbrcknl](https://sel4.discourse.group/u/bbrcknl)\ **Replies:** 0\ **Last updated:** [June 1, 2026, 7:27am UTC](https://sel4.discourse.group/t/gapfruit-joins-the-sel4-foundation/1056 "2026-06-01T07:27:08Z")
We are pleased to welcome a new member - Gapfruit - to the seL4 Foundation. Gapfruit is a Swiss technology company building trustworthy foundations for the systems society depends on - from industrial controls to energy… --- ## [Unikernel vs SMP vs Multi-Kernel docs?](https://sel4.discourse.group/t/unikernel-vs-smp-vs-multi-kernel-docs/1055)
**Author:** [@fdelizy](https://sel4.discourse.group/u/fdelizy)\ **Replies:** 3\ **Last updated:** [May 22, 2026, 3:26pm UTC](https://sel4.discourse.group/t/unikernel-vs-smp-vs-multi-kernel-docs/1055 "2026-05-22T15:26:55Z")
I read through this very interesting thread: “Performance comparison with non-L4 kernels” which digressed into SMP vs Multi-kernel verification. I am working on a Genode based project, at the moment genode supports seL… --- ## [seL4 iMX95 support](https://sel4.discourse.group/t/sel4-imx95-support/1054)
**Author:** [@fdelizy](https://sel4.discourse.group/u/fdelizy)\ **Replies:** 1\ **Last updated:** [May 21, 2026, 8:38pm UTC](https://sel4.discourse.group/t/sel4-imx95-support/1054 "2026-05-21T20:38:46Z")
Hi, as part of a few projects I am working on a combination genode + sel4 on various ARM processors. So far, I got iMX8Mp boards running armstone i.MX8MP (FS-net) Verdin i.MX8MP SOM + Dahlia carreer board (Toradex) M… --- ## [Changing rust-root-task-demo from targeting aarch64 to x86\_64](https://sel4.discourse.group/t/changing-rust-root-task-demo-from-targeting-aarch64-to-x86-64/1049)
**Author:** [@bpisch](https://sel4.discourse.group/u/bpisch)\ **Replies:** 1\ **Last updated:** [May 12, 2026, 8:46am UTC](https://sel4.discourse.group/t/changing-rust-root-task-demo-from-targeting-aarch64-to-x86-64/1049 "2026-05-12T08:46:04Z")
Dear Community, I am a completely new seL4 developer wanting to explore possibilities with Rust on seL4. I have successfully booted the sel4/rust-root-task-demo repository’s system with the default configuration. Howeve… --- ## [Does seL4's verification story guarantee the integrity of the kernel itself at runtime?](https://sel4.discourse.group/t/does-sel4s-verification-story-guarantee-the-integrity-of-the-kernel-itself-at-runtime/1047)
**Author:** [@Whatever314](https://sel4.discourse.group/u/Whatever314)\ **Replies:** 4\ **Last updated:** [April 29, 2026, 9:04am UTC](https://sel4.discourse.group/t/does-sel4s-verification-story-guarantee-the-integrity-of-the-kernel-itself-at-runtime/1047 "2026-04-29T09:04:29Z")
I know that the integrity proof guarantees a policy of integrity. But I wonder whether malicious calls of the kernel’s interfaces (i.e. vspace) that could interpolate the kernel’s code is allowed, though those callsalso … --- ## [Improve Documentation](https://sel4.discourse.group/t/improve-documentation/1046)
**Author:** [@indolering](https://sel4.discourse.group/u/indolering)\ **Replies:** 0\ **Last updated:** [April 19, 2026, 12:24am UTC](https://sel4.discourse.group/t/improve-documentation/1046 "2026-04-19T00:24:05Z")
As a UX engineer and not an OS dev, I find the on-boarding process to be full of unnecessary challenges. Just figuring out where to start is difficult because the documentation for seL4, LionsOS, and microkit is spread … --- ## [Thank you Proofcraft, silver sponsor of the seL4 Summit 2026](https://sel4.discourse.group/t/thank-you-proofcraft-silver-sponsor-of-the-sel4-summit-2026/1045)
**Author:** [@bbrcknl](https://sel4.discourse.group/u/bbrcknl)\ **Replies:** 0\ **Last updated:** [April 16, 2026, 9:53pm UTC](https://sel4.discourse.group/t/thank-you-proofcraft-silver-sponsor-of-the-sel4-summit-2026/1045 "2026-04-16T21:53:46Z")
The seL4 Foundation thanks Proofcraft, silver sponsor of the seL4 Summit 2026. Founded by the seL4 verification leaders, Proofcraft offers commercial support and projects in formal verification in general, and involving… --- ## [Thank you Riverside Research, sponsor of the seL4 Summit 2026 reception](https://sel4.discourse.group/t/thank-you-riverside-research-sponsor-of-the-sel4-summit-2026-reception/1044)
**Author:** [@bbrcknl](https://sel4.discourse.group/u/bbrcknl)\ **Replies:** 0\ **Last updated:** [April 15, 2026, 4:05am UTC](https://sel4.discourse.group/t/thank-you-riverside-research-sponsor-of-the-sel4-summit-2026-reception/1044 "2026-04-15T04:05:44Z")
The seL4 Foundation thanks Riverside Research for sponsoring the seL4 Summit 2026 reception. Riverside Research is a national security nonprofit serving the DOD and Intelligence Community. Through the company’s Open Inn… --- ## [seL4 summit 2026: one week to go to submit a talk](https://sel4.discourse.group/t/sel4-summit-2026-one-week-to-go-to-submit-a-talk/1043)
**Author:** [@bbrcknl](https://sel4.discourse.group/u/bbrcknl)\ **Replies:** 0\ **Last updated:** [April 13, 2026, 12:58am UTC](https://sel4.discourse.group/t/sel4-summit-2026-one-week-to-go-to-submit-a-talk/1043 "2026-04-13T00:58:49Z")
One week to go to submit a talk for the seL4 Summit 2026! If you’d like to submit a talk, please upload an abstract of one page or less to the submission portal. Abstracts are due on 20 April 2026. NEW! The 2026 edit… --- ## [Tutorial problem on macOS](https://sel4.discourse.group/t/tutorial-problem-on-macos/1042)
**Author:** [@daveyost](https://sel4.discourse.group/u/daveyost)\ **Replies:** 1\ **Last updated:** [April 5, 2026, 8:35pm UTC](https://sel4.discourse.group/t/tutorial-problem-on-macos/1042 "2026-04-05T20:35:12Z")
On macOS 26.4, following the instructions for the microkit tutorial, I did all the brew-ha-ha, then I get stuck: Z% ll -tr total 160656 drwxr----- 9 yost staff 288 2026-03-30.22:37:34 microkit-sdk-2.2.0 -rw-rw-… --- ## [March 2026 Releases](https://sel4.discourse.group/t/march-2026-releases/1041)
**Author:** [@gerwin.klein](https://sel4.discourse.group/u/gerwin.klein)\ **Replies:** 0\ **Last updated:** [March 31, 2026, 9:35am UTC](https://sel4.discourse.group/t/march-2026-releases/1041 "2026-03-31T09:35:50Z")
We’re pleased to announce the release of seL4 15.0.0: The seL4 microkernel Microkit 2.2.0: The seL4 Microkit for building static-architecture systems CAmkES 3.12.0: Component Architecture for microkernel-based Embedded… --- ## [Planned any SpacemiT K3 SBC (e.g. K3 Pico-ITX) kernel support?](https://sel4.discourse.group/t/planned-any-spacemit-k3-sbc-e-g-k3-pico-itx-kernel-support/1040)
**Author:** [@onlineinternaut](https://sel4.discourse.group/u/onlineinternaut)\ **Replies:** 3\ **Last updated:** [March 23, 2026, 5:30pm UTC](https://sel4.discourse.group/t/planned-any-spacemit-k3-sbc-e-g-k3-pico-itx-kernel-support/1040 "2026-03-23T17:30:22Z")
Hi! Hope I am asking on the proper forum. It is announced that SBCs with SpacemiT K3 RISC-V CPU boards will be available on market soon. I’m just wondering whether any SBC with this CPU will be supported by the SeL4 kern… --- ## [Reframing IPC as XDC](https://sel4.discourse.group/t/reframing-ipc-as-xdc/1038)
**Author:** [@indolering](https://sel4.discourse.group/u/indolering)\ **Replies:** 1\ **Last updated:** [March 19, 2026, 12:41am UTC](https://sel4.discourse.group/t/reframing-ipc-as-xdc/1038 "2026-03-19T00:41:02Z")
The pop-culture opinion of microkernels is that IPC is their achilles heel, even though the style of IPC seL4 uses is much faster than Unix or Mach. I would like to suggest reframing all seL4/LionsOs IPC to Cross Domain … [Next page](https://sel4.discourse.group/latest.md?page=1)