Veriflex is a verified lexer generator for Lean 4 based on Brzozowski derivatives of regular expressions. Its design is heavily inspired by the paper Verbatim: A Verified Lexer Generator by Egolf, Lasser and Fisher.
The library provides inductive types RE for regular expressions and Rule for regular expressions together with a semantic action, i.e. a function from the lexed string to tokens.
Rules are parameterized over the token type, and a grammar consists of a list of rules.
The file Example.lean contains a simple example for how the library can be used.
This library is still under active development. The computation of Brzozowski derivatives is implemented and fully verified. The lexer using the maximal munch principle is implemented and works, but not yet verified relative to its spec.
Expect major breaking changes before we reach version 1.x.
Please consult Contributing.md for information about how to contribute to the project.