The better look at this is not to prove that you have no bugs is that to prove that a program conforms to a specification that Lean can verify.

Even with the addition of two numbers the execution of a program can be wrong if the CPU has a fault or if the runtime of the program has a bug.

I think you just need to look at why formal verification exists.