Project Page

POPL2026 Formal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics and Its Applications

Extended Version. Appendix A of the extended version provides a correspondence between paper definitions and the code.

Authors: Aurèle Barrière, Victor Deng and Clément Pit-Claudel.

This repository contains mechanized proofs, in Rocq, about JavaScript Regular Expressions. This includes:

• a new backtracking tree semantics for JavaScript regexes, in folder Semantics.
• a proof that this semantics is equivalent to the Warblre mechanization of JavaScript regexes, in folder WarblreEquiv.
• a proof of the PikeVM linear-time matching algorithm supporting a subset of JavaScript regexes, in folder Engine. The algorithm is adapted to fit JavaScript unique quantifier semantics, following section 4.1 of Linear Matching of JavaScript Regular Expressions.
• proof of JavaScript regex contextual equivalences, in folder Rewriting.

1. Create a local opam switch:

   opam switch --no-install create .
   

2. Pin the version of Warblre:

   opam pin add --no-action warblre.0.1.0 https://github.com/epfl-systemf/Warblre.git#a5a312072b892f4fb0343b8c2ac9d35d451c84f1
   

3. Install dependencies:

   opam install --deps-only .
   

4. Build all proofs with dune build.