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.

In a previous blogpost, Erik wrote about how he implemented the linear time matching algorithm from [RegElk+PLDI24] in the popular regex engine RE2. In this one, we're looking at how to do the same thing for the official regex engine from the Rust language. Namely, we add support for unbounded captureless lookbehinds.

Specifications (such as RFCs, programming language standards) are typically written in natural language. To formally verify an implementation of such a spec, we need two things: a mechanization of the spec (in a theorem prover like Coq, Lean, Dafny, …), and a proof of correctness relating the implementation to the mechanized spec.

The correctness of the proof is guaranteed by the theorem prover. But who checks the correctness of the mechanization? The original spec is in natural language, so the best we can do is an audit. To make these audits easier, some specs are written in a “literate” style, with comments from the spec interleaved throughout the mechanization. This helps a lot, but… who checks the comments? In this post, I present SpecMerger, a tool that checks that literate comments match the spec they came from.

Modern regexes are fiendishly complex: beyond traditional features like alternations and loops, they include complex constructs such as backreferences, possessive groups, recursion, conditionals, or bounded (and sometimes even unbounded!) lookarounds.

Surprisingly, the complexity characteristics of these modern regex features are not fully known. Take lookarounds, for example: until recently, if you wanted a regex flavor that supported lookarounds, you had to use a backtracking-based algorithm.