Transformers are revolutionary neural networks architecture, which has been the backbone of our modern Large Language Models (LLMs). Despite the success of transformers in practice, we often do not know why they work (or occasionally also, why they do not work). Recent years have witnessed rapid progress in understanding transformers through the lens of logic and automata (in the community called FLaNN = Formal Languages and Neural Networks). In particular, the toolbox from logic and automata (i.e. connections to linear temporal logic) has helped us understand why PARITY (and in general “state-tracking”) is difficult for transformers. I will recount some of the fundamental results in the field and open problems at the intersection of logic, automata, verification and transformers.