Research and development of graph query languages has been gaining
traction with the increase in popularity of graph databases,
specifically due to the flexible schema and other rich semantic
offerings of the latter's most common underlying data model: the
property graph. This has culminated in the standardization of the ISO
Graph Query Language (GQL) as ISO/IEC 39075 in 2024, the first
international standard for property graph-based graph query
languages. However, ISO/IEC 39075 codifies its semantics informally
across 600+ pages of prose, making it difficult to formally reason
about the standard or for a standard-faithful implementation.

Existing formalizations are not adequate because they either: (1)
significantly reduce the semantic complexity by omitting bag
semantics, schemas, and composite queries on multiple graphs; (2) or
significantly reduce the syntactic complexity by only considering
isolated fragments such as pattern-matching, leaving the full query
pipeline unformalized. Yet it is these semantic--syntactic features
that make formalizing GQL non-trivial.

We present MGQL, the first mechanized, small-step operational
semantics for a substantial read-only fragment of GQL that is grounded
in the ISO/IEC 39075 standard. Our formalization models multi-graph
property graphs with mixed edge directionality and supports a large
fraction of GQL pattern constructs: quantified paths and edges,
directional and undirected matching, label expressions, pattern lists,
and composite queries. The semantics is supported by a schema-aware
type system that refines variable types via closed-graph schemas,
tracks nullability, supports multiple composite query operators, and
models quantified-path bindings with list types. We prove that our
type system is sound, ensuring an end-to-end guarantee of well-formed
queries yielding results that conform to their declared schemas. MGQL
provides the first bridge between GQL's informal specification and a
mechanized implementation, enabling formal reasoning about
correctness.