Today, the seL4 Foundation and RISC-V International announced that the verified seL4 microkernel on the RV64 architecture has been proved down to the executable code by CSIRO’s Data61, thanks to funding provided by HENSOLDT Cyber GmbH. This guarantees that the seL4 microkernel on RV64 will operate to specification even when built with an untrusted C compiler, GCC.

For details please see:

seL4 news: https://sel4.systems/news.pml.html

RISC-V International announcement: https://riscv.org/announcements/2021/05/risc-v-international-and-sel4-founda...

My blog explaining what it means: https://microkerneldude.wordpress.com/2021/05/05/sel4-on-risc-v-verified-to-...

Gernot