We say that a model of ZFC $M$ correctly solves that halting problem if for every turing machine $T$, $T\text{ halts} \iff M \models T \text { halts}$.
Is there a countable computably saturated model of ZFC which correctly solves the halting problem? (See pg 3 of https://arxiv.org/pdf/1104.4450.pdf for what computably saturated means.)
Sure. Any (consistent) theory (in a computable language) has computably saturated models, so just take $T$ to be (say) the theory ZFC + all true $\Pi_{17}$ statements of arithmetic. $T$ correctly decides (among other things!) whether the $e$th Turing machine halts, for each standard $e$, so any model of $T$ correctly solves the halting problem; now simply take an arbitrary computably saturated model of $T$.
Why do all appropriate theories have computably saturated models? Well, the point is that we only have to realize countably many types. Start with an arbitrary countable model $M$ of the theory, and list the computable types; at stage $s$, pass from the current model to a countable elementary extension realizing the $s$th computable type of that type is finitely consistent with the current model, and otherwise don't change the model - the union of this elementary chain will be a saturated model of the theory.