I'm mostly with you.

But strictly speaking, ‘ZF is consistent.’ is not a statement with an absolute meaning, because it is itself a statement about a completed infinity. I have high confidence that no inconsistency in ZF has a formal proof of feasible length, but I really have no opinion about whether it has an inconsistency of length 3^^^3; we haven't come close to exploring such things.

These feasibility issues are definitely interesting. Another possibility is that there is a formal proof of feasible length, but no feasible search will ever turn it up. (Well, unless P = NP). Yet another possibility is that a feasible search will turn it up, I certainly regard it as more likely than most people do.

To the extent that I have this intuition, this is mostly because people have used these systems without running into inconsistencies so far. (At least, not in the systems, such as ZF, that people still use!)

I agree that this counts as evidence, but it's possible to overestimate it. Foundational issues hardly ever come up in everyday mathematics, so the fact that people are able to prove astonishing things about 3-manifolds without running into contradictions I regard as very weak evidence in favor of ZF. There have been a lot of man-hours put into set theory, but I think quite a bit less than have been put into other parts of math.

(Come to think of it, I believe that my Bayesian probability as to whether ZF is consistent to such a degree ought to be quite low, for essentially the same reason that a random formal system is likely to be inconsistent, although I'm not really sure that I've done this calculation correctly; I can think of at least one potential flaw.)

JoshuaZ and I had a discussion about this a while ago, starting here.