It depends on what you mean by that. In general we hope that the environment and theorum statements are correct. If they are, we know that the formal proof proves the theorum we want. If your asking how we know that the formal proof actually matches the informal proof, we do not.