The undecidability of the halting set is done via proof by contradiction (in the constructively friendly way), i.e. we assume there exists some algorithm by we can determine whether an arbitrary program halts and we show that that leads to a contradiction, so we say no such program exists. But can we then conclude that for any formal system there exist programs which we cannot prove they will halt and we cannot prove they will not halt? There seems to be some connection to Godel's 1st Incompleteness Theorem here. The question also arises in relation to the Collatz conjecture. It was proved that an appropriate generalization can be constructed for which the Collatz conjecture is generally undecidable, but does that mean it is possible that we could prove the Collatz conjecture independent of ZF (or ZFC). That seems ridiculous, as the Collatz conjecture is the sort of computational claim that one would expect is either true or false, not undecidable.
With suitable hypotheses, the answer to your question is "yes". The suitable hypotheses would include that the formal system is sound (in particular, if it proves that a certain computation never halts then that computation will not in fact halt) and that it's effective, i.e., that an algorithm can tell what is and what is not a proof.
Now if we had such a formal system that could prove, for any given program (and input) that it halts or that it doesn't halt, then we'd have the following decision procedure for the halting problem. To decide whether a given program halts, start running the program and, in parallel, start searching for a proof, in your formal system, that it doesn't halt. If the program halts, output "yes"; if you find a proof that it doesn't halt, then output "no".
Since there cannot be a decision algorithm for the halting problem, this argument shows that there cannot be a formal system (of the sort described above) that proves non-halting for all programs that don't in fact halt.