Is there a formal way of defining a Zeno Machine?
Hamkins' survey Infinite time Turing machines, linked by Yuval Filmus, formally defines a computational model (Infinite time Turing machine) that meets the requirements of a Zeno machine.
The definition of ITTMs does not use the time based framing; instead it is an extension of classical binary TMs to be defined at transfinite ordinals.  A classical TM has a start status (empty tape, etc.) and a function to get the successive status; a ITTM just adds the status of the machine at limit ordinals.
Rather than taking the limit of the cells in the tape, as suggested and refuted in the question, we take the limit supremum.  Formally for
$$
T(\lambda)_k = \limsup_{n\rightarrow \lambda} T(n)_k
$$
where $\lambda$ is a limit ordinal, $k$ is the index of some cell, and $T$ is the function that gives the tape at some numbered step.
The $\limsup$ ensures that it will always be defined for any sequence (since the alphabet is bounded).  If the normal limit does not converge for some cell then (for a binary alphabet) the cell at time $\lambda$ will be $1$, since in order for it to not converge it must be $1$ at an infinite number of steps.
The state and the location of the read head are resolved much more simply.  Just as there is a start state, there is also a limit state.  At times corresponding to limit ordinals the machine is in the limit state, and the read head is set to the beginning of the tape.

The linked paper does not even mention &quot;Zeno machine&quot; (although it mentions Zeno) and ITTMs may not be the only formal model of a Zeno machine possible (beyond trivial modifications).  However it is a model of computation that allows a Turing machine to perform an infinite number of operations and then continue calculations, so if you are looking for a formal way to talk about Zeno Machines ITTMs work just fine.