The proof of Godel's theorem is based on the existence of a program which correctly checks proofs. So I would say that proof checking is a classic example, perhaps the classic example, of something that can be done correctly. In fact, that is literally the assumption of Godel's theorem---it says that if proofs in an axiom system can be checked using a computer, then there are statements in the language which can't be proved.