Is there a contradiction hiding in this alternative set theory with 3 axioms?

Let us take as a vocabulary the $\in$ relation (is an element of), and a single unary predicate $C$, where $Cx$ is read "$x$ is constructible" or "$x$ is a constructible set" (I'm making this up, but the term seems appropriate). We may then write down an alterative set theory with three intuitive axioms (one of them an axiom schema):

1. Extensionality: $$\forall X \,\forall X'\;:\; (\forall x\,:\, x \in X \longleftrightarrow x \in X') \to X = X'.$$

   (I.e.: Objects with the same elements are equal.)

2. Schema of construction: For any formula $\varphi$ which does not contain C, if $\varphi$ has free variables $x$ and $\overline{y} = (y_1, y_2, \ldots, y_k)$, IF $$ \forall \overline{y} \, \forall x \;:\; (Cy_1 \land \cdots \land Cy_k \land \varphi(x,\overline{y})) \to Cx $$ THEN $$ \forall \overline{y} \, \exists X \, \forall x \,:\, x \in X \longleftrightarrow \varphi(x,\overline{y}). $$ In other words, if it is possible to deduce that $x$ is constructible from only the fact that $y_i$ are constructible and $\varphi(x,\overline{y})$, then the set $X = \{x \mid \varphi(x,\overline{y})\}$ exists.

3. Constructible sets are those with constructible elements:

   $$\forall X \; : \; CX \longleftrightarrow (\forall x \;:\; x \in X \to Cx).$$

It seems to me I can deduce many of the axioms of ZF from these: at least, pairing, union, power set, and specification.* So I am thinking there must be a contradiction lurking somewhere. The question:

(i) Is there an (obvious) contradiction in these three axoims?

For instance, we could try to encode Russell's paradox. It can't translate directly, since if we just assume "$x \in x$", it doesn't follow that $Cx$. And one cannot play tricks with "the set of all constructible sets that don't contain themselves" because $C$ is not allowed in $\varphi$ in the comprehension schema.

However, there does seem to be something fishy going on: in ZFC, well-founded induction is a theorem, and well-founded induction cannot be true here or else we could prove that all sets are constructible (using axiom 3). At that point, (2) reduces to unrestricted comprehension and the theory becomes inconsistent.

I would also like to know:

(ii) Is this theory similar to any existing alternative set theories?

When I wrote down these axioms this afternoon, I was trying to formalize the intuitive justification for the axioms of ZFC, namely, that every axiom constructs bigger sets out of smaller sets which have already been defined.

*For pairing, if $A$ and $B$ are constructible, and $x = A$ or $x = B$ then $x$ is constructible. The other axioms I mentioned (union, power set, and specification) use axiom (3): For union, if $A$ is constructible and $x \in a$, $a \in A$, $x$ is constructible. For power set, if $A$ is constructible and $B \subseteq A$, then every $x \in B$ is constructible so $B$ is constructible. For specification, if $x \in A$ and$ \varphi(x)$, and $A$ is constructible, then in particular $x \in A$ so $x$ is constructible.

Your theory bears large similarity to Ackermann's. Notice that Ackermann's originally used a one place predicate symbol $M$ standing for "is a set", later on the constant symbol $V$ became to be used instead (which is in some sense a relatively stronger approach as far as fragments of Ackermann's is concerned). You can think of your predicate $C$ as the predicate $M$ of original Ackermann's. Definitely your theory proves the following axioms of Ackermann's set theory: Extensionality, both Completeness axioms for $V$, and all instances of set construction (reflection scheme); but it adds to it, the principle that every subclass of $V$ is a set (your third axiom) but on the other hand not having class comprehension, your theory cannot prove existence of $V$ [which would correspond to the class of all $C$ sets] and because of that I'd conjecture (not really sure) that it cannot prove infinity. Actually there is a similar question that I've posed about Ackermann, where I've posed the challenging axiom of every proper subclass of $V$ being a set (i.e. an element of $V$) and I added it to Ackemrann - foundation - class comprehension. I don't think anyone came with an inconsistency with it, and there it proved even infinity, and it might even be as strong as the original Ackermann's system. I think your theory here is more benign since it doesn't even construct a universal class. I think it is consistent and it is equivalent to Ackermann - foundation- class comprehension with having its primitive being the original primitive of Ackermann which is the one place predicate symbol $M$. And I think it might be equivalent to $PA$. You need to refer to fragments of Ackermann's set theory!

Note: actually I've also asked almost exactly the same as your question, but with the slight addition of infinity, and freedom on parameters (on the antecedent as well as on the consequent of set construction) See here