Thank you for your reply, but I have to say that I think it understates the problem.<p>&gt;The source code for the contract can be made to have a proof of correctness in it..<p>Has this capability already been implemented for the Ethereum contract language(s)? If so, I would greatly appreciate a link, as my admittedly cursory search did not find it (there is some discussion of verification of the Ethereum infrastructure, but that is merely a precondition to contract verification.)<p>Even so, I think it is significant that only a tiny fraction of today&#x27;s software is written this way, and only a tiny fraction of all developers know how to do it. Someone has to write these contracts.<p>&gt;... or, as it is probably not all that long...<p>Ethereum&#x27;s promoters are imagining nothing less than a revolutionary new economy, with vast networks of interacting contracts. The amount of contract software implicit in these dreams is huge.<p>&gt;If you look at the source code long enough you can be sufficiently convinced that it runs how you expect it to.<p>The steady stream of security vulnerabilities that are being found in ordinary software shows that this is not an effective technique. If you are a software developer, imagine doing your work in an environment where any bug of yours could cause you, personally, to lose a significant amount of money.<p>Nor do I think &#x27;gas&#x27; completely solves this problem. Now your analysis has to cover the issue of whether your contract, or any of those it is dependent on, will run out of gas before completion. In most cases, and particularly in networks of dependent transactions,  reverting back to the initial state is not a viable outcome (imagine that happening on the last payment of your mortgage on a house.) I can imagine that running out of gas on some obscure corner case might be used by an attacker as as a means to disrupt a network of dependent transactions.