It’s not done because software development is an unregulated shitshow full of wildly unethical companies scrambling for the bottom. It’s not unlike early aerospace, or early medicine, or any frontier which develops rapidly before legal frameworks inevitably close in.
This is not true at all. First of all, there's no such thing as being able to mathematically prove a design is sound in any engineering discipline, software or non-software. After all, it is infeasible if not impossible to encapsulate all the details of the implementation of _any_ system in mathematics or any other system of reasoning (down to every last atom, if you stretch your imagination).
All we have in engineering (non-software) is something like safety factors and confidence, and this is done with (usually) rigorous mathematical models as well as loads and loads of testing to fill in the gaps of mathematics (think unknown constant/parameters, assumptions, etc).
None of this is impossible to do for software. There are systems that enable one to do easy/entry level verification (such as something like TLA+), to much more complicated reasoning (something like COQ). This will allow the system designers to gain confidence in if the system will work and gain understanding about under what scenario they will fail. Contrast this with the existing software landscape, which is mostly, at least from my perspective, just let me write some stuff until things do approximately what I want. Even at the top of the ladder, I feel the tests conducted are "adhoc" at best and with none of the rigours that you associate with traditional engineering fields.
