The microkernel seL4 is mathematically verified for the RISC-V architecture.
The RISC-V Foundation has reported the verification of the seL4 microkernel on RISC-V instruction set architecture systems. The verification consists of a mathematical proof of the reliability of seL4, which indicates full compliance with specifications defined in formal language. The proof of reliability allows using seL4 in mission-critical systems based on RISC-V RV64 processors, which require a higher level of reliability and guarantee the absence of […]
