Ce projet vise à formaliser Cypher, un langage de requête graphique, dans l'assistant de preuve Coq. L'objectif de la formalisation est de poser des bases solides pour l'évolution du langage, ansi que de créer un créer un cadre de vérification des optimisations de requêtes.