Comment by Confusion

What isn't yet clear to me about these kinds of proofs: how can you verify that this proof is correct? How can you know there isn't a wrong assumption or wrong bit of 'code' in those 5500 lines? Would it have been impossible for Voevodsky to make his original mistake in such a formalization? Obviously the point of his entire homotopy type theory project is that he thinks he couldn't have. But why are mistakes (near) impossible here?