What happened to those developments that started in the 70s where you have automatic formal proofs that a piece of code does what it is supposed to do?

The stochastic parrots we have today are pretty good at doing that kind of tedious, extensive, franky mind numbingly boring stuff. They're also fast enough that you can "afford" to take the time / effort required to do those kinds of proofs where they are warranted - it makes them "a good idea" in a lot more places than they used to be when they were so much more expensive to perform.