We show how the software Walnut can be used to obtain concise proofs of results concerning variants of the famous Wythoff game, incorporating blocking maneuvers or additional terminal positions, as discussed by Larsson (2011) and Komak et al. (2025), respectively. Our approach provides automatic proofs that both confirm and extend their results, and the same techniques apply equally to newly introduced variants. Then, using classical techniques, we obtain new recursive and morphic characterizations of Wythoff-type games in which the terminal positions (x,y) satisfy x + y ≤ ℓ. The use of Walnut in combinatorial game theory is relatively recent, and only a few examples have been investigated 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 a fixed value of a parameter.