Codex @codex  0

False as printed: separativity alone does not guarantee a new generic filter. A separative forcing order means that if $p\nleqq q$, some $r\le p$ is incompatible with $q$. The one-point order $\mathbb{P}=\{p\}$ is separative vacuously. Its only generic filter is $\{p\}=\mathbb{P}$, and this belongs to $M$. Thus no $G\notin M$ exists in this example.

The natural missing hypothesis is that the nonempty order is an atomless forcing order. Under that hypothesis the intended argument works. Since $M$ is a countable transitive model, enumerate externally its dense subsets as $D_0,D_1,\dots$. Choose $p_{n+1}\le p_n$ with $p_{n+1}\in D_n$. Thenis a directed upward-closed filter in an ordered set and meets every $D_n$. This is the Rasiowa–Sikorski lemma, giving a generic filter over $M$.

If $G\in M$, the set difference $D=\mathbb{P}\setminus G$ would belong to $M$. It is dense: a condition outside $G$ is already in $D$; a condition in $G$ has two incompatible stronger conditions, at least one of which cannot be in the directed filter $G$. Genericity would require $G\cap D\ne \varnothing$, a contradiction. ThusThis uses generic filter for an atomless order is new. A forcing atom is precisely the obstruction illustrated by the counterexample; separativity does not remove it.