The parser combinators are a common approach in functional languages. Basically, instead of generating the whole parser from a grammar, you assemble a lot of small functions, in other functions. The resulting code often ressembles the grammar very closely, and all of the intermediate parsers are very easy to test.

Proving with Coq the soundness of a parser compared to its grammar is a cool approach! The biggest problem one has when writing parsers in "safe" systems like parser generators or parser combinators, is the gaps between the input language intended by the designer, the input language described by the grammar and the input language described by the code. Anything that can reduce those gaps is welcome.

I shoul try at some point to use Coq or some SMT based system to hunt ambiguity in formats. That would make an interesting research ;)