seL4 actually makes proofs for some core isolation promises, like realtime-ness and data flow adhering to capabilities (though with neglect of side channels for that aspect, which can be corrected for by also verifying the code that runs on top to not do shady stuff to probe side channels).