The solidity programming language is expected to support embedded proofs in the near future, so that contract developers can specify invariants that are guaranteed to hold true if the contract compiles... so you'll be able to state things like "No person other than the depositor in a bank will be able to withdraw the money" and the compiler will generate a proof to verify this, visible to any users of the contract.

(That said, this is an EXTREMELY ambitious feature and I'm mildly skeptical that they'll be able to deliver it... but the team working on Solidity has put out very good work so far...)

A very good question about a very hard problem.

We've discussed a variety of approaches. The one I like best is that "contract interpreters" offer a professional service, which is that they read a contract and tell you what it will do. You pay them for this service, and they have a public bond of sufficient size that if they screw up, a claim against their public bond will make the person affected whole.

This assumes a few things: dispute resolution services, flexible escrow agreements, and a lot of human judgement in a relatively corruption-free environment. My guess is that this is going to be expensive to provide, and might well rest up against existing contracting infrastructure (i.e. KPMG type agencies might offer a blockchain auditing service with insurance in some imagined futures.)

Hence I'd expect a long tail from high value, deeply audited contracts with insurance and bonds to back them up, through to collaborative pools that just note when they've been ripped off, down to "it worked for me!" reviews on forums.

I'm not sure there's a better solution than this, but it's a topic of ongoing research and discussion.

So, one potential idea is to incentivise developers to "audit" smart contracts in repositories. The metrics of the audit score can then be shown to the end user to let them make the decision as to whether a smart contract is safe or not.

It's a start.