For contract-based programming, I'm personally planning on experimenting with Prusti: https://github.com/viperproject/prusti-dev

The withdraw example would look something like

    impl Account {
        #[requires(amount <= self.balance)]
        #[ensures(self.balance >= 0)]
        pub fn withdraw(&mut self, amount: uint) { ... }
    }

and Prusti has a good story for going from this to larger proofs.