Currently, there are many different formalisms that can be used to correctly display programs (for example, formalizations in evidence assistants, typed programming languages, separation logic, etc.). As others have noted, there is no automatic way to prove the correctness of a given program (see Stop Problem). However, the formalisms mentioned are often applicable to specific programs. (Such an application can be far from automatic and requires a huge amount of creativity.)
Another very important point is what we actually mean by proving the correctness of the program or, as you said, they prove that the program has no error. Even with formal methods, there is usually no way to say that nothing can go wrong with a program. The reason is that formal methods usually show that a program meets specifications.
You can imagine the specification as a logical formula (which contains some property about the program) and proof of correctness as a formal proof that the program satisfies this formula (i.e., has the corresponding property). Because of this setting, anything outside the specification is not even “considered” evidence. Therefore, in order to really show that there are no errors in the program, you will first need to write a logical formula that states that the program has no errors.
Therefore, it would be more honest to say that formal methods can often (without doubt) prove that a program does not have certain types of errors (depending on the specification used).