Apologies for the extreme length of this answer, but addressing your question requires a bit of a build-up.
First, I'll briefly discuss why the brute-force proofs of cyclicity for $\mathbb{Z}/p\mathbb{Z}^\times$ are fully constructive in the technical sense.
Nonetheless, the underlying motivation of your question is sound and interesting: one can and should distinguish "brute-force" proofs from non-brute-force ones. Fortunately, we don't need any new formalism to study the distinction: I'll explain how constructive mathematics and its proof theory already has everything we need.
In the end, the distinction between brute-force and non-brute-force boils down to whether the same proof would work under weakened finiteness assumptions. This will be the answer to your object-level question ("what formalism can we use to give meaning...")
I'll end by refining the question of cyclicity of $\mathbb{Z}/p\mathbb{Z}^\times$ itself into a subtler one about the constructive theory of fields that should match your original intent fairly closely (i.e. understanding the answer would tell us a lot about the possible proofs of cyclicity of the group).
I. Direct constructive proof
Do we have direct constructive proofs of cyclicity for $\mathbb{Z}/p\mathbb{Z}^\times$? Well, one can e.g. show directly that any element of maximal order in $\mathbb{Z}/p\mathbb{Z}^\times$ indeed generates the whole group. This yields a quite impractical algorithm, that calculates the orders of all elements, then returns the one with the biggest order. But it absolutely does not require us to first show that the group is cyclic and then find a generator: it's just one proof showing that a maximal order element is in fact a generator, and a direct one at that.
So in the straightforward technical sense, we have a direct and constructive proof of cyclicity for $\mathbb{Z}/p\mathbb{Z}$ that one can carry out in any of the usual constructive foundations of mathematics.
Of course, the mere fact that such proofs are direct and constructive does not mean that they are not awkward or "problematic" in some other, less technical sense.
These proofs are constructive, even though they make use of an exhaustive search which would have questionable constructive validity over an infinite set; it is precisely the
finiteness of $\mathbb{Z}/p\mathbb{Z}$, and our ability to decide equality on its elements, that enable the use of exhaustive or brute-force search in this context, without losing constructivity. So if we want to study proofs which do not make use of such search, it is these finiteness and discreteness assumptions that we'll have to weaken, and the key thing to study becomes the plethora of notions of finiteness and discreteness available in constructive mathematics.
II. Finiteness notions
In the strong, classical foundational system that most mathematicians work in (Zermelo-Fraenkel Set Theory with the Axiom of Choice), one can define and use the notion of finite set in many different ways. For example, one could call a set $S$ finite if:
- one can find a bijection between $S$ and the set $\{0,\dots,n\}$ for some $n \in \mathbb{N}$;
- every injection $\iota : S \rightarrow S$ is a bijection;
- the functor $\mathrm{Hom}(S,-)$ preserves filtered colimits;
- all ultrafilters on $S$ are principal;
- $S$ can be written as a union of $I$-indexed set of sets $A_i$, so that each $A_i$ is finite in the sense of Notion 1, and the image of $A_i$ is itself finite in the sense of Notion 1; etc.
Within ZFC, one can prove all of these notions equivalent. However, in other foundational systems, these concepts of finiteness begin to diverge. For example, if we pass from ZFC to ZF, we can get Dedekind-finite infinite sets, special sets that are not finite in the sense of Notion 1, but finite in the sense of Notion 2. By itself, this phenomenon need not have anything to do with constructivity: it happens even though both ZFC and ZF have the full Law of Excluded Middle. (Exercise: explain what happens to Notion 4 in the foundational system ZF extended with the axiom stating that all ultrafilters are principal)
In constructive mathematics, the phenomenon is even more pronounced, however: the classical monolith of finiteness crumbles into dust, revealing a multitude of inequivalent variations with complicated relationships between them.
Often, even constructivists find this phenomenon annoying. It makes things more verbose for us when we state results about finite structures, sometimes prevents the formally most convenient versions of classical proofs from working in our foundations, and sometimes prompts endless chains of clarifications when we answer Math.SE questions about constructive mathematics.
However, when evaluating the robustness of proofs concerning finite structures, the large variety of finiteness notions turns from a nuisance into a useful measuring stick. Generally, the more powerful your proof, the more modest the notion of finiteness required to make it work.
A related phenomenon that comes into play in the constructive setting is discreteness. Given a general set $S$, you usually cannot prove $\forall x, y \in S. x = y \vee \neg (x = y)$, an instance of LEM. However, one can prove this when $x,y$ range over certain special sets such as $\mathbb{N}$, often called discrete sets (or sets with decidable equality). Again, one can use this as a measuring stick: sets whose discreteness would imply strong intuitionistic taboos (such as the limited principle of omniscience) are really quite amorphous, so proofs/algorithms that work even on such sets have to be clever, and cannot do things one would consider brute-force.
III. Underdetermined structures
So, how does one study the content of different proofs under these lens?
Let's start by looking at a situation that's a bit simpler in the classical case. Consider a field $F$ that is finite in the sense of Notion 1 above. Can we write every polynomial over $F$ as a product of irreducible polynomials? Of course, this has a perfectly constructive brute-force proof where you do trial division by each of the finitely many polynomials of lower degree, until you end up with an irreducible factorization.
This is exactly the sort of brute-force proof that you want to rule out. How could we do that? Well, since the proof hinges on the fact that for finite $F$, we can enumerate the polynomials of lower degree, perhaps we should try to arrange a situation where the potential proofs don't have the ability to do that!
Fortunately, one can define some very "underdetermined" algebraic structures in constructive mathematics! For example, one can fix a prime number $p \equiv 3 \mod 4$, then pick an arbitrary infinite sequence $y: \mathbb{N} \rightarrow \{1,i\}$, and consider the field $F = \bigcup_{n \in \mathbb{N}} \mathbb{Z}/p\mathbb{Z}(y_n)$.
Even though this object $F$ is a discrete field, it feels a bit underdetermined, in the sense that one cannot really tell whether $F$ is $\mathbb{Z}/p\mathbb{Z}$ or $\mathbb{Z}/p\mathbb{Z}(i)$, unless one can somehow divine whether the infinite sequence $y$ ever takes the value $i$ or not. But the ability to do that would immediately imply the limited principle of omniscience, an intuitionistic taboo.
Consequently, one cannot prove constructively that $x^2 + 1$ factors as a product of irreducibles over such fields $F$ by enumerating the polynomials of lower degree. Indeed, if one could prove constructively that $x^2 + 1$ factors into irreducibles over $F$, by BHK one would get an algorithm that performs the factorization. Looking at the resulting factorization, one could determine whether the sequence $y$ takes on the value $i$ or not, proving the limited principle of omniscience. So this is not possible.
Where does the brute-force argument that would work perfectly well for $\mathbb{Z}/p\mathbb{Z}$ $\mathbb{Z}/p\mathbb{Z}(i)$ break down? It breaks down because we cannot exhibit a bijection between the underlying set of $F$ and the set $\{0,\dots,n\}$ for any particular $n \in \mathbb{N}$. Classically, $F$ would be finite, but constructively, finiteness broke apart into many nonequivalent notions, and the field $F$ is not finite in the strong sense of Notion 1 that our original proof required, only in the constructively much weaker and more exotic sense of Notion 5.
We successfully reduced the question of existence of a non-brute-force proof to the existence of a constructive proof with a weaker assumption (Notion 5 instead of Notion 1). We did not need to give a formal, proof-theoretic definition of "brute-force" either.
IV. Refining your question
Let $\mathbb{N}_P$ denote the set of prime natural numbers. One can start with an arbitrary sequence $x : \mathbb{N} \rightarrow \{0\} \cup \mathbb{N}_P$ satisfying $\forall n,m. x_n > 0 \wedge x_m > 0 \rightarrow n = m$, then define the ideal $X$ of $\mathbb{Z}$ generated by all elements of the sequence $x$, and consider the field of quotients of the ring $\mathbb{Z}/X$. Generally, it is impossible to determine the characteristic of the resulting field $F$, as the ability to do so would imply the limited principle of omniscience again.
But if you give me an $n$-element multiplicative subgroup $G$ of $F^{\neq 0}$, I can still prove the existence of a single element $g \in G$ so that $\langle g \rangle = G$. Somewhat surprisingly, even though $F$ itself is very ambiguous, as long as only $G$ is finite in the sense of Notion 1, this remains still possible.
So a good way to refine/formulate your initial question about "direct constructive proof of cyclicity" amounts to asking whether one can strengthen this result much further. If we replace $F$ with a field that is not discrete, or replace $G$ with a group that's not strictly an $n$-element group but satisfies only a weaker finiteness notion such as Notion 5, does the theorem still admit a constructive proof? Or rather, for which notions of discreteness/finiteness does this theorem admit a constructive proof?
