That's just half of the problem though. The other half is knowing that your specification doesn't admit any unpleasant behaviors. I expect some combination of KISS and model checking is appropriate.
[1] https://en.wikipedia.org/wiki/Predicate_transformer_semantic...
As for the second part, do you know off the top of your head if [not checking whether the proved behavior admits abuse] was the issue that resulted in "millions of dollars" worth of coins being stolen in the various debacles we hear about? I have an inkling that almost every time, it's actually this.
The only one I ever looked into was the 2016 DAO[1] hack and I didn't get the impression that it was because they didn't check their code for spec violations, rather they just designed a system that allowed someone to do something bad. I have no idea how we can prevent this, even with all the power of theorem provers.
Like most of his work, the general theme is "how can we avoid making a mess of things unnecessarily?" Avoiding needless complexity is clearly the programmer's greatest challenge.
[1] https://www.goodreads.com/book/show/3144463-predicate-calcul...
[2] https://www.goodreads.com/book/show/2276288.A_Discipline_of_...