seL4 has a proof of noninterference. As OP shows, this is an extremely strong property.
Comprehensive formal verification of an OS microkernel (2014)
Interestingly, original seL4 didn’t satisfy noninterference, because userland could affect kernel scheduling decisions. They rewrote the scheduler to be isolating while developing the proof. Details are in the paper.
Thanks for sharing this. This paper is incredibly interesting. You should submit it as its own story :)