Dear seL4 community,
it’s my pleasure to announce that even more proofs have become available for seL4.
In particular, the Intel x64 version of seL4 now has a functional correctness proof from abstract specification down to the C code.
This brings the number of architecture configurations seL4 is verified for up to three (ARMv7, ARMv7 with hypervisor extensions, Intel x64) with a fourth one (RISC-V) in progress.
The x64 functional correctness proof does not yet include the fast path, VT-x, or VT-d extensions, nor binary verification or the security proofs we have for ARM, but functional correctness is the core part for all of these other properties and is in itself a big step forward for reliability of the x64 code base.
As usual, the proofs and code for seL4 are available on https://github.com/seL4/l4v and https://github.com/seL4/seL4.
Enjoy! Gerwin for the Trustworthy Systems Team