This project aims to formalize Cypher, a graph query language, in the Coq proof assistant. The purpose of the formalization is to make a rigid foundation for further evolution of the language, as well as to provide a framework for verifying optimizations of queries.