Weakest axiom to make ZFC+X imply GCH? What is the weakest axiom $X$ that we can add to $ZFC$ to enable
$GCH$ to be proven? Obviously we could just add $GCH$ but because
$ZF\vdash GCH\implies AC$ that makes $AC$ redundant. So $X$ would
have the properties that $ZF\vdash AC+X\implies GCH$ but $ZF\nvdash GCH\implies X$.
Is such an $X$ known?

I think that your question is inherently problematic. We can't quite say "weakest". 
It can be $V=L[A]$ for some $A\subseteq\omega_1$, but that's not right since we have models of $\sf GCH$ which are not of this form (e.g. start with $L$ and add a single Cohen subset to some regular $\kappa>\omega_1$, or to all of them).
Requiring $\sf HOD$ is too weak, since it is known that $\sf HOD$ need not imply $\sf GCH$, but we can do all sort of crazy shenanigans and still have $\sf GCH$ around.
We can also always force $\sf GCH$ by collapsing cardinals. Perhaps a proper class of them. Which can completely mess up most "nice definability axioms".
So you end up with $X$ being a very nondescript axiom, which may or may not be just $\sf GCH$ itself again, or something equivalent to it (e.g. $\lozenge$ exists for all regular cardinals+$\sf SCH$ or something like that).
