Suppose I have a simple program that implements an algorithm (say depth-first search), written in a simple imperative programming language with the standard for loops, recursions, conditional statements and so on. It takes in a well-specified input and has a well-specified output.
Suppose I want to verify that it always produces the correct output for each input. I can treat the program as a mathematical object subject to certain rules of the programming language. I write a formal mathematical proof, assuming the usual axioms of ZFC and first-order logic, to show that this is true.
How would I know that my program definitely works (i.e. for all inputs, output correctly) due to this proof? I do know that in the ZFC axiom system, my program works because it is defined to work (it is deducible formally). However, it seems that the correctness of my program does not require the full machinery of ZFC; its only axioms are the rules of the programming language. Commonly used proof techniques like mathematical induction are founded on axioms in ZFC, but we do not yet know that these hold due only to the rules of the programming language.
Is it possible that my program does not actually work, but it is proven to work in ZFC? If that's the case, why are all algorithms proven in the usual framework of ZFC (assuming all axioms of set theory, and first-order logic)?
EDIT: Can formal verification of programs (with 100% certainty according to specifications of the programming language) be done in ZFC? I am assuming it can be done under weaker axiom systems (e.g. Hoare logic)?