you could make a program that verifies that the code matches the proof and that the proof is sound, but then you have to verify the program, and verify the verification, and verify your system of logic is consistent, which by gödel's incompleteness theorem is impossible(?)