I didn't read it as a critique of formal program analysis either. In fact, several aspects of his approach can be found in formal verification of probabilistic systems. However to me, it seems that the author thinks to have accomplished the same thing as the author of TTTM.

> The mathematical method described here has a number of advantages over formal verification, including reduced code size and complexity.

My comment was intended to stress that the authors achieved different things. This article proved that the game design is sound, i.e. verification at model-level, while the original one proved that the implementation cannot reach certain undesired states. Both are perfectly reasonable, justifiable and necessary.