The axiom of choice implies that there is a subset $E$ of $\mathbb R$ that are Vitali sets : this means that $E$ is a transversal with respect to the additive subgroup $\mathbb Q$ of $\mathbb R$, i.e. the natural projection $p:{\mathbb R} \to \frac{{\mathbb R}}{\mathbb Q}$ becomes bijective when restricted to $E$.
It is also known that there are models of ZF where no Vitali sets exists.
My question is in-between : is there a formula $\phi$ of set theory such that it is provable in ZF that “If there is a Vitali set then $\phi$ defines a unique Vitali set”.
No, there cannot be a formula that always defines a Vitali set whenever one exists. In fact we can say something stronger: There is a model of $\mathsf{ZFC}$ with no definable Vitali set.
Assume that $\mathsf{ZF} + \mathsf{DC}$ holds but there is no Vitali set (this follows, for example, from "$\mathsf{ZF} + \mathsf{DC} + {}$every set of reals has the Baire property," which is consistent relative to $\mathsf{ZFC}$ by a theorem of Shelah.) Force with $\text{Col}(\omega_1,\mathbb{R})$ to add a well-ordering of the reals. Because the forcing is countably closed and $\mathsf{DC}$ holds in the ground model, no reals are added. The generic extension has a well-ordering of its reals, so it has a Vitali set. But it cannot have a definable Vitali set because the forcing is homogeneous, so every subset of the ground model that is definable in the forcing extension is an element of the ground model.
Remark: As Andreas Blass points out in the comments, there is a more direct construction assuming the existence of an inaccessible cardinal. Let $\kappa$ be inaccessible and let $g \subset \text{Col}(\omega,\mathord{<}\kappa)$ be a $V$-generic filter. Then in the generic extension $V[g]$ every definable set of reals is Lebesgue measurable by a theorem of Solovay (in fact, every set of reals that is ordinal-definable from a real parameter is Lebesgue measurable, has the Baire property, etc.) So in this generic extension there can be no definable Vitali set.