The world’s first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement is available as open source.
- seL4 is a high-assurance, high-performance microkernel developed, maintained and formally verified by NICTA (now the Trustworthy Systems Group at Data61) and owned by General Dynamics C4 Systems. It is a member of the L4 family of microkernels, and is the world’s most advanced, highest-assured operating-system microkernel.
- seL4’s implementation is formally (mathematically) proved correct (bug-free) against its specification, is proved to enforce strong security properties, and its operations have proved save upper bounds on their worst-case execution times.
Sample projects and resources
- RISC-V-Guide. RISC-V Guide. Learn all about the RISC-V computer architecture along with the Development Tools and Operating Systems to develop on RISC-V hardware..
- NeptuneOS. Neptune OS: A Windows NT personality for the seL4 microkernel.
- awesome-provable. A curated set of links to formal methods involving provable code..
- veracruz. Main repository for the Veracruz privacy-preserving compute project, an adopted project of the Confidential Compute Consortium (CCC)..
- ferros. A Rust-based userland which also adds compile-time assurances to seL4 development..
- seL4_tools. Basic tools for building seL4 projects.
- docs. This is the source of the seL4 docs..
- seL4-CAmkES-L4v-dockerfiles. Dockerfiles defining the dependencies required to build seL4, CAmkES, and L4v..
- selfe-sys. A generated thin wrapper around libsel4.a, with supporting subcrates..
- sel4-armv8-vmm-manifest. A manifest that allows one to build virtualized seL4 for zcu102 and i.MX8.
- rpi3-rust-fel4-workspace. Rust embedded things running on the seL4 microkernel for the Raspberry Pi 3.
- ICSVerifiedSoftwareProject. A formally verified implementation of a bolt-on security device for ICS networks. Designed with TLA+ and written/proved in F*.
- solox-amp-rust. AMP experiments in feL4 (seL4/Rust) on SoloX ARM SoC (A9 + M4).
- ci-actions. CI GitHub actions for the seL4 repositories.
- website. The seL4.systems website.
- SeL4_101. How to create a Hello World seL4 project from scratch .
- Sofa. Operating System built on top of the seL4 microkernel..
- ferros-sabrelite-toy-system. Rust seL4 toy system built on ferros for the imx6 sabrelite platform.
- Advanced_Operating_System_2017. Basic operating system features implementation. File system/Process management/Memory management.
- veracruz-examples. A repository of larger example Veracruz computations .
- seL4_hydra. Attestation and software update in seL4.
- sel4-hobd-prototype. Prototype HOBD system running on seL4.
- seL4cp-workshop. My solutions to the draft-version of the seL4 Core Platform (seL4cp) Workshop held during the 2022 seL4 Summit (11 - 13 Oct)..
- whitepaper. Source for the seL4 white paper.
- fel4-test-project. A feL4 test project (Rust on seL4) - armv7 imx6 sabre lite.
- ferros-fancy-test. Test-runner support libraries for ferros..
- SeL4_CPIO. Create a simple SeL4 Project with a CPIO archive.
- SeL4_UserLandLib. How to Create a library and link an application against it .
- Sel4_EGA. how to use EGA display with Sel4.
- sel4twinkle-alloc-rs. An experimental Rust port of libsel4twinkle allocator.