Parsers are the “trusted gatekeepers” of high-assurance software; larger programs rely on them to consume input from untrusted sources. In the high-assurance parsing project, we are using formal methods to develop parsers that come with machine-checked proofs of their correctness. Parsers are natural targets for formal verification because they are hard to implement correctly but easy to specify: while parser bugs are pervasive (with grave security consequences), parsers have a simple high-level definition of what constitutes correct behavior. By proving that a parser conforms to this correctness specification, we can guarantee that it is free of common classes of bugs. The two verified parsers we have developed, Vermillion and CoStar, occupy different points on the “speed vs. expressiveness” spectrum of parsing algorithms. Vermillion runs in linear time and is compatible with a more restricted class of grammars; CoStar is slower in the worst case, but it achieves linear performance on many real-world grammars and is suitable for parsing a broader range of languages.