I want to construct a model $M[f] \models ZF$ containing a function $f$ that is discontinuous but sequentially continuous at a point. I would like to ask if the following proof sketch works? I would also like to ask if there are other constructions of such models?
Let $M \models ZF$ be a countable transitive model.
Let $\alpha = o(M) = Ord \cap M \in \omega_1$, the ordinals in $M$.
In the background theory, we construct a sequence $r = \langle r_i : i \in \omega\rangle$ of rational numbers with
$$\lim_{i \to \infty} r_i = 1$$ and
$$Ordertype (( r, <_{\mathbb{Q}}))= \alpha.$$
Lemma Construction of such a sequence.
(By induction on $\alpha$.)
Now we define the function $f:\mathbb{R}\to \mathbb{R}$ as follows.
$$ f(x) = \left\{ \begin{array}{ll} 2 & \mbox{if } x = r_n \text{ for some } n,\\ 1 & \mbox{otherwise.} \end{array} \right. $$
Clearly, $f$ is both discontinuous and sequentially discontinuous at $x=1$. However, we will now construct the model $M[f] \models ZF$ in which $f$ is discontinuous but sequentially continuous at $1$.
For our notion of forcing $(\mathbb{P}, \leq_{\mathbb{P}}, 1_{\mathbb{P}})$, we set
$$\mathbb{P} = F(f)= \{p: \text{ finite }p \subset f\}, $$
$$p \leq_{\mathbb{P}} q \leftrightarrow p \subseteq q,$$
$$1_{\mathbb{P}}= \emptyset.$$
By forcing over $\mathbb{P}$, we get the model $M[f] \models ZF$ which contains $f$ as an element (for details see Kunen, Set Theory, 2011, Ch. IV). First we show
$$M[f] \models f \text{ is discontinuous at }1.$$
By definition, $f$ is discontinuous at $1$ just in case there exists an $\epsilon$ (here $\epsilon = 0.5$ does the job) such that
$$\forall \delta. \exists x. |1-x| < \delta \text{ and } |f(1)-f(x)| > \epsilon.$$
$M[f]$ satisfies this, since it contains all the $r_i$'s (the points of discontinuity of $f$), which have a point of accumulation at $1$. However, while $M[f]$ contains all these points individually, it does not contain the set of all these points collectively, nor any of its $<_{\mathbb{Q}}$-cofinal subsets.
To see this, suppose
$$\langle s_j : j < \omega \rangle \subseteq \langle r_i : i < \omega \rangle,$$
$$\lim_{j \to \infty} s_j = 1,$$
$$\langle s_j : j < \omega \rangle \in M[f].$$
Let $\xi_j = Ordertype((r, <_{\mathbb{Q}})\upharpoonright s_j)$. For each $j$, the ordinal $\xi_j \in M[f]$. Using the Axiom of Replacement, from $\langle s_j : j < \omega \rangle \in M[f]$ we can infer that $\langle \xi_j : j < \omega \rangle \in M[f]$. But this is clearly a contradiction, since a denumerable sequence cofinal in the ordinals of $M[f]$ cannot be contained in $M[f]$.
Therefore, $M[f]$ cannot contain any subsequence of $r$ that tends to $1$. In other words, $M[f]$ satsifies
$$ \forall \langle x_i : i < \omega \rangle. \lim_{i \to \infty} x_i = 1 \Rightarrow \lim_{i \to \infty} f(x_i) = f(1),$$
i.e., $f$ is sequentially continuous at $x = 1$.
Well, if your sequence of rational numbers is in $M$, then $f$ is in $M$, since it was pretty straightforward to define from the sequence. If $f$ is not in $M$, then your forcing is not going to be in $M$ either, in which case, in what sense do we use it to force over $M$? Moreover, adding this sequence to $M$ will witness that $\alpha$ is countable, so you must have added ordinals, if you were to have a model of $\sf ZF$, which you cannot do with forcing, and quite possible, you might not be able to do it at all.
The idea, instead, is to consider Cohen's first model. This model is obtained by starting with a model of $\sf ZFC$, adding an $\omega$-sequence of Cohen reals, and then using permutations to "forget" the sequence, and only remember the set of these Cohen reals. The result is that this set is Dedekind-finite, so it does not contain any nontrivial sequences.
Call this set $A$, and now pick some $a\in A$ and consider the function, defined on $A$, which is $1$ everywhere, except $a$, and $0$ otherwise. Since all convergent sequences in $A$ are eventually constant, this is trivially sequentially continuous; and it is not hard to show that $A$ must be dense, and therefore the function is not continuous at $a$.