Este proyecto pretende formalizar Cypher, un lenguaje de consulta de grafos, en el asistente de pruebas Coq. El propósito de la formalización es construir una base rígida para la evolución posterior del lenguaje y proporcionar un marco para verificar las optimizaciones de las consultas.