Yes, the seL4 specification comes with proofs of strong integrity and information flow security guarantees, and with integrity and authority confinement proofs.

Yes, the seL4 specification comes with proofs of strong integrity and information flow security guarantees, and with integrity and authority confinement proofs. It also comes with a configuration that is proved to be a static separation kernel. The implementation, including the code emitted by gcc, implements this specification, and is guaranteed to be free of buffer overflows, pointer errors, memory leaks, arithmetic overflows, and undefined behavior. [1] https://ts.data61.csiro.au/projects/seL4-verification/ https://ts.data61.csiro.au/projects/seL4-verification/