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

本文针对认证数据结构（Authenticated Data Structures）的开发与实现正确性难题，提出了一种基于新关系分离逻辑的形式化证明方法。认证数据结构允许不可信的第三方执行操作并生成可验证的输出证明，但此类系统容易因实现错误导致安全漏洞。作者首先设计了一种关系分离逻辑，用于推理使用抗碰撞哈希函数的程序，该逻辑为类型系统构建了两个语义模型，从而阐释了如何通过类型抽象来强制实现安全性与正确性。基于这些模型，论文进一步证明了库中多项优化的正确性，并展示了如何将优化的、手工编写的认证数据结构实现与自动生成的代码安全链接。所有结果均在 Coq 证明助手中使用 Iris 框架完成机械化验证。该工作为认证数据结构库的可靠实现提供了坚实的理论基础，有助于减少此类系统中的安全缺陷。适合形式化验证、编程语言理论与安全协议交叉领域的研究者阅读。