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).
Article: https://www.zdnet.com/article/data61s-sel4-security-enforcement-now-available-to-the-risc-v-ecosystem/