Yes, because the standard formalism for forcing that Kunen uses starts with a countable transitive model of $\sf ZFC$, rather than just any countable model, more care is needed. Whether there is a transitive model of $\sf ZFC$ is independent from $\sf ZFC + Con(ZFC),$ though once you have one, you can get a countable transitive model by Lowenheim-Skolem + Mostowski collapse.
On the other hand, the reflection schema allows you to construct, in $\sf ZFC$ alone, a countable transitive model of any finite subtheory of $\sf ZFC$. Analyzing the forcing formalism, if we have an arbitrary finite fragment $T$ of $\sf ZFC + \lnot CH,$ it's possible to find a finite fragment $T'$ of $\sf ZFC$ such that we can, working in $\sf ZFC,$ construct a countable transitive model $M$ of $T'$ and show the generic extension $M[G]$ satisfies $T.$
If $\sf ZFC + \lnot CH,$ were inconsistent, there would be some finite fragment witnessing this, and then the above procedure would produce a contradiction in $\sf ZFC$ alone. So, as a bonus, this is no mere infinitary proof of $\sf Con(ZFC)\to Con(ZFC+\lnot CH)$ using model theory within $\sf ZFC$, but rather a finitary syntactic proof of $\sf Con(ZFC)\to Con(ZFC+\lnot CH)$.
On a side note, it is possible to carry out an independence proof that starts out like you suggested. Note that in the transitive approach, the construction of $M[G]$ uses the (external) well-foundedness of $M$ in an essential way. An analogous construction in the not-necessarily-well-founded case is possible, but more complicated$^*$. Between that complication and the fact that transitive models are nicer to work with for all sorts of reasons, the transitive models approach is generally favored as an introduction, despite the mild metamathematical hiccups it causes.
$^*$ One approach that works is to construct the relevant Boolean-valued model inside $M$ and then take a quotient of it by any ultrafilter. But then again, Boolean-valued models already produce a nice relative consistency proof on their own. See also this answer for a brief description, and JDH's answer to the same question for more on the BVM approach.
Best Answer
One possible poset would be as follows: Let $\mathbb{P}=[\omega]^{<\omega}\times U$, and $(s,X)\ge (t,Y)$ if and only if
Let $G$ be a $\mathbb{P}$-generic filter, and let $x_{gen}=\bigcup\{s\mid \exists X\in U: (s,X)\in G\}$. For each $Z\subseteq \omega$ that is not in $U$, consider $$\mathcal{D}_Z = \{(s,X)\in\mathbb{P}\mid X\subseteq \omega\setminus Z\}.$$ Then we can see that $\mathcal{D}_Z$ is dense. Hence there is $s$ such that $(s,\omega\setminus Z)\in G$. From this, we can see that $x_{gen}\setminus \max s\subseteq \omega\setminus Z$. Especially, $x_{gen}\cap Z\subseteq \max s$.
It remains to show that $\mathbb{P}$ has c.c.c. Let $\{(s_\alpha,X_\alpha)\mid \alpha<\omega_1\}\subseteq \mathbb{P}$. Since $[\omega]^{<\omega}$ is countable, we may assume that $s_\alpha$ is constant with value $s$. Hence it suffices to show that $(U,\subseteq)$ satisfies c.c.c., and in fact, every pair of elements of $U$ is compatible.