Yes, there are some general methods to attain your properties for
any theory $T$.
Method 1. For any theory $T$ extending ZFC, let $T'$ be the
theory consisting of the following:
- ZF
- all the arithmetic consequences of $T$
- all assertions of the
form $\text{AC}\to\sigma$, where $\sigma$ is in $T$.
If $T$ is a computably enumerable theory, then so is $T'$.
Since all the axioms of $T'$ are provable in $T$, we have $T\vdash
T'$ and consequently
$\newcommand\Con{\text{Con}}\Con(T)\to\Con(T')$. Also, notice that
$T'+\text{AC}$ is equivalent to $T$, which is another way to see
that $\Con(T)\to\Con(T')$.
Conversely, if $T'$ is consistent, then $T$ is consistent, since
otherwise it would prove a contradictory arithmetic assertion, and
this would be amongst the axioms of $T'$. So $\Con(T')\to\Con(T)$. The point is that the consistency strength of a theory is contained already in its arithmetic consequences. This is clear enough, but perhaps you don't regard it to fulfill
the "niceness" property you mentioned in statement 3, in which
case I refer you to method 2. For example, I don't know in general
how to build a model of $T$ from a model of $T'$ by forcing or by
going to an inner model.
Meanwhile, $T'$ does not prove AC, if consistent, because if $M$
is any model of $T$, then let $W$ be a model of
$\text{ZF}+\neg\text{AC}$ with the same arithmetic as $M$. For
example, we could use $L(\mathbb{R})^M$, if AC failed there, or we
could in any case let $W$ be a symmetric extension of $M$ by Cohen
forcing. Since $W$ and $M$ have all the same arithmetic
assertions, we get $T'$ in $W$ with $\neg\text{AC}$.
Method 2. For any theory $T$ extending ZFC, let $T'$ be the
theory asserting:
- ZF
- all axioms of the form $\text{AC}\to\sigma$ for $\sigma$ in $T$
- plus the assertion that if AC fails, then $\sigma$ holds in $\newcommand\HOD{\text{HOD}}\HOD$, for every $\sigma$ in $T$.
Thus, the theory $T'$ basically asserts that either $T$ holds outright, or it holds in HOD. And if $T$ was a finite extension of ZFC, then $T'$ will
be a finite extension of ZF.
Since $T'+AC=T$, we get $\Con(T)\to\Con(T')$ in a nice way.
Conversely, we get $\Con(T')\to\Con(T)$ in a nice way, since any
model of $T'$ will have a definable inner model of $T$.
Lastly, $T'$ does not prove AC, if consistent, since if $M\models T$, then we can find an extension $W$ satisfying $\neg\text{AC}$ such that $\HOD^W=M$. Thus, $W$ will satisfy $T'+\neg\text{AC}$.