Comment by tkz1312

sel4 is implemented 3 times: in c, haskell and isabelle/HOL.

The implementation in isabelle is proven to satisfy various key high level security properties. All 3 implementations are proven to be semantically equivalent. The compiled assembly output from gcc is also proven to be semantically equivalent to the C implementation.

Having these implementation layers is helpful for the proof work since the highest level properties can be proven over a much simpler and highly abstracted implementation (in issabelle / HOL), and the layers make the chain of equivalence proofs down to assembly more tractable. Most of the proof work is done in isabelle with the final C <-> assembly proofs using a custom automated smt based proof engine implemented in python.

The trusted components are the various language semantics / import tools, as well as a few very low level pieces of actual OS code (mostly parts of the early boot sequence iirc).