@ocicat
Mathematically proven software often have not one, but a several of them. Each proof is about one thing.
A lot of your doubts are addressed by seL4's FAQ.
https://wiki.sel4.systems/FrequentlyAskedQuestions
https://sel4.systems/Info/FAQ/proof.pml
Mathematically proven software competes with high-assurance software. Software is used not only by laptops, smartphones and servers. There are also microcontrollers found in cars, planes. Software found in them is more stable (or at least should be because life depends on it and it is doable) than OpenBSD, Gnu/Linux, Windows and any other general-purpose operating system by a few orders of magnitude. There are people who know how to do it.
Of course verification of all OpenBSD code is beyond Project resources and I doubt that even biggest IT corporations could do that.