Yes, this! What would be helpful is if formal methods were powerful enough to be able to prove contracts and assertions about expectations and invariants; howe

Yes, this! What would be helpful is if formal methods were powerful enough to be able to prove contracts and assertions about expectations and invariants; however, all formal systems I've experienced are not powerful enough to do this at scale in any interesting program, not without spending way more time reconstructing the entire system in the formal world, with the attendant likelihood of introducing spec bugs in that reconstruction. It is entirely different in the world of hardware, where the specification in many cases is the RTL and the thing being proved is the, supposedly identical, physical implementation.