[y.....m]

Mikrokernel seL4 został zweryfikowany dla architektury RISC-V

seL4 to jest o tyle ciekawym mikrokernelem, że w sposób matematyczny dowiedziono, że jego kod(też po kompilacji) nie zawiera błędów:

What sets seL4 aside from all other OS kernels, including other microkernels, is its verification story. It was the world’s first OS kernel with a machine-checked, mathematical proof of the functional correctness of its C implementation (winning us a Hall of Fame Award as a result). This means that it is proved to be bug-free relative to a specification formulated in a mathematical logic.

RISC-V jest trzecią architekturą po ARM i x86-64 na którą w pełni przeportowano seL4.

seL4 is verified on RISC-V!
The seL4 Microkernel: An Introduction

#riscv i #linux (dla zasięgu)