[en] We show how the software Walnut can be used to obtain concise proofs of results concerning variants of the famous Wythoff game, in which blocking maneuvers or terminal positions are added, as discussed respectively by Larsson (2011) and Komak et al. (2025). Our approach provides automatic proofs that both confirm and extend their results, and the same techniques apply to newly introduced variants as well. Then, using classic techniques, we obtain new recursive and morphic characterizations of Wythoff-type games where the set of terminal positions (x, y) satisfy x + y ≤ l. The use of Walnut in combinatorial game theory is relatively recent, and only a few examples have been explored so far. The Wythoff game, being directly connected to the Fibonacci numeration system, proves especially well suited to this kind of approach. It permits us to solve instances for fixed value of a parameter.
