Skip to content

The Linden Regex project aims to take a new look at modern regexes.

  • We work on new linear-time algorithms to match modern regex features.
  • We design and mechanize the semantics of real-world regex languages.
  • We write mechanized proofs of regex properties, and of the correctness of matching algorithms.

Check out the project homepage.

Pinned Loading

  1. Linden Linden Public

    Formal Verification for JavaScript Regular Expressions

    Rocq Prover 15 1

  2. RegElk RegElk Public

    Ocaml Linear Engine for JavaScript Regexes, implementing the algorithms described in Linear Matching of JavaScript Regular Expressions at PLDI24

    OCaml 26 3

  3. Warblre Warblre Public

    A Rocq Mechanization of ECMAScript 2023 Regexes

    OCaml 16 4

  4. I-regexp_mechanization I-regexp_mechanization Public

    A Rocq mechanization of XSD and RFC 9485 (I-Regexp) regular expressions

    Rocq Prover

Repositories

Showing 10 of 14 repositories
  • Linden Public

    Formal Verification for JavaScript Regular Expressions

    LindenRegex/Linden's past year of commit activity
    Rocq Prover 15 1 0 4 Updated Oct 8, 2026
  • js-regex-matching-complexity Public

    Complexity results about JavaScript regex matching, mechanized in Rocq

    LindenRegex/js-regex-matching-complexity's past year of commit activity
    Rocq Prover 0 0 0 0 Updated Oct 5, 2026
  • RegElk Public

    Ocaml Linear Engine for JavaScript Regexes, implementing the algorithms described in Linear Matching of JavaScript Regular Expressions at PLDI24

    LindenRegex/RegElk's past year of commit activity
    OCaml 26 3 0 2 Updated Oct 1, 2026
  • LindenRegex/lindenregex.github.io's past year of commit activity
    HTML 0 0 0 0 Updated Sep 7, 2026
  • babblre Public

    JS / WASM builds of 80+ regex engines.

    LindenRegex/babblre's past year of commit activity
    C 1 0 0 0 Updated Aug 26, 2026
  • viz Public

    Graphical explorer for JavaScript regex semantics using backtracking trees

    LindenRegex/viz's past year of commit activity
    TypeScript 0 0 0 0 Updated Aug 26, 2026
  • Warblre Public

    A Rocq Mechanization of ECMAScript 2023 Regexes

    LindenRegex/Warblre's past year of commit activity
    OCaml 16 4 2 2 Updated Jul 8, 2026
  • I-regexp_mechanization Public

    A Rocq mechanization of XSD and RFC 9485 (I-Regexp) regular expressions

    LindenRegex/I-regexp_mechanization's past year of commit activity
    Rocq Prover 0 0 0 0 Updated Jul 6, 2026
  • VirtualTrees Public
    LindenRegex/VirtualTrees's past year of commit activity
    Rocq Prover 0 0 0 0 Updated Jun 22, 2026
  • .github Public
    LindenRegex/.github's past year of commit activity
    0 0 0 0 Updated Mar 23, 2026