Graph Neural Networks (GNNs) are a common formalism for graph learning. We provide results on the complexity of basic verification problems for GNNs like whether a certain value can be achieved, or whether two GNNs are equivalent. We also show a close connection between certain flavors of GNN and Presburger logics: these are two-variable logics where one can assert a linear inequality between certain cardinalities defined by subformulas. For example, in a labelled graph one can assert that the number of blue neighbors is equal to the sum of the number of red neighbors and the number of green neighbors. We show equivalence between GNN models and Presburger logics, and derive decidability results for Presburger logics. This is joint work with Chia-Hsuan Lu and Tony Tan.