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 not 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.