Summary
Parsing untrusted inputs into formats usable by software systems is a ubiquitous, security-critical task. Bugs in parsing components are one of the most common sources of critical security vulnerabilities in practice. As more software is automatically generated by AI systems, this problem exacerbates as manual human auditing for correctness and security is reduced or eliminated. The project's impacts are to enable mathematical verification of correctness, safety and security of parsing components for a variety of parsing domains encountered in practice. Any code using this system, even AI gene
