Consider the size of the "proof" that would be required. seL4 is a
micro kernel. Just a kernel, consisting of 1100 files, with 95,000 lines of code.
OpenBSD is a complete operating
system. That system consists of:
- A monolith kernel with more than 500 integrated drivers. The kernel alone is more than 7000 program files and contains nearly 3 million lines of code.
- The userland consts of approximately 3000 separate executables and libraries, consisting of nearly 70,000 program files and contains more than 21.5 million lines of code.
Good luck!
Sources:
OpenBSD -current /usr/src, find(1), xargs(1), wc(1), grep(1), and editors/libreoffice.
SeL4 project source at github: project seL4/seL4