Checking invariants and bounded model checking. What is a formal proof?

03-01-Live1, CS-550 Formal Verification