The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement is available as open source.
Read the white paper, Mathematically Verified Software Kernels: Raising the Bar for High Assurance Implementations.
Read the Brochure.
Meanwhile, if you're interested in learning more about seL4, please check out about seL4, or the Data61 seL4 project site. More generally, you can find out about Data61's trustworthy systems activities.
If you would like to learn how to build a system on seL4, you might want to follow the lectures and especially the seL4-based project of UNSW's Advanced Operating Systems course.