El microkernel seL4 ha sido verificado formalmente para procesadores RISC-V [ENG]

El kernel de un sistema operativo es el software que funciona a más bajo nivel en un ordenador. Es el código que funciona en modo privilegiado (S-Mode en RISC-V), por lo que es el responsable principal y único de la seguridad del sistema. Que un kernel, en este caso seL4, esté formalmente verificado significa que su implementación en C es funcionalmente correcta, ya que ha sido matemáticamente verificada mediante software probando que está libre de errores.