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)