Chiming in to the chorus: what do you use for that type of programming? How does it support the kinds of formal proofs you mentioned? Although I have proven the correctness of some simple code, I have found that the proof and the code can diverge too much to mean much. (Some of people interviewed in Coders at Work said the same thing.) Do your tools unify the proof and the code somehow?
