Implications of a model of ZFC By the completeness theorem ZFC is consistent if there is a model where ZFC is true.
What would happen if we found a model for ZFC? Would we be able to stop worrying if ZFC is inconsistent? 
Are people trying to find such a model?
Or is there a proof that no such model exists?
My model theory and set theory is weak in general, but I understand basic ideas.
 A: Gödel's second incompleteness theorem tells us that ZFC (if it is consistent) cannot prove that ZFC is consistent. Therefore, ZFC (if it is consistent) cannot prove that there is a model of ZFC, either. Thus we do not have a proof that no model exists, but we do have a proof that trying to find such a model is a pointless pursuit.
If you make stronger assumptions, such as assuming the existence of large cardinals, then you can prove that models of ZFC exist, and you can study them.
A: The question is always what are you willing to take "on faith". This is a source of tension between "minimal hypotheses" and "convenient hypotheses".
On the one hand, if you're willing to assume that set theory (by which I mean $\sf ZFC$ or one of its close relatives) is your meta-theory, you might as well assume that it is consistent. Because why would you work in a meta-theory which isn't consistent? And so you might as well assume that $\sf ZFC+\operatorname{Con}(ZFC)$ is also consistent, and so on.
Now since you've already made these "oh well" assumptions, you can indeed use Gödel's completeness theorem and see that $\sf ZFC$ has a model, and in fact it has a model in which $\sf ZFC$ is internally consistent, and so on.
But now, since we've made all of these "oh well" assumptions, since for "any reasonable iteration of the consistency operator" we assume the consistency statement, we must have gone through $\omega_1^{CK}$, so our meta-theory is not computable anymore. And that's not nice, and we don't want that.
So in order to salvage this, we need to set a recursive upper bound on the consistency operator. Call this new theory $T$. So now we're working in $T$ but we are not assuming $\operatorname{Con}(T)$. But it doesn't really change a lot from assuming just $T=\sf ZFC$. So we might as well do just that. The key observation here is that there is a bound which we can compute on how many times we are guaranteed that the consistency operator is iterable.

Now what about large cardinal axioms? Well, indeed even the statement "There is a well-founded model of $\sf ZFC$" already gives us a lot of consistency power relative to the above, and of course this statement is a consequence of all large cardinal axioms, you can now apply the above argument to the theory $\sf ZFC+\varphi$, where $\varphi$ is your large cardinal axiom(s).
So at the end of the day, you're not gaining a whole lot.
Now, what does it matter if we make these assumptions or not? At the end, it matters very little in terms of results. We need to have some agreed upon meta-theory in mathematics, and even if it's not $\sf ZFC$ per se, it is something which can be easily interpreted in $\sf ZFC$ (or its close relatives, or arguably an even weaker theory) in the most cases, perhaps much to the dismay of some people.
But we need to have some common denominator. And due to historic reasons that is "more or less $\sf ZFC$". So by adding new axioms we are deviating from this norm. It's not necessarily a bad things, these axioms can—and often do—simplify many arguments in mathematics, but we have some ways of stripping them from the proofs in most cases.
(For example forcing can be developed by working over a countable transitive model of $\sf ZFC$, but in fact we can develop forcing in arithmetical meta-theories, and there's no need to assume anything beyond that. It just that these additional assumptions illuminate and clarify the arguments, the proofs, and the results.)
