I looked into SeL4 some years back for a potential project and along the way learned a reasonable bit about it. I recall that one of the things they were trying to do was to verify not just the design but that the compilation outputs match the designed outputs.
Yep... I’ve checked the site and confirmed my fuzzy recollections. https://sel4.systems/Info/FAQ/proof.pml has a pretty good summary that also has a nice TLDR explaining just what they are proving. “The binary code of the ARM version of the seL4 microkernel correctly implements the behaviour described in its abstract specification and nothing more.”
Yep... I’ve checked the site and confirmed my fuzzy recollections. https://sel4.systems/Info/FAQ/proof.pml has a pretty good summary that also has a nice TLDR explaining just what they are proving. “The binary code of the ARM version of the seL4 microkernel correctly implements the behaviour described in its abstract specification and nothing more.”