Graphs are widely used in various domains to model complex relationships, often requiring the specification and verification of their properties. These properties may involve complex conditions placing, e.g., structural requirements on subgraphs of unbounded size. In this paper, we propose graph formulas as a new formalism for specifying graph properties, providing a higher level of “graphical” abstraction compared to well-known approaches such as monadic second-order logic. We show how these graph formulas can be translated into alternating graph automata, allowing to check computationally difficult graph properties, such as the existence or non-existence of Hamiltonian paths.