I recently became aware of the effort here to make a formal grammar for TFormula. This is great!
I had made my own attempt for correctionlib using a PEG parser (see here for early thoughts in that direction), with the current grammar viewable here. As of this PR the parsed AST is also accessible from python. Perhaps it might be useful to investigate if we can merge efforts? One feature of the C++ PEG parser is it will in general be much faster than lark.