Regexes are an extremely practical tool to process text; so much so that these are available in the standard library of a wide range of programming languages (Perl, JavaScript, C++, PHP, Java, …), or even as a standalone library, such as the RE2 library or the Rust regex crate. Yet, despite their ubiquity, the set of features included in modern regexes, and even the semantics of said features, are not that well-defined and vary from one implementation to another. “Regex” does not designate one single language with a fixed syntax and semantics, but rather a family of many similar looking languages with subtle differences in their semantics. This situation makes it difficult to correctly reason about regexes, including stating and proving theorems about them. The goal of this project is to mechanize the ECMAScript semantics for regexes, enabling further mechanized work on them from a proof assistant. Using our mechanization, we additionally prove, for the first time, some properties of the semantics.