Careful with that formulation.
https://en.wikipedia.org/wiki/Rice%27s_theorem
https://en.wikipedia.org/wiki/Solved_game
Several major strategy games, notably checkers, have been formally solved. That does make it possible to prove that some engines for those games behave in an optimal way (although it would still be impossible to verify whether an arbitrary program is equivalent to an optimal engine, because the arbitrary program could do something else first whose outcome couldn't be foreseen by the optimal-engine detector).
Although chess has a higher branching factor and a greater depth in various ways than games that have been solved, nobody has found a theoretical barrier to solving it, which in turn means that we can't rule out the possibility of a proof that a particular engine is optimal.
From the formal computation theory standpoint, the situation is even more extreme: the game tree given the threefold repetition rule is finite, which means that we can immediately write down an explicit game tree brute force engine which is guaranteed to perform optimally in every position. This is probably just a handful of lines of code! While this engine can't actually make a single move in a human timescale, from an algorithmic point of view it plays perfectly and we can be sure of that.
The theorems on undecidability of program behavior don't include time constraints like this because they're established using models of computation like Turing machines, where physical limitations of real computing devices are no issue.