Proving that your algorithmic design is correct (to the degree the proof tool can assure) is already a big help - even if your implementation of the algorithm might still have bugs.

At least now you know it's just bugs you need to fix, and not a faulty logic to begin with.