Dear seL4 community,
I’m extremely pleased to announce that we have completed the functional correctness proof of seL4 on the RV64 ISA. Congratulations to our awesome Proof Engineering Team on achieving this major milestone for seL4! And many thanks to HENSOLDT Cyber for making it possible.
My blog discusses provides a bit more context for this announcement: https://microkerneldude.wordpress.com/2020/06/09/sel4-is-verified-on-risc-v/
What we have now is the refinement proof from the seL4 formal spec to the C implementation, putting RV64 on the same level as x64 in terms of seL4 verification. The binary verification, which extends this refinement to the binary code of the kernel is progressing, stay tuned for more news on that in the foreseeable future.
Gernot for the Trustworthy Systems team and the seL4 Foundation