Can we formalize the operational/denotational semantics of a Turing Machine? Is there any formalization in literature?
The usual definitions of Turing machines are given in terms of formal semantics. For instance, the Wikipedia definition describes Turing machines in precise mathematical formalism. If you are looking for something even more formal, have a look at this Coq formalization of Turing machines.