Appreciate the feedback. My plan was to push some formal methodists or LANGSEC types to try to do a verified GLL if the opportunity arises. So far, there's been SLR [1], LR(1) [2], and PEG [3] verified for correctness. Think verified GLL generator is ideal next target given benefits?

[1] http://users.cecs.anu.edu.au/~aditi/esop.pdf

[2] http://pauillac.inria.fr/~xleroy/publi/validated-parser.pdf

[3] https://arxiv.org/pdf/1105.2576.pdf