本文提出了 ARMOR，这是首个针对 X.509 证书链验证逻辑（CCVL）的大规模形式化验证实现，旨在为 RFC 5280 的大部分内容提供机器可检查的正确性保证。ARMOR 的设计目标有两个：一是作为 RFC 规范的形式化、机器可检查的替代品，二是作为参考实现和测试预言机。其架构采用模块化设计，将 X.509 CCVL 分解为多个模块，每个模块独立地进行规格说明、实现和验证。目前，ARMOR 已正式验证的模块包括 PEM 和 ASN.1 X.690 DER 语言（子集）的规格说明与解析、证书链构建，以及单个证书内和证书链中证书字段所需属性的多种语义性质。为了实证评估这些目标的达成情况，作者将 ARMOR 与 11 个开源 X.509 实现及一个开源证书检查工具进行了比较，评估其规格准确性和运行时开销。实验结果显示，尽管 ARMOR 引入了较高的运行时开销，但通过使用它，能够检测出若干不符合规范的情况。最后，作者展示了 ARMOR 的端到端应用：将其集成到 BoringSSL 的 TLS 1.3 实现中，并使用 Curl 进行测试。这项工作为证书链验证的正确性提供了可验证的基准，有助于发现现有实现中的合规性问题。