El código binario del microkernel seL4 ha sido verificado formalmente para procesadores RISC-V [ENG]

En junio de 2020 anunciamos que el microkernel seL4 fue el primer kernel de sistema operativo del mundo con prueba de corrección de implementación verificada por máquina, también verificada para la arquitectura RV64, lo que lo convierte en el primer sistema operativo verificado formalmente para RISC-V. Ahora nos complace anunciar que esta verificación se ha extendido al código binario ejecutable, lo que significa que se ha demostrado que el código máquina que se ejecuta en el procesador es correcto. // Relacionada: El microkernel seL4 ha sido verificado formalmente para procesadores RISC-V.