Yes, one can undertake forcing without the transitivity assumption,
and even the countability of the model is not important.
One of the standard ways to do this is with the Boolean-valued
model quotient construction, which has been described in many places. Basically, given a forcing notion $B$,
a complete Boolean algebra (take the completion if you have only a
partial order), form the class of all $B$-names, and then define
the Boolean values $[\![\varphi]\!]^B$. This can be done internally
to any model $M$. If $U\subset B$ is any ultrafilter — no need for
genericity of any kind, and even $U$ inside $M$ is fine — then you define the
quotient $M^B/U$ by the equivalence relation $$\sigma =_U\tau\quad\iff\quad[\![\sigma=\tau]\!]\in U,$$ which is a congruence with
respect to the relation $$\sigma\in_U\tau\iff
[\![\sigma\in\tau]\!]\in U.$$ One then verifies the Łoś theorem property
that $M^B/U\models\varphi\iff[\![\varphi]\!]\in U$, and so $M^B/U$
is a model of any statement whose Boolean value is in $U$.
To construct a model of ZFC+$\neg$CH, for example, start with any model $M\models\text{ZFC}$, and let $U\subset B$ be any ultrafilter in the Boolean algebra arising from Cohen's forcing to add $\aleph_2$ many Cohen reals. The model $M^B/U$ will satisfy ZFC+$\neg$CH. No need for $M$ to be countable or transitive!
You can find further extensive details in my paper, Well-founded
Boolean ultrapower as large cardinal
embeddings, including
a discussion of what I call the naturalist account of forcing,
which describes how one can take the common set-theorist's talk of
"forcing over $V$" at face value.
Update. Let me respond to your comment and clarified question. You want to know where the argument commonly used with countable transitive models goes wrong without those assumptions. So let me explain.
Countability is clearly used in order to find the generic filter. Strictly speaking, one doesn't need that the entire model is countable, but rather only that the model $M$ has only countably many dense subsets of the forcing notion $P$ being used for the forcing. For example, one can easily find generic filters for any forcing notion in an $\omega_1$-like model, which is an uncountable model all of whose rank initial segments are countable. More generally, it suffices if there are only countably many maximal antichains for the forcing, since meeting these suffices for genericity. One can relax this a bit in certain cases. For example, if you have Martin's axiom or some other forcing axiom, and if $M$ has fewer than continuum many open dense sets for a forcing notion P that happens to be ccc in the ambiant universe, then it will be instance of the forcing axiom to know that there is an $M$-generic filter. And similarly with proper forcing and PFA and so on. So these are some ways in which you can dispense with the countability assumption and still get a generic filter.
Transitivity. The use of transitivity in the CTM approach to forcing is used critically in the definition of what $M[G]$ is. Namely, one usually defines $M[G]$ to consists of all the interpretations of names $\tau$ in $M$ by $G$, defining the value $$\newcommand\val{\text{val}}\val(\tau,G)=\{\val(\sigma,G)\mid\exists p\in G\ \langle\sigma,p\rangle\in \tau\}.$$ This definition takes place by $\in$-induction in a realm where both $M$ and $G$ exist. One cannot seem to carry out this induction on names if the model is not $\in$-standard or at least well-founded, and so this is the main point of failure with the usual CTM approach to forcing. Without transitivity or at least well-foundedness, we don't seem to know exactly what $M[G]$ should mean. This problem is addressed in the Boolean-valued model quotient construction by defining $M[G]$ as a quotient by an equivalence relation, rather than by the $\in$-inductive value procedure. Furthermore, if $G$ is $M$-generic for a non-well-founded model $M$, then indeed after forming the model $M[G]$ by the quotient construction $M^B/G$, then inside $M[G]$ one can see that it arises internally via the values-of-names construction. But the point is that without having first provided an alternative definition of what $M[G]$ is, one doesn't seem at first able to carry out that name-value process, because the induction takes place in context with both $M$ and $G$ already available. (And this subtle point, I believe, seems to be the answer to your question as updated by the revision.)
I have proposed such an axiomatization. It is published in Comptes Rendus: Mathématique, which has returned to the Académie des Sciences in 2020 and is now completely open access. Here is a link:
https://doi.org/10.5802/crmath.97
The axiomatization I have proposed is as follows:
Let $(M, \mathbb P, R, \left\{\Vdash\phi : \phi\in L(\in)\right\}, C)$ be a quintuple such that:
$M$ is a transitive model of $ZFC$.
$\mathbb P$ is a partial ordering with maximum.
$R$ is a definable in $M$ and absolute ternary relation (the $\mathbb P$-membership relation, usually denoted by $M\models a\in_p b$).
$\Vdash\phi$ is, if $\phi$ is a formula with $n$ free variables, a definable $n+1$-ary predicate in $M$ called the forcing predicate corresponding to $\phi$.
$C$ is a predicate (the genericity predicate).
As usual, we use $G$ to denote a filter satisfying the genericity predicate $C$.
Assume that the following axioms hold:
(1) The downward closedness of forcing: Given a formula $\phi$, for all $\overline{a}$, $p$ and $q$, if $M\models (p\Vdash\phi)[\overline{a}]$ and $q\leq p$, then $M\models (q\Vdash\phi)[\overline{a}]$.
(2) The downward closedness of $\mathbb P$-membership: For all $p$, $q$, $a$ and $b$, if $M\models a\in_p b$ and $q\leq p$, then $M\models a\in_q b$.
(3) The well-foundedness axiom: The binary relation $\exists p; M\models a\in_p b$ is well-founded and well-founded in $M$. In particular, it is left-small in $M$, that is,
$\left\{a : \exists p; M\models a\in_p b\right\}$ is a set in $M$.
(4) The generic existence axiom: For each $p\in \mathbb P$, there is a generic filter $G$ containing $p$ as an element.
Let $F_G$ denote the transitive collapse of the well-founded relation $\exists p\in G; M\models a\in_p b$.
(5) The canonical naming for individuals axiom: $\forall a\in M;\exists b\in M; \forall G; F_G(b)=a$.
(6) The canonical naming for $G$ axiom: $\exists c\in M;\forall G; F_G(c)= G$.
Let $M[G]$ denote the direct image of $M$ under $F_G$. The next two axioms are the fundamental duality that you have mentioned:
(7) $M[G]\models \phi[F_G(\overline{a})]$ iff $\exists p\in G; M\models (p\Vdash\phi)[\overline{a}]$, for all $\phi$, $\overline{a}$, $G$.
(8) $M\models (p\Vdash\phi)[\overline{a}]$ iff $\forall G\ni p; M[G]\models \phi[F_G(\overline{a})]$, for all $\phi$, $\overline{a}$, $p$.
Finally, the universality of $\mathbb P$-membership axiom.
(9) Given an individual $a$, if $a$ is a downward closed relation between individuals and conditions, then there is a $\mathbb P$-imitation $c$ of $a$, that is, $M\models b\in_p c$ iff $(b,p)\in a$, for all $b$ and $p$.
It follows that $(M, \mathbb P, R, \left\{\Vdash\phi : \phi\in L(\in)\right\}, C, G)$ represent a standard forcing-generic extension: The usual definitions of the forcing predicates can be recovered, the usual definition of genericity can also be recovered ($G$ intersects every dense set in $M$), $M[G]$ is a model of $ZFC$ determined by $M$ and $G$ and it is the least such model. (Axiom $(9)$ is used only in the proof that $M[G]$ is a model).
Best Answer
Guillaume :
There are several ways of making sense of forcing. It is useful to be able to move between all these versions, as each may have its specific advantages in some cases.
The approach of consider countable transitive models $M$ and their extensions by explicit construction of generic objects is very useful, although somewhat restrictive, and we do not really need the restrictions it imposes.
For example: One can use a purely syntactical approach, where we transform formulas into forcing statements, and never worry about models. In turn, there are several ways of doing this. We can, by simply manipulating formulas, check that the weakest condition forces the axioms of first order logic, and we can apply modus ponens and the rules about quantifiers to formulas forced by the empty condition. Then we can check that each axiom of ZFC is forced by the empty condition. Finally, we can check that if $p$ is a condition, the theory (without variables, but allowing appropriate names) that it forces is consistent.
(I actually wrote all of this down as a grad student. It is not entirely without pain. One can simplify this brutal approach at times, by using, say, the reflection theorem and a bit of the semantic approach you know of with countable models.)
Another approach is the Boolean-valued models construction. This is due to Dana Scott and Robert Solovay, and it is very flexible and useful. It makes sense over any model. This approach produces a proper class (from the point of view of the original model) and rather than being a model in the usual sense, truth-values are understood as varying over a complete Boolean algebra (the completion of the poset, from the point of view of the model). One can see that there is a natural way of interpreting the ground model as a (classical) substructure of its Boolean-valued extensions, so we can safely argue as if we had an ideal generic extension of the universe. If there are appropriate ultrafilters in the Boolean algebra (say, in the true universe of sets), then we can form a (Boolean) ultrapower and recover an honest model from a Boolean valued extension.
Sometimes, we can actually show that generics over certain ground models exist, and build transitive models even if the original model was uncountable. For example: Assuming appropriate large cardinals, the powet set of many posets in $L$ is actually countable in $V$, so we can find forcing extensions of $L$ as submodels of $V$. A cute example is that if $0^\sharp$ exists and $\kappa=\omega_1$ (of $V$, this is much larger than the $\omega_1$ of $L$), then in $V$ there is an inner model which is a forcing extension of $L$ by the poset ${\rm Col}(\omega,<\kappa)$, so this is a forcing extension of $L$ that computes $\omega_1$ correctly. However, we cannot have (in $V$) an inner model that is a forcing extension of $L$ and computes both $\omega_1$ and $\omega_2$ correctly (this would force $0^\sharp$ to belong to $L$).
As another example, under determinacy, given any (transitive) model of choice, a large initial segment of it is very small, so we can find generics over these models. This is useful to prove results about the models of determinacy, by arguing about its inner models of choice. A similar approach is used in Solovay's model to show Lebesgue measurability of all sets of reals. Essentially, by finding appropriate codes for the sets in small models of choice, and arguing that the sets the codes represent are measurable in these small models, and then using the codes to check that measurability is preserved.
A good reference for this question, as Amit mentioned, is Kunen's book, chapter VII. I strongly recommend that you begin by looking at this book.
If you want to delve deeper: For the Boolean-valued approach, the best reference is John Bell, "Set Theory: Boolean-Valued Models and Independence Proofs" (Oxford Logic Guides), of which the third edition just appeared, in 2005. When Scott and Solovay developed forcing in terms of Boolean algebras, they promised a paper explaining their approach. The paper never quite materialized and somehow morphed into this book by Bell.
I know some books try to avoid the "transitive models" approach since they are only interested in consistency results. I remember James Cummings criticized this avoidance a few years ago in a review (published in the JSL). For example, the countable models approach allows us to prove, using forcing, that $\Sigma^1_1$ sets are Lebesgue measurable (provably in ZFC), by adapting appropriately the argument I sort of hand-waved above about Solovay's model.
(The countable models version of forcing has other advantages. For example, to construct Suslin trees with special properties in $L$, one can proceed by induction on the levels of constructibility, and at appropriate limit stages choose the branches of the partially formed tree to be generic over the stage built so far.)
Once one realizes that forcing is essentially an internal construction, it is clear we do not really need the models we work with to be transitive, or countable, or any such thing. However, it is nice to see how to make explicit sense of the construction in other cases. The clearest presentation of this I have seen is by Woodin. You may want to look at the Woodin-Dales book, "An Introduction to Independence for Analysts", Cambridge UP (1987), and its sequel, "Super-Real Fields: Totally Ordered Fields with Additional Structure" London Mathematical Society Monographs New Series, Oxford UP (1996).