There's been security evaluations of products where evaluators do both checklist stuff and try to hack the product. Consumers could buy the stuff that gets cleared through those processes. For instance, there's products on the market like INTEGRITY-178B and LynxSecure designed specifically for securely partitioning systems. They have networking stacks available, too. On occasion, a company would make things like routers with them. Virtually nobody bought them because they cost more than insecure devices or lacked unnecessary Thing X, Y, or Z. Intel tried with i432 APX, BiiN with i960 CPU (a nice one), and Itanium w/ security enhancements Secure64 SourceT uses. Lost a billion dollars or something over the three. So, those companies usually folded, withdrew the products, or switched to selling for outrageous amounts to defense sector.

So far, almost no money is going into stuff with higher assurance of correctness. Those companies are losing money when they try though. So, the market naturally responded to the demand. I strongly discourage anyone from even trying again given the cost and fact that users won't buy it. Instead, I recommend making a product that's decently secure that can be secured later. Make it good enough to sell on its own with great marketing and so on. As money comes in, move a percentage of it toward improving its overall assurance. Basically takes a nonprofit and/or ideological group that wants strong security to happen at a loss or at least opportunity cost to get it done. CompSci people also make strong designs with FOSS code that often needs polish. Companies can pick up their ideas or prototypes to convert into something that can sell. Alternatively, team up with them to split the work into what each can financially sustain and are good at. That's happening with CompCert whose innovations come from CompSci but sold by AbsInt. K Framework people and Runtime Verification Inc. are another good example with one coming from the other.