Has the semantics of TeX (as a programming language) ever been formalized?
No, to my knowledge there has been no work on formalizing TeX of the kind you are interested in.

(What follows is a subjective and personal commentary). I think it is an intriguing and well-posed idea, and your motivation of using it to perform optimizations sounds reasonable -- another related question is whether you could define a bytecode format for it to speed up interpretation. On the other hand, the idea has two downsides.

First, it is not clear to me that there is a large potential for optimizations (for example, what kind of program-preserving transformations could one perform to speed up computation?), as it may be that the language semantics is intimately related to parsing the character flow, and thus not very accommodating to the design of optimization-friendly intermediate representations.

Second, the need for improvements in TeX interpretation speed is not well-established: the speed of batch speed building has remained reasonable thanks to hardware improvements. Cases where speedups could be welcome are complex graphics package (beamer presentations can take quite some time to build), packages embedding rich computations (but then another language may be more appropriate), and use cases requiring fast rebuild for instant user feedback (but then incrementality, rather than optimization, may be the point; a formal semantics would certainly help reason about incremental implementations as well).

That is to say: this sounds like a fun, instructive topic, but it is not clear to me that the practical justifications for doing the work are strong. If someone was interested in doing it out of curiosity, that sounds like an excellent adventure, but otherwise there may be other ways to employ the same skillset whose impact would be more sought-after by end-users.