Yeah this seems like the specification/implementation problem. One can perfectly implement a bad spec, but coming up with the perfect spec is a human problem.

It's possible you could at least mitigate the problem by checking that what you've proven isn't trivial. If you slightly change a mathematical statement, it frequently becomes either trivially true or trivially false. So if you accidentally proved the wrong thing, there's a good chance that your proof can be shortened to a point that it becomes obviously wrong. For example, if you accidentally put "there exists" instead of "for all" in Fermat's last theorem, the proof is 1^3 + 1^3 != 1^3. That is obviously too short to prove FLT - it would have fit in Fermat's margin.

It's interesting that this rather fundamental problem doesn't seem to have an established name and Wikipedia article. At least I couldn't find one. Perhaps the problem is too obvious.