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