Does this move the bugs from the implementation language to the language of the verification spec? Or is there a way to express some generic requirements such as "don't strand assets"?
Presumably one would have to first formalize that constraint (taking care, for example, that 'not stranded' is not being satisfied by someone stealing the assets), and then, unless the language makes it impossible, prove that it is not violated anywhere. In Solidity, it is a long deductive chain from the specific bug here to the realization that it could lead to stranding.
