Thanks! One of the things I find useful for avoiding overconfidence in proof results, beyond making sure to test the proof on multiple broken versions, is to s

Thanks! One of the things I find useful for avoiding overconfidence in proof results, beyond making sure to test the proof on multiple broken versions, is to spell out many additional implications of the function that I and/or the caller might expect of it and ask for proofs on them too, even if they seem somewhat redundant. For example, cout = 2ab + cin; I would also prove that for all a,b,cin that cout >= cin; for a or b ==0 that cout == cin, etc.