The objective of our research is to build environments where formal proofs of programs are integrated into software development. We present recent work on proofs of Java or C programs in the tools Caduceus and Krakatoa and show how correctness of programs is insured by a chain of program transformations.