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).

This reminds me of people who argue that, because P != NP, we will never prove this. (The key to the argument, IIRC, is that any proof of this fact will have very high algorithmic complexity.) I'm not sure how to find this argument now. (There is something like it one of Doron Zeilberger's April Fools opinions.)

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

Yes, these results should be formalisable in higher-order arithmetic (indeed nth order for n a single-digit number). It is the set theorists' work with large cardinals and the like that provides the only real evidence for the consistency of such a high-powered system as ZF.