How are models constructed? As I understand, a model $\langle S,\sim\rangle$ of $\mathsf{ZFC}$ is a set $S$ coupled with some binary operation $\sim$, in which the axioms of $\mathsf{ZFC}$ hold (please correct me if I am wrong). It seems modern set theory is capable of producing models of all sorts. Something I cannot find much information on is how exactly these models are constructed: what kind of sets do set-theorists consider to build useful models? A brief insight into this would be appreciated.
 A: In $\text{ZFC}$ alone, there may not be any actual sets that models ZFC. Additional assumptions are necessary. For example $\text{ZFC} + \text{Con(ZFC)}$ implies there is a set model of $\text{ZFC}$. More useful additions to $\text{ZFC}$ which imply the existence of set models of ZFC are the so called large cardinal axioms. If there exists a weakly inaccessible cardinal, call it $\kappa$, then the set $L_\kappa \models \text{ZFC}$. 
There are other constructions in set theory used to produce consistency results which are not really models of $\text{ZFC}$. These include the familiar inner model $L$ used to establish the consistency of $V =L$, axiom of choice, $\text{GCH}$, $\diamondsuit$. These are not sets but some definable collection of a given universe of set theory. More precisely these are just some first order formula $\varphi(x)$. $L$ is just some collection defined by some formula $\psi(x)$. 
In consistency proofs, proper class models are used as follows. Let $(M, E)$ be a proper class structure. That is, $M$ is defined by some formula $\phi$ and $E$ is defined by some formula $\psi$. Given a formula $\sigma$ in the language of set theory, one can relativize the formula in $\text{ZFC}$ to obtain $\sigma^{(M,E)}$. (More generally these are relativized interpretation of a language in a theory.) The relativization is defined recursively but roughly you replace $(\exists x)$ in $\sigma$ with $(\exists x)(\phi(x) \wedge ...)$ and $x \in y$ with $\psi(x,y)$. You say that $(M,E)$ models $\sigma$ if and only if $\text{ZFC} \vdash \sigma^{(M,E)}$ holds in your original universe. So $(M,E)$ is a model of $ZFC$ if and only if $\sigma^{(M,E)}$ holds for all $\sigma \in \text{ZFC}$. 
Now suppose you want to show that the consistency of ZFC implies the consistency of $ZFC + \sigma$ for some sentence $\sigma$. One such way would be to produce a proper class model $(M,E)$ such that $\gamma^{(M,E)}$ holds for all $\gamma \in \text{ZFC}$ and $\sigma^{(M,E)}$ holds. Now suppose that $\text{ZFC} + \sigma$ was inconsistent. Then there are finitely many axioms $\gamma_1$, ..., $\gamma_n$ of $\text{ZFC}$ such that $\{\gamma_1, ..., \gamma_n, \sigma\} \vdash 0 = 1$. Then $\text{ZFC} \vdash (\gamma_1^{(M,E)} \wedge .... \wedge  \gamma_n^{(M,E)} \wedge \sigma^{(M,E)}) \Rightarrow 0 = 1$. However by assumption, $\text{ZFC} \vdash \gamma_k^{(M,e)}$ and $\text{ZFC} \vdash \sigma^{(M,E)}$. Hence $\text{ZFC} \vdash 0 = 1$. This contradict the consistency of $\text{ZFC}$. 
The other construction common in set theory is the forcing construction. Forcing models are sets but they are not models of all $\text{ZFC}$, which can not necessarily exists by the incompleteness theorem. These are models of fragments of $\text{ZFC}$. One approach to these is to take a countable transitive set $M$ and some poset $\mathbb{P}$ and use a $\mathbb{P}$-generic filter over $M$ called $G$ and make another transitive set called $M[G]$. The construction is long but not really difficult and can be found in Jech or Kunen. 
More importantly these transitive are used in consistency proofs in the followng way: By the reflection theorem, the downward Loweinheim-Skolen, and Mostowski collapse, for any finite amount of $\text{ZFC}$, there is a countable transitive set model of that fragment. Now suppose one wants to show $\text{ZFC} + \sigma$ is consistent relative to $\text{ZFC}$. Suppose it is not. Then there is a finite set $\Gamma \subseteq \text{ZFC}$ such that $\Gamma \cup \{\sigma\} \vdash 0 = 1$. The forcing results shows that there is some finite subset of $\Sigma \subseteq \text{ZFC}$ such that $\text{ZFC} \vdash M \models \Sigma \Rightarrow M[G] \models \Gamma \cup \{\sigma\}$, where $M$ is a countable transitive set and $G$ is a generic filter for a judicious choice of poset $\mathbb{P}$. By the remark above, there is always a countable transitive $M$ such that $M \models \Sigma$ and generic $G$. So $\text{ZFC} \vdash M[G] \models \Gamma \cup \{\sigma\}$. But $\Gamma \cup \Sigma \models 0 = 1$. Hence $\text{ZFC}$ prove that there is a model of $0 = 1$. This contradicts the consistency of $\text{ZFC}$. 

So without additional assumptions added to $\text{ZFC}$, there may not be any model of $\text{ZFC}$. However, what are often called "models of $\text{ZFC}$" in set theory are these constructions of things resembling models that are used for establishing consistency. 
A: We don't really construct models of $\sf ZFC$. Not out of thin air, like we would construct models of other theories from thin air (well, from the empty set (well, by iterating a lot of set theoretical operations to construct enough sets from the empty set so we can construct the other models)).
In the case of models of $\sf ZFC$ we have to assume that they exist. We often assume more, that nice models exist. Sometimes we assume enough to have that sufficiently many nice models exist in which case we can cherry pick and say something like "Let $M$ be an elementary submodel of ...", which will allow us to have certain properties in $M$.
However, once you do have some models of $\sf ZFC$ then you can construct more using either model theoretic methods (compactness, Lowenheim-Skolem, ultraproducts) or using set theoretic methods (forcing, inner models). The latter is what we often use because these methods preserve "nice properties" of our original models.
But we don't construct them per se. When we do say that we construct models then we often mean that in one of two ways:


*

*We use forcing or inner models to create (or rather prove the existence of) models, given the existence of other models.

*We don't construct sets. Rather we construct proper classes. When we do that we essentially use the same set theoretic methods as above, but we don't end up with sets, but rather with classes. The distinction is very important, since the existence of set models is unprovable, but the existence of classes which [in the meta-theory] satisfy $\sf ZFC$ (and more, or less) does not prove the consistency of $\sf ZFC$, so we're not running into problems with incompleteness.
A: This is just completeness theorem and there is nothing specific to ZFC here. P. Cohen gives, in my opinion, a very readable account of this in the first chapter of his "Set theory and continuum hypothesis".
