Linden: A Linear Dependable Engine for JavaScript Regular Expressions

Project Page

Related Publication

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.

About

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.

Usage

1. Create a local opam switch:

   opam switch --no-install create .
   

2. Add needed dependency repositories:

   opam repo add rocq-released https://rocq-prover.org/opam/released
   

3. Install dependencies:

   opam install --deps-only .
   

4. Build all proofs with dune build.