[cocoafleck]

I feel obligated to point out that there are tools that effectively repair broken proofs, but they just aren't labeled as such. For example, Frama-C is a program that takes in a simplified written proof (in a C comment language), and then validates it (as in the tedious middle steps) with z3, cvc4, etc. Unfortunately, Frama-C can't handle dynamic memory yet, and it doesn't handle array sizes correctly forcing for loops over memcpys in some cases if you want to prove anything. I wouldn't recommend it for actual usability, but it does seem to "repair" proofs (as in they were never non-broken/whole in the first place).