Let me expand a little my comment because it is more subbtle than what I suggested and it relies heavily on a recent result. I agree that this does not exactly answser your question but is I think relevant.
I will proove that this decomposition result hold in any boolean Grothendieck toposes (which are in particular place where no form of the axiom of choice holds, not even dependant choice... in this frame work completness is taken in the sense of Cauchy filter or Cauchy approximation but not in the sense of cauchy sequences...).
So let $T$ be a boolean Grothendeick topos, $C$ a $C^*$-algebra in $T$ and let $\phi$ be a linear form on $C$ whose norm is smaller than $1$.
In this paper, I proved that there is a classifying locale $Fn C$ for linear form of norm smaller than $1$ on $C$ (see section 3.5 and proposition 4.2.3). $\psi$ is a point of $Fn C$.
By Barr's covering theorem $T$ admit a covering $p:T' \rightarrow T$ such that $T'$ is boolean and the axiom of choice holds in $T'$. Moreover as $T$ is boolean $p$ is automatically an open surjection.
Pulling back everything to $T'$ ($C$ has to be completed after pull-back of course), one have a $C^*$-algebra $p^* C$ with a point of $Fn p^* C = p^* Fn C$. One can then apply the decomposition of $\psi$ in $\psi_+$ and $\psi_-$ in $T'$. They are again linear form of norm smaller than $1$, hence give rise (internally) in $T'$ to two new point of $p^* Fn C$.
By uniqueness of these two point, they actually lift to global section, i.e. to external morphisms from $T'$ to $p^* Fn C$ over $T'$.
$\psi_+$ and $\psi_-$ are characterised by properties which are pullback stable (the positivity and the condition one the norm) and are unique hence they are automatically compatible with the canonical descent data (for $p$) on the point and on $p^* Fn C$. Then as $p$ is an open surjection it is an effective descent map for locale and hence the two points $\psi_+$ and $\psi_-$ are pullback of two points $Fn C$ in $T$ that we also denote $\psi_+$ and $\psi_-$, these two points also satisfies the conditions on the norm and of positivity because their pullbacks along a surjection do. SO this prove the existence of the decomposition in $T$.
The uniqueness can also be proved by pulling back to $T'$, but I'm pretty sure that the uniqueness can be proved directly without the axiom of choice quite easily...
Let me mention the consequence of this for your question.
It is an extremely encouraging sign that the results can be proved without AC.
The result will holds in any model of ZF constructed using combination of forcing and permutation models (because these corresponds to certain boolean Grothendieck toposes).
It is going to be very hard to produce a counterexemple if it is false, first because of the previous observation and secondly because for any $C^*$-algebra "geometrically described" one should be able to use the previous argument in a booleanisation of a classifying topos to obtain a proof for this specific exemple. So the counter example has to be either non-explicit or has to rely on non geometric constrution (which in my opinion mean a very weird construction)
It might be possible to use a similar argument to proove that this result holds in the Solovay model (which if I remeber correctly is constructed by first taking a forcing model and then an inner model, but I'm not really familiar with inner model so I can't say anything clever about that...)
