What set of formal rules can we use to safely apply Universal/Existential Generalizations and Specifications? This question is mainly about formality, not intuition.
There are some questions here (and a lot of answers) about Universal Generalization. Each of these states some rules that can be used to avoid fallacies in a First Order Logic argument.
1: This post says:

Assume $\Gamma$ is a set of formulas, $\varphi$ a formula, and $\Gamma \vdash \varphi(y)$ has been derived.  The generalization rule states that $\Gamma \vdash \forall x \varphi(x)$ can be derived if $y$ is not mentioned in $\Gamma$ and $x$ does not occur in $\varphi$.

2: This other one says:

The following restrictions apply:

*

*The term $t$ cannot occur in any undischarged assumption of the derivation of $\phi[t/x]$

*The term $t$ cannot occur in $\phi$

3: An answer on the same question says:


*

*$t=0$ --- assumption : is $\phi[t/x]$


*$\forall x \ (x =0)$ --- from 1) by $\forall$I : wrong : $t$ is free in the one-line derivation of $\phi[t/x]$ , i.e. in $t=0$

4: One answer on this question says:

So, typically formalizations of the rule will say that $a$ needs to be a 'fresh' or 'new' constant: a constant that is not used elsewhere for a different purpose.
[...]
For Existential Elimination something similar happens. [...] In other words, once again you have to introduce a new constant.

From that, we can extract some rules that can be used (some of them are repeated, like "there can't be $x$ on the premise" and "there can't be $x$ anywhere before", in that case, we'll use the stronger version). For any substitution $P(a)$ to $\forall x[P(x)]$ (Universal Generalization) or $\exists y[P(y)]$ to $P(b)$ (Existential Instantiation):

*

*$a$ can't have appeared in any undischarged assumptions/premises.

*$a$ can't occur in $P$ after the substitution.

*$x$ has to be a new variable.

*$b$ has to be a new variable.

From this answer, it is clear that they are not meant to be used together:

Different systems define these rules a bit differently in terms of notation. For example, some systems simply drop quantifiers for the elimination rules, leaving what seems to be free variables in the formula, while others replace those variables with constant symbols. Either way, however, restrictions do indeed need to be in place that prevent you from making invalid inferences, as you already suspected.

A smaller combination of these seems to be usually regarded as enough, but for the sake of argument, let's use them all of them together. Now consider the following:
$$ \begin{align}\exists x[P(x)] & \quad \text{Premise} \\ P(a) & \quad \text{Existential Instantiation} \\ \forall y[P(y)] & \quad \text{Universal Generalization} \end{align} $$
It is clear that the above argument is a fallacy. If it works for one example, it doesn't mean it works for all of them. Still, all the rules were followed:

*

*$a$ doesn't appear in the premise

*$a$ doesn't occur after the substitution

*$y$ is a new variable

*$a$ is a new variable

Now of course, we can also add a new rule that states "If $a$ came from a Existential Instatiation, then it cannot be used in a Universal Generalization", but given that even following those 4 (quite strict) rules still resulted in a fallacy, what guarantees that there isn't some subtle example in which, even following those 5 rules, we'll still end up with a fallacy?
Almost all of these answers cite that "$a$ has to be arbitrary and not specific", or "we can't have previously assumed anything about $a$", but those are very informal and imprecise ways of stating how Universal Generalization can be safely used.
So, given that, my question is: What set of rules can one use, for which it is guaranteed that, given a statement $P(x)$, you can safely conclude that $\forall x[P(x)]$?
Edit: Though this question has been marked as a duplicate of Restrictions on the use of universal generalization, that question is asking how to understand these rules, and why they exist (also the case for this linked question), which is not the point of my question. It is clear to me how to use them (or so I hope, if I did not apply one of the rules properly, I'd be more than glad to be corrected). Also, it is clear why they exist, it's to avoid fallacies like the one presented above (namely, $ \exists x[P(x)] \Rightarrow P(a) \Rightarrow \forall y[P(y)]$). Now, even though that is their purpose, they don't seem to be strong enough to always avoid a fallacy. Even on an argument in which all of them are followed, it still leads to a conclusion that clearly shouldn't follow from the premise. So my question remains: Since these don't seem to be enough, which set of rules can be used to always avoid a fallacious use of UG?
Edit: Changed question from only Universal Generalization to Universal/Existential Generalizations and Specifications, to reflect evolving answers regarding the other quantifier rules.
 A: Some preliminary comments.
First: the formal expressions of the rules and their provisos may slightly differ according to the proof system: Natural Deduction, Hilbert-style, etc. Thus, it is a good practice to refer to a consistent set of rules.
Second: every proof system must be sound, i.e. it must allow us to derive only true conclusion from true premises.
Thus, for example, every proof system must avoid the following fallacy:

"Plato is a Philosopher; therefore everything is a Philosopher".

The usual proviso regarding Universal Generalization is exactly designed to avoid it.
This proviso is present also in the Natural Deduction version of the rule.
But we have to consider that the "standard" version of Natural Deduction does not have a rule like "Existential Specification": "from $\exists x Px$, derive $Pc$, for a new constant $c$".
Why so ?
Exactly in order to avoid the fallacy you have rediscovered:

"There is an Even number." Let $3$ a new name for it. Thus, from the premise above, using ES: "$3$ is Even". Now "generalize" it with UG to conclude with: "Every number is Even".

As you can see the Natural Deduction for Existential Elimination is more complicated.
Also Hilbert-style proof system, where we have the Generalization rule, cannot have Existential Specification.
Assume it; then we have (by Deduction th): $∃xPx → Pc$, and also: $∃x¬Px → ¬ Pc$.
By contraposition: $¬¬Pc → ¬∃x¬Px$ that (in classical logic) amounts to the invalid: $Pc → ∀xPx$.
You can see e.g. P.Suppes, Introduction to Logic (1957) for a detailed discussion of quantifiers rules and related restrictions.
See page 90 for the fallacy we are discussing, and see page 91 for additional restriction on UG necessary to avoid that fallacy when the system has ES.
A: If you follow these guidelines, what you can safely do with universal generalizations should not be an issue.  Here, I am assuming proofs are ordered lists of statements. No statement may refer to or depend on a subsequent statement.
It should be simple, but I found making universal generalizations perhaps the most difficult thing to master in formal logic. I came up with the following guidelines that I have used for several years now, and that can also be used in ordinary, informal proofs:
How to introduce free variables
Only introduce new free variables by means of a premise or existential specification. Though it is not usually done in mathematical proofs anyway, do not introduce new free variables by universal specification.
How to discharge a premise
When discharging a premise to obtain a conclusion, your conclusion should contain no free variables that were introduced in that premise or on subsequent lines. This may require first doing existential generalizations in the last statement to get rid of the free variables introduced by existential specifications in the interval. Then introduce $\implies$ or $\neg$ depending on whether a contradiction was obtained. Then do universal generalizations on any free variables that were introduced in that premise. This is the only time you should be doing universal generalizations.
When a premise is discharged, it, along with subsequent statements up to but not including the conclusion, will be deactivated so that other statements may not refer to or depend on them.
EXAMPLES
1. Conditional (direct) proof
Premise: $~~P(x)~~~~~~~~~~~~~~~~~~~~~~~~~~$ (introduces free variable $x$)
$~~~~~~\vdots$
Introduce free variable $y$ by existential specification
$~~~~~~\vdots$
Derive statement: $~~Q(x,y)$
Conclusion: $~~\forall a: [P(a) \implies \exists b: Q(a,b)]~~~~~~$ (no free variables $x$ or $y$)

2. Proof by contradiction
Premise: $~~P(x)~~~~~~~~~~~~~~~~~~~~~~~~~~$ (introduces free variable $x$)
$~~~~~~\vdots$
Derive statement: $~~Q \land \neg Q~~~~~~$ or $~~~~~~Q\iff \neg Q~~~~~~$  (contradiction)
Conclusion: $~~\forall a: \neg P(a)~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~$ (no free variable $x$)
