Este projeto tem o objetivo de formalizar o Cypher, uma linguagem de consulta em grafos, no assistente de provas do Coq. A finalidade da formalização é criar bases rígidas para a evolução futura da linguagem, além de fornecer um framework para verificar otimizações de consultas.