Have you heard that CSIRO has announced the completion of the proof of implementation correctness of the open-source seL4 microkernel for the RISC-V ISA?
The Commonwealth Scientific and Industrial Research Organisation's (CSIRO) Data61 has completed the proof of implementation correctness of the open-source seL4 microkernel for the RISC-V instruction-set architecture (ISA).
Unlike most other ISA designs, the RISC-V ISA is provided under open source licences that do not require fees. According to Data61, many organisations are developing processors based on the open RISC-V ISA, targeting platforms ranging from embedded and cyberphysical systems to high-end servers.
Data61's development means that seL4's security enforcement is now available to the RISC-V ecosystem.