The field of formal methods and game theory is witnessing significant advancements, driven by innovative applications of automata theory, regular languages, and decision procedures. Researchers are exploring new frontiers in model checking, satisfiability modulo theories (SMT), and mean payoff games, leading to improved efficiency and expressiveness in formal verification. Notably, the development of polyregular functions and cycle patterns is enabling more effective analysis of complex systems. Furthermore, the investigation of commutativity problems in formal series and the algorithmic analysis of systems with affine input and polynomial state dynamics are opening up new avenues for research. Noteworthy papers include: Simplifying LTL Model-Checking Given Prior Knowledge, which presents a novel approach to simplifying automata for more efficient model checking. Polyregular Model Checking, which reduces the model checking problem for a subset of Python to the satisfiability of a first-order formula over finite words. The commutativity problem for effective varieties of formal series, and applications, which shows that commutativity is decidable for all classes of series that constitute a so-called effective prevariety.