"The most comprehensive formal systems yet set up are, on the one hand, the system of Principia Mathematica and, on the other, the axiom system for set theory of Zermelo-Fraenkel (later extended by J. v. Neumann). These two systems are so extensive that all methods of proof used in mathematics today have been formalized in them, i.e. reduced to a few axioms and rules of inference. It may therefore be surmised that these axioms and rules of inference are also sufficient to decide all mathematical questions which can in any way at all be expressed formally in the systems concerned. It is shown below that this is not the case, and that in both the systems mentioned there are in fact relatively simple problems in the theory of ordinary whole numbers which cannot be decided from the axioms."
From "On Formally Undecidable Propositions of Principia Mathematica And Related Systems" by Kurt Gödel, 1930
I am aware of Godel, thanks, and of course that choice / Zorn's / well ordering (not to mention CH) are independent of ZF (and in particular that's why I mentioned ZFC). I'm also willing to accept the existence of an inaccessible cardinal, which bears on ZFC's consistency.
Ultimately my belief is this: there was a very real crisis in foundations at the end of the 19th century and over the next several decades this was fixed as best as it could be. The edges of the foundation are not perfect, the edges of the foundation cannot be perfect, but the edges of the foundation have been pushed back so far that for nearly every working mathematician they're good enough. (and if the algebraic geometers need Grothendieck universes, I'm ok with that)
