Modern regex engines differ in many ways: syntax, semantics, and even matching complexity. Most of these differences come from advanced features (e.g., lookarounds) and semantic choices (e.g., reporting capture-group boundaries).

To allow for regex interoperability across languages, the I-Regexp standard (RFC 9485 An Interoperable Regular Expression Format) defines a regex dialect whose syntax and semantics are restricted in a way that makes it possible to implement I-regexp matching on top of most existing engines.

Until now, I-Regexp's interoperability claims had never been formally studied. We provide the first mechanization (in the Rocq proof assistant) of I-Regexp's syntax and semantics, and we prove the correctness of the translation function from I-Regexp to ECMAScript regexes defined in the specification. In doing so, we confirm that I-Regexp is indeed interoperable with JavaScript.