Comment by aureianimus

There's no guarantee that the intermediate statements match the informal mathematical intermediate statements, but if there is a mismatch, then this has to be repaired elsewhere to yield a proof that passes the Comparator tool. Running this tool indeed reduces the correctness question to what the parent comment mentioned.