"ZF can quote formulas as structured, and encode models as sets, and then represent a finite ZF-formula which says whether or not a set of quoted formulas is true about a model. ZF can then prove that no step of classical logic goes from premises that are true inside a set-model, to premises that are false inside a set-model. In other words, ZF can represent the idea 'formula X is semantically true in model Y' and 'these syntactic rules never produce semantically false statements from semantically true statements'."

Wait, then why can't ZF prove itself consistent? If ZF believes in all the axioms of ZF, and it believes that logic never produces false statements from true statements -

"Ah, but ZF can't prove that there exists any set which is a model of ZF, so it can't prove the ZF-axioms are consistent.

Note: this is actually connected to an ambiguity in "ZF believes in all the axioms of ZF". That system has infinitely many formal axioms, and lacks any finite way to assert them all at once (eg, to use them all in a particular proof). If it could, then it could use a principle appropriately called "reflection" to show that they must all be true inside a particular set - a natural model like the ones Eliezer talks about in the OP, though not provably as large as those - and could thus prove itself consistent.