Let $\ell^\infty(\mathbb{N})$ denote the set of bounded real sequences $(a_n)_{n\in\mathbb{N}}$. The $\lim$ operator is a partial linear operator from $\ell^\infty(\mathbb{N})$ to $\mathbb{R}$. With the Hahn-Banach theorem, $\lim$ can be extended to a generalized limit functional. The Hahn-Banach theorem uses the Axiom of Choice.
Are there models of $\mathsf{ZF}$ in which no generalized limit functionals exist?
Yes. In fact, if you work in $\mathsf{ZF}+\mathsf{DC}+$ "all sets of reals have the property of Baire" ($\mathsf{BP}$), say the Solovay or Shelah models, you can prove that $(\ell^\infty)^* = \ell^1$, so that the only continuous linear functionals on $\ell^\infty$ are those coming from $\ell^1$. The generalized limits are certainly not of this form, since they vanish on $c_0$ but not identically. Under these axioms, $\ell^1$ is reflexive.
You can find a proof in Schechter, Handbook of Analysis and its Foundations, sections 29.37–38.
Interestingly, under these axioms all linear functionals on any Banach space are continuous, so in fact the algebraic dual of $\ell^\infty$ also equals $\ell^1$. And the limit operator has no linear extension to $\ell^\infty$.
Digression: This is a fun example because there are several different ways to prove in $\mathsf{ZFC}$ that $(\ell^\infty)^* \ne \ell^1$. It is interesting to see how all of them fail in this model, and where they used choice. For instance:
Use Hahn-Banach as in your example. Hahn-Banach doesn't work without choice.
Use Alaoglu's theorem to produce a weak-* limit point of the usual basis $\{e_i\}$ of $\ell^1 \subset (\ell^\infty)^*$. This is another sort of generalized limit. So Alaoglu also must fail without choice; of course, the usual proof uses Tychonoff.
Recall the following exercise: "If $X^*$ is separable then so is $X$." Note that $\ell^1$ is separable and $\ell^\infty$ is not. But the "exercise" used Hahn-Banach, and isn't necessarily true without choice.
