Formal verification is a very time consuming process. Designing something that can be formally verified is very consuming process. seL4 is just few thousand lines of code, so it can be designed (microkernel) and formally verified. Something the size of OpenBSD kernel with all the drivers is beyond resources such as work hours.
Even then formal verification it does not tells you that you can be sure this system is secure. It only proves that code is doing everything that is written in description of code. If assumptions of description are incomplete or wrong, the code probably have bugs.
Of course formal verification improves code quality by orders by magnitude.
You also should keep in mind that world changes. Hardware changes. Protocols are changing. Your project must be flexible enough to adapt to this changes and incorporate new features at reasonable pace.
https://theinvisiblethings.blogspot....rnels-and.html