I think there's definitely something to the notion that there will be correlation between things you forget to (try to) guarantee in your code and things you th

I think there's definitely something to the notion that there will be correlation between things you forget to (try to) guarantee in your code and things you think to test for. It's not clear to me that it's meaningfully stronger than the correlation with things you forget to prove. Any which way, more prodding of the model (mental or more formal) is probably going to help correctness but may or may not be worth the cost, depending.