El microkernel seL4 ha sido verificado matemáticamente para la arquitectura RISC-V
La organización RISC-V Foundation ha anunciado la verificación del microkernel seL4 en sistemas con arquitectura de conjunto de instrucciones RISC-V. La verificación se reduce a una prueba matemática que demuestra la fiabilidad de seL4, evidenciando su conformidad total con las especificaciones definidas en un lenguaje formal. Esta prueba de fiabilidad permite utilizar seL4 en sistemas críticos basados en procesadores RISC-V RV64, que requieren un alto nivel de fiabilidad y garantizan la ausencia de errores.
