> Ideally you'd have a set of properties that the contract must hold, then prove that X satisfies those properties.
The issue is that how do you know you have the correct set of properties that a contract must hold? You might think you have all the properties that you need, but realize later that you missed one that is critical for your desired outcome.
Fair enough, but that problem exists regardless of whether you’ve bothered to formally verify the functionality. Gathering requirements is hard, in other words.
My concern is that the verification will provide a false sense of security. This article, for example, seems to be arguing that the verification means there can’t be flaws. I think misunderstanding requirements is much more likely than they are making it seem.
The issue is that how do you know you have the correct set of properties that a contract must hold? You might think you have all the properties that you need, but realize later that you missed one that is critical for your desired outcome.