vermillion. LL(1) parser generator verified in Coq
CoStar. A parser based on the ALL(*) algorithm, implemented and verified in Coq.
AllStar. Haskell
