@skematica …but seL4 does have a machine-verified proof of its correctness and security. ;)

/ @kdfrawg