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...)