本文提出并实现了一个名为 Verbatim 的可执行词法分析器（lexer），其开发和验证均基于 Coq 证明助手。词法分析器和解析器常被用作大型软件系统的前端，负责连接外部输入与系统内部逻辑，因此成为攻击者试图攻陷整个系统的天然目标。作者认为，一个经过形式化验证、具备机械化词法分析能力的工具能够显著降低针对这些前端的攻击效力。论文的核心贡献在于：1）给出了 Verbatim 的完整实现，它是一个可执行的、与标准词法分析器规范兼容的 lexer；2）在 Coq 中机械证明了 Verbatim 相对于标准词法分析器规范的正确性，即所有正确性证明均已机器检查，避免了手工证明中可能存在的漏洞；3）分析了 Verbatim 的理论复杂度，并提供了实证性能评估结果。与依赖测试或运行时检查的传统 lexer 生成器不同，Verbatim 从构造上保证了词法分析的正确性，为构建高可信软件前端提供了新的思路。该研究适合对形式化验证、编译器前端安全、高保证软件工程感兴趣的 researchers 和开发者；对于蓝队而言，理解这类验证工具可帮助评估在关键系统中引入形式化验证组件的可行性和收益，从而减少外部输入处理环节的潜在攻击面。然而，由于本文尚未发布完整工具链或大规模应用案例，其实际工程部署价值仍需进一步验证。