I think to make software more reliable, you'd have to go back to the "waterfall" method of development.
If we went back to Dijkstra's notion of correctness by construction, then a specification for the program would be made, and then a programmer would prove their part of the code correct to the specification. They would write the precondition and postcondition of every effectful statement, document the invariant of every loop, and prove by induction that each loop does what it's supposed to do. Basically, annotate your program with Hiare triples. (There are books about how to do this). Then, extensive tests should be run for as much of rhe program as possible.
Nowadays, we have tools for this so that we don't actually have to write a proof by induction for every loop; instead, we have bounded model checkers. In theory, the manual proof writing could be isolated to the parts of the program whose properties a bounded model checker cannot verify.
However, it seems like this whole plan is infeasible unless regulations are written that enforce this onto the industry. It would make them a lot less productive, and therefore less profitable. The only benefit would be that software is more reliable. By necessity, it would have to become simpler, too. For instance, there's absolutely no way that web browsers like Chromium, with 38 million lines of code, will ever be verified, because they're too large and complex.