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