Foundation member Proofcraft has delivered a work package towards the verification of the MCS variant of seL4.
Having earlier started the design-to-code refinement proof of MCS seL4, funded by the Foundation, Proofcraft has now delivered the completion of the proof framework, setting up all the infrastructure and hierarchy of theorems about the approximately 500 C functions of the kernel.
This was made possible by a generous donation from Foundation member XCalibyte, for which the seL4 Foundation is very grateful. We are looking for further funding that will allow completion of the verification of the MCS variant. Once verified, MCS will become the default configuration of seL4, bringing the highest levels of assurance to mixed-criticality real-time systems.
