Great work by the LANGSEC crowd. My recent interest in parsers was those verified for correctness or security. So, they have security and a certain amount of correctness. A great next step would be combining it with work on formal verification of parsers or generators (see below). On top of that, ensure the subset could generate SPARK and/or CompCert-compatible C code to automate much of the rest of the problem.

TRX formally verified parser interpreter http://arxiv.org/pdf/1105.2576.pdf

Validating LR(1) Parsers http://gallium.inria.fr/~xleroy/publi/validated-parser.pdf

Verifying a parser for a C compiler http://gallium.inria.fr/~scherer/gagallium/verifying-a-parse...