I see adjointness between the two concepts of "being a definable set" and "being a set-builder formula":
A set $X$ is definable when there is a formula $\phi(x)$ such that $X = \lbrace x : \phi(x)\rbrace$.
A formula $\phi(x)$ is a set-builder when there is a set $X$ such that $X = \lbrace x : \phi(x)\rbrace$.
In which (category theoretical) contexts this adjointness is made explicit and valuable?
Given any pair of sets $X, Y$ (let me not be too specific about what "sets" means because what follows is robust with respect to changes in the definition), any relation $R : X \times Y \to 2$ whatsoever induces a contravariant adjunction between the poset of subsets of $X$ and the poset of subsets of $Y$ given by
$$2^X \ni S \mapsto F(S) = \{ y \in Y : xRy \forall x \in S \} \in 2^Y$$
$$2^Y \ni T \mapsto G(T) = \{ x \in X : xRy \forall y \in T \} \in 2^X.$$
A contravariant adjunction between posets is also known as an antitone Galois connection. Any such thing determines two closure operators, one on $2^X$ and one on $2^Y$, and it is often interesting to determine the corresponding closed subsets. Examples:
Let $L/K$ be a Galois extension, let $X = L$, and let $Y = \text{Gal}(L/K)$. The relation is "the element $y \in Y$ fixes the element $x \in X$." The adjunction sends a subset of $L$ to the subgroup of the Galois group fixing it and sends a subset of the Galois group to its fixed field. The fundamental theorem of Galois theory tells us that the closed subsets are the subgroups of the Galois group on the one hand and the subextensions of the Galois extension on the other.
Let $X = k[x_1, ..., x_n]$ be a polynomial ring over an algebraically closed field and let $Y = \mathbb{A}^n$ be the corresponding affine $n$-space. The relation is "the polynomial $x \in X$ vanishes on the point $y \in Y$." The adjunction sends a set of polynomials to the variety it cuts out and sends a set of points to the ideal of functions vanishing on it. The Nullstellensatz tells us that the closed subsets are the radical ideals on the one hand and the Zariski-closed subsets on the other (the second statement is tautologous; this is the definition of being Zariski closed. But the first one has content).
Let $X$ be the set of models of a first-order theory $T$ and let $Y$ be the set of possible sentences that could be added to $T$. The relation is "the sentence $y \in Y$ is true in the model $x \in X$." The adjunction sends a set of models to the set of sentences true in every model and sends a set of sentences to the set of models of those sentences (together with $T$). The completeness theorem tells us that the closed subsets are the deductively closed sets of sentences on one hand and whatever their sets of models are on the other.
In your example one of the "sets" is the set of all sets, the other is the set of all formulas, and the relation is "the set $x \in X$ satisfies the formula $y \in Y$." It is a version of the slogan "syntax is adjoint to semantics," an observation first made, as far as I know, by Lawvere.
Your question is not as precise as you portray it, and apart from the question of adjointness, a naive treatment of definability like this leads easily to contradictions. Specifically, I claim that your definitions do not actually succeed in defining the concepts of definability and of being a set-builder.
To convince you of this, let me prove that the property of a set-theoretic formula $\varphi$ being a set-builder is not expressible in the language of set theory.
Specifically, let me prove that no expressible property $P(\varphi)$ aligns with your concept of being a set-builder. Consider any property $P(\varphi)$ of formulas that is expressible in the language of set theory. By the Gödel fixed point lemma, there is a sentence $\sigma$ such that we can prove the equivalence $\sigma\iff P(\sigma)$; and we can prove this equivalence in a very weak system. Note that since $\sigma$ has no free variables, it follows that $\{ x \mid \sigma\}$ is either the empty set or everything, depending on whether $\sigma$ is false or true, respectively. In particular, $\sigma$ is a set builder in your sense just in case $\sigma$ is false. The point now is that this is equivalent to saying that $P(\sigma)$ is false. Thus, this particular formula $\sigma$ is a set-builder if and only if $P(\sigma)$ fails, and so $P$ gets the wrong answer in this instance. Since $P$ was arbitrary, there simply is no way to express the property of a formula that it is a set-builder.
(One could alternatively argue like this: suppose that we could express the property of being a set-builder. By the fixed-point lemma, there is a sentence $\sigma$ that is equivalent to "$\sigma$ is a set-builder". And so $\{x \mid \sigma\}$ is a set if and only if it isn't.)
Moving to a richer theory or to category theory does not solve the fundamental problem, since the Gödel fixed point lemma applies to any sufficiently rich system, including GBC, KM or ETCS. In these systems, there simply is no way to express the concept of being a set-builder in that system.
In particular, you haven't actually defined what it means for a formula to be a set-builder. And similar issues arise with the concept of being a definable set.
The basic obstacle here, of course, is Tarski's theorem on the non-definability of truth, which can be thought of as the claim that we have no definable way to express when a particular sentence is true. Both of your definitions in effect appeal to such a predicate, since you are defining a property of $\varphi$, but then making assertions about the truth of instances of $\varphi$. Although we may speak of specific formulas being set-builders or not, there simply is no general concept of a formula being a set-builder that is expressible in the same language.
Lastly, and perhaps this will be good enough for you, one can address part of the problem by working in a stronger system, but being satisfied with notions of definability and set-builders only for formulas in a weaker system. For example, in Kelley-Morse set theory KM, we can define a truth predicate for first-order truth in the language of set theory. In this case, working in KM we have robust concepts of definability and set-builders, but only for formulas in the first-order language of set theory, and not for formulas in the language of KM.
Another way to address the issues is to work with the notions of definability and set-builders over a specific set model. If $M$ is a set model of some theory, then we have notions of definable-in-$M$ and of a formula $\varphi$ being a set-builder-in-$M$. This model-theoretic treatment of definability is used throughout logic. But when using it, one has in effect an outside-the-universe account of the topic, since the notions are not expressible inside the model $M$ being considered. The truly problematic issues arise only when one wants to refer to definability in the whole universe.
These definability issues arose before on MathOverflow, in my answers to Anixx's question Is analysis in fact the analysis of definable numbers? and to Scott Aaronson's question Succinctly naming big numbers. In those answers, I show some examples showing that there are models of set theory with a range of paradoxical behavior with respect to definability. Most of those examples appear also in my paper, J. D. Hamkins, D. Linetsky, J. Reitz, Pointwise definable models of set theory, JSL 78(1):2013, which includes a relatively accessible account of some of these metamathematical issues with definability.
This is really just an answer stub but it's worth mentioning anyway...
In some way, this is one of the many facets and extensions of Stone Duality. Henrik Forssell's 2008 thesis is one of the latest attempts that I am aware of to formalize this general idea to the fullest.
