Verbatim++: verified, optimized, and semantically rich lexing with derivatives
Derek Egolf, Sam Lasser, Kathleen Fisher · 2022
Lexers and parsers are attractive targets for attackers because they often sit at the boundary between a software system's internals and the outside world. Formally verified lexers can reduce the attack surface of these systems, thus making them more secure.