Many of those following the DeepSpec project will have heard of the verification of the seL4 microkernel. This talk will recap the seL4 verification project when first completed, and the engineering work that has been done to maintain and extend the proofs over nearly ten years since then.

Nearly all modern hardware is now multi-core. To support this, we have begun the most substantial change to the seL4 proofs to date. Supporting multi-core platforms requires new kernel mechanisms, but more importantly, requires the correctness properties of the kernel to handle concurrency. This talk will present the verification approach we have designed, and give an overview of the effort that remains to adapt the existing proofs into the new framework.