If we consider ordinary Turing machines, we can assume that if an $i$-th machine halts, there exists a finite proof of this: just write the corresponding computation history.
But if we consider Infinite Time Turing Machines and pick an arbitrary natural number $i$, then, if an $i$-th machine halts and clocks any ordinal which is not less than $\omega$, there is no direct way to have a finite string that encodes the corresponding computation history step by step (because the computation is infinite). Does this imply that it is not possible to have a finite proof of halting for the $i$-th ITTM?
If the answer to the previous question is “No, it is possible”, then how can this be done? And what can be an example of a formal language that allows to write such proofs?