Yep. Imagine a prover that accepts all statements. It would accept a buggy program, and it would accept itself.

It would obviously help reduce errors but it wouldn't categorically eliminate them.