LL(1) Parser Generator

In this formalization, we implement an LL(1) parser generator that first pre-computes the NULLABLE set, FIRST map and FOLLOW map, to then build a lookahead table. We prove correctness, soundness and error-free termination for LL(1) grammars. We provide the JSON grammar and show how to parse a tokenized JSON string using a parser created with the verified parser generator. The proof structure is significantly based on Vermillion, an LL(1) parser generator verified in Coq.