Can you expound in this some? I am not fully grasping your point. Are you saying "building safe by default" is a bad thing or assuming "safe forever" is a bad thing. Or are you saying something entirely different?
It is almost impossible to prove a program is "correct". But things like memory safe languages, static typing, and automated tests allow us to prove the ways in which it is not "incorrect". And the more places it is not incorrect, the more likely it is to be correct (even if we can't prove it).
I meant that it's over-reach to say it's completely trustworthy just bc it's written in a GC/borrow checked language.