The open-source seL4 microkernel, the first general-purpose kernel to have been proven to-spec using formal verification methods, has been ported to the open RISC-V instruction set architecture – though its creators warn it’s in a very early, limited form.

Originally developed by Australia’s National Information and Communications Technology (ICT) Research Centre of Excellence (NICTA) and now under the stewardship of Data61’s Trustworthy Systems Group, the seL4 microkernel is a security-focused offshoot of the high-performance L4 microkernel developed by Jochen Liedtke. Already available for Armv6, Armv7, and x86 instruction set architectures, the microkernal’s latest release – seL4 v9.0.1 – comes with initial RISC-V support, though in prototype form.

“RISC-V, through its openness and greenfield design, provides an opportunity for re-thinking the hardware-software stack. The open architecture, which is designed by leading architects and has strong industry support, is an ideal platform for our open-source seL4 system,” Data61’s Professor Gernot Heiser explains in a statement to Computerworld on the port. “We anticipate the combination of seL4 and RISC-V to provide a compelling security solution for the next-generation Internet of Things and cyber-physical systems.”

The prototype release currently supports only 64-bit RISC-V without floating-point unit (FPU) and multicore support on the Spike simulation platform, though extended support is expected to follow in future releases. Data61 has warned that the RISC-V port currently has no verification, unlike the microkernel’s other ports. More information is available on the release page.