in general, formally verifying software is a must if you're doing something that cannot have any maintenance done to it
take for instance, deep space stuff
software on those is usually formally verified to ensure it is completely bug-free, because you can't really afford to fix bugs in prod
but smart contracts, for some reason, are treated as a normal computer app, instead of something where a bug can mean all your apes, gone