Regular-language formations yield congruence formations

For every type $S$ of sorts equipped with a finiteness instance (with no assumption that $S$ is inhabited or nonempty), every implicit $S$-sorted signature $\Sigma$—that is, an arbitrary family of types $\Sigma_{w,s}$ of operation symbols indexed by finite lists $w$ of input sorts and an output sort $s$, with no finiteness assumption on the operation-symbol types—and every regular-language formation $\mathcal L$ for $\Sigma$, there exists a finite-index congruence formation $\mathcal F$ for $\Sigma$ such that, for every $S$-sorted family $X=(X_s)_{s\in S}$ of generator types, $\mathcal F_X$ is exactly the set of congruences $\Phi$ on the free $\Sigma$-algebra $T_\Sigma(X)$ satisfying both: the disjoint union $\coprod_{s\in S} T_\Sigma(X)_s/{\Phi_s}$ of their sortwise quotient carriers is finite, and every sorted language $K=(K_s\subseteq T_\Sigma(X)_s)_{s\in S}$ saturated by $\Phi$—meaning $\Phi_s(x,y)$ implies $x\in K_s\iff y\in K_s$ for every $s,x,y$—belongs to $\mathcal L_X$. Here a congruence is a sortwise family of equivalence relations preserved by every basic $\Sigma$-operation, and $T_\Sigma(X)$ consists sortwise of the well-sorted terms generated by variables from $X$ and applications of symbols from $\Sigma$. The assumption that $\mathcal L$ is a regular-language formation supplies, for every $X$, a set $\mathcal L_X$ of sorted languages on $T_\Sigma(X)$ such that: each selected language has finite-index syntactic congruence; every language saturated by the universal congruence is selected; whenever $L,K\in\mathcal L_X$, every language saturated by the intersection of the syntactic congruences of $L$ and $K$ is selected; and whenever $M\in\mathcal L_Y$ and $f:T_\Sigma(X)\to T_\Sigma(Y)$ is a homomorphism whose composite with the quotient by the syntactic congruence of $M$ is surjective at every sort, every language saturated by the pullback along $f$ of that syntactic congruence belongs to $\mathcal L_X$. The syntactic congruence used here relates $x,y$ at sort $s$ exactly when every congruence $\Psi$ that contains every congruence saturating the language also relates $x,y$. The asserted witness $\mathcal F$ must itself assign to each $X$ a nonempty set $\mathcal F_X$ of congruences, be closed under pairwise intersection and upward enlargement, be closed under pullback along every homomorphism that is sortwise surjective after quotienting by the target congruence, and contain only finite-index congruences; the displayed equality asserts membership equivalence in both directions for every $X$ and every congruence, but asserts neither uniqueness of $\mathcal F$ nor any finiteness or nonemptiness of $X$ or its fibers. Thus empty $S$, empty or infinite generator fibers, signatures with empty or infinite symbol types, and free-algebra sorts with no terms are included; sortwise saturation and compatibility conditions over empty carriers are vacuous, and any pullback-closure implication whose quotient-surjectivity premise is impossible is vacuous as well.