$\sf ZF$ — Sets that can be proven to exist
I don't know if there's a name for that model, but there's a name of a famous "dilemma" in set theory. Formally it is not a dilemma, because it has a very reasonable, and formal, solution.
The Skolem paradox says exactly that there exists a countable model of set theory. You only need something called (downward) Löwenheim-Skolem theorem; this theorem states that if $\mathcal{L}$ is a first-order language with cardinality $\mu$, and $\mathcal{T}$ is an $\mathcal{L}$-theory with an infinite model $\mathcal{M}$, then there is a countable elementary submodel $\mathcal{A}$ of $\mathcal{M}$ of size at most $\mu$ (if you're not familiar with this terminology you can understand it as "exists a smaller universe where happens everything that happen in the larger one"). It is trivial that the language $\mathcal{L}_\in$ of set theory has cardinality $\aleph_0$, and $\mathbf{ZFC}$ (we do not know if this theory is consistent, but we can give it the benefit of the doubt, that is we can assume that in fact it is consistent) has infinite models (such as $V_\kappa$ with $\kappa$ inaccessible).
With that we have a countable model $\mathcal{M}$ of set theory in which $\omega_1$ exists, that sounds like a paradox but in fact it isn't. When you say that $\omega_1$ (in fact $\omega_2,\omega_3,\dots$) lives in this countable universe $\mathcal{M}$ (and yes $\mathcal{P}(\mathbb{N})$ lives here too) you're only saying that there's someone that plays the role of $\omega_1$; you aren't saying that this $\omega_1$, lets call it $\omega_1^\mathcal{M}$, is the "real" first uncountable ordinal, like the one that responds to our mathematical intuition (it can not be). You are just saying that $\mathcal{M}$ does not have enough material to build the real one, so it has build a cheaper one. In fact you could think of $\omega_1^\mathcal{M}$ as $\omega_1\cap\mathcal{M}$ (this isn't quite right but responds to an intuitive argument).
Hope this responds to your question!
There are some inherent problems with this question, which stem from a naive approach to this issue.
First of all, formulas and proofs live in the meta-theory, whereas sets live in the universe of the theory.
Let me interpret your question, in the most naive way, then, "proof of existence" is a parameter-free formula $\varphi(u)$ such that $\sf ZF$ proves that there exists a set $x$ which is exactly the class defined by $\varphi$.
[I am taking parameter free formulas here, since once you start with parameters you can just write $\varphi(u,x)$ to be $u\in x$, and then every set provably exists with itself as the parameter. You can start talking about predicative formulas and stuff like this, but now you complicate everything because you need to start keeping track of your formulas and parameters, and that makes everything harder.]
Now, let's move on to existence. You want to "carve" these sets out of some model, I presume. So in principle, it seems, you have the set theoretic universe, and you ask what is the collection of sets which satisfy this "provable existence". Of course, this collection itself is not first-order definable, but let's not worry about this for now.
Suppose that our universe is one where every set is definable without parameters (this is consistent, and of course, implies—in the meta-theory—that the model is countable), then for every $\varphi(u)$ you can now write $\varphi'(u)$ to be "$\varphi(u)$ if it defines a set, or the empty set otherwise". Then every set in the universe provably exist, and you get the whole model.
But suppose that you are in a different universe. Say working over an uncountable model, or something else where not even every countable ordinal is definable, then $\omega_1$, while provably exists, will appear after a significant gap when you exhaust the provably-existing-countable ordinals.
Here is an observation. If $\alpha$ is an ordinal which provably exist, then $V_\alpha$ and $\omega_\alpha$ provably exist, and in fact, for every $x$ which provably exists, $\mathcal P^\alpha(x)$ also provably exists. But you quickly run into problems here, either all sets provably exist, or you start having "holes" in your universe fairly fast. And you lose transitivity, making this collection odd. Sure, we can collapse this class to a transitive class (relative to the universe, of course). But there is absolutely no guarantee now that this is a model of $\sf ZF$.
In the comments, it seems that you want to think about this as somehow built inductively, step by step, by taking at each point the subsets "which provably exist". Perhaps similar to the construction of $L$ by taking the definable subsets. But here is the issue. When we construct $L$, we use the internal notion of "definable". This notion is at least somewhat robust, since given a structure, you can talk about the definable subsets there.
Suppose that we wanted to try and use "provably existing" instead of "definable". You run into two major problems:
Different structures have different theories. In the construction of $L$ we go through several different theories at different steps. There are $L_\alpha$'s which satisfy the power set axiom, and others which do not. There are some which satisfy "every set is countable" and others which satisfy $\sf ZFC$. If you want to talk about provability, you need to fix your theory, but the collection of sets that provably exist—and especially if you think about this as an inductive construction—need not satisfy your theory again.
Different universes might disagree with their meta-theory about proofs and definitions. Since your universe and its meta-theory might disagree on the integers, they might also disagree on whether or not $\sf ZF$ is even consistent, or plenty of other things of that fashion which might complete skew the internal notion of provability and give you unwanted results. This might be overcome if you assume more, e.g. that you work inside a transitive model, or something like that, but this just shows that these assumptions are not "clean".
Alas, not all is bad. In a very recent post on arXiv, Merlin Carl and Philipp Schlicht define the notion of a canonical sentence, which is a sentence which provably describes some unique inner model (e.g. $V=L$). This notion is much more technical and I think to some extent tries to capture the notion of "canonically existing models", which is what I think you're trying to get with "all provably existing sets". But of course, this is more complicated than just that.
Merlin Carl and Philipp Schlicht, Canonical Truth. Posted on Dec. 7th, 2017, arXiv:1712.02566.