It's easy to come up with examples of spaces which are provably-in-ZFC not first countable: e.g. the order topology on $\omega_1+1$, or the cocountable topology on any uncountable set. However, these proofs tend to rely on principles of the form "every 'small' union of 'small' sets is 'small'," and these can fail quite badly without choice.
Conversely, at the other end of things, if we extend ZF by a strong anti-choice principle, we can often get provably non-first-countable spaces. For example, the cofinite topology on an amorphous set $A$ is non-first-countable.
Why? Pick $a\in A$, and consider a sequence $(U_i)_{i\in\mathbb{N}}$ of neighborhoods of $a$. The union of the complements of the $U_i$s must not be finite in order for the sequence to witness first countability. Let $V_i$ be the set of points "thrown out for the first time" at stage $i$: that is, $V_i$ is the set of $y$ such that $y\not\in U_i$ but $y\in \bigcup_{j<i} U_j$. Infinitely many of the $V_i$s must be nonempty; WLOG suppose each $V_i$ is nonempty. But then $\bigcup_{i\in\mathbb{N}}V_{2i}$ and $\bigcup_{i\in\mathbb{N}}V_{2i+1}$ are two disjoint infinite subsets of $A$.
So my question is whether we can find non-first-countable spaces in ZF alone. Phrased most simply, this is:
Does ZF prove that there are non-first-countable spaces?
We can also ask a question which might be a bit more satisfying:
Is there a formula $\varphi$ which ZF proves defines a non-first-countable topological space?
I suspect that the answer to even the first question is "no," and that this is witnessed in something like Gitik's model; but I'm not sure.