Instead of just thinking about the proof in your mind or putting it in comments you can actually embed pre/post conditions and compile time proofs in actual code using ADA SPARK. You use Pre and Post aspects for subprograms and pragma Invariant for loops and such constructs. The spark toolchain will run provers against your code and show if it can show the proofs hold.