I read this and thought, "this can't be right, they must be assuming some things." According to them, they, sensibly, are indeed assuming some things to be cor

I read this and thought, "this can't be right, they must be assuming some things." According to them, they, sensibly, are indeed assuming some things to be correct without proof: http://sel4.systems/Info/FAQ/proof.pml http://sel4.systems/Info/FAQ/proof.pml This is effectively the same idea behind Rust's `unsafe`. It represents the things you assume to be true. Of course, when compared to seL4, the scales are massively different. :-)