本文对 Go 标准库 `crypto/internal/fips140/bigmod` 中的 `extendedGCD` 实现进行了形式化验证。该实现用于 RSA 密钥对生成中的扩展欧几里得算法，是从 BoringSSL 移植而来。然而，研究者发现了两处偏差：一是系数更新方式与原始实现不同，二是允许更大的输入域。第一个偏差导致算法不变量被破坏，第二个偏差使得原有证明不再适用。研究者修复了第一个偏差（性能提升平均 24%），并针对第二个偏差将 BoringSSL 的证明移植并扩展到更大的输入域。他们使用 Go 语言专用验证器 Gobra 证明了修复后实现的正确性和终止性，并借助 Lean 验证了一些非线性算术引理。验证过程表明，即使是经过充分审查的代码也可能存在细微错误，形式化验证是发现此类错误的有效工具，而 AI 代理可通过迭代优化不变量和引理来辅助验证。

本文介绍了使用Lean 4证明助手对StarkWare的S-two证明器中的代数中间表示（AIR）进行形式化验证的工作。S-two证明器用于在区块链上高效地证明用Cairo虚拟机语言编写的程序能够运行完成。该证明器通过一个代数中间表示（AIR）捕获Cairo语言的语义，该AIR断言存在满足特定代数约束的有限域值表。然后，加密交互式证明系统circle STARK提供一个高效验证的证书，证明AIR是可满足的。本文的核心贡献在于，利用Lean 4证明助手对AIR编码的可靠性（soundness）进行了形式化验证，即证明AIR的可满足性蕴含相应的计算性声明。这一验证确保了AIR编码不会错误地声称一个无效的程序运行完成。论文详细描述了验证过程，包括如何在Lean 4中形式化AIR的语义、约束以及soundness证明。该工作对于提高Cairo智能合约和区块链应用的安全性具有重要价值，因为它提供了一个数学上严谨的保证，防止因AIR编码错误导致的虚假计算声明。读者包括对形式化验证、区块链安全性以及零知识证明感兴趣的研究者和工程师。

本文提出了首个经过机器检查的OpenZeppelin重入防护模式正确性证明，该证明针对生产部署的Solidity源代码的Lean 4状态机模型。所有十三个定理都经过了机器检查，没有使用任何“sorry”或用户引入的公理，公理足迹仅由[propext]（一个标准的mathlib4公理）限定，并集成在持续集成中。智能合约重入攻击自2016年以来已导致超过5亿美元的损失，其中DAO 2016攻击盗取了约360万ETH，并迫使以太坊硬分叉。OpenZeppelin ReentrancyGuard模式是生产DeFi中的事实标准防御措施，但此前没有工作建立其判别能力：即该防护能阻止对易受攻击实例的攻击，保持非攻击交易的正确执行，并区分相邻的安全和易受攻击变体。以往的工作要么形式化了玩具合约上的防护正确性，要么形式化了孤立实例上的攻击可行性，但未同时涵盖两个方向及针对生产源码的边界情况。本文通过变异测试验证了三种生产实例：DAO 2016、Compound v2和Aave V3的flashLoan，以及Aave V3 flashLoan的一个最小差异突变体（flashLoanVulnerable），该突变体隔离了一个安全关键差异。三方向结构包括：(a) DAO 2016模式的攻击复现，(b) Compound v2的正确性证明，(c) 区分Aave V3符合CEI模式的flashLoan与突变体的边界案例证明。一个顶层的元定理在“无改造”原则下组合了这三个方向，并在首次跨协议压力测试（从Compound v2到Aave V3）中进行了演示；更广泛的家族可移植性是未来工作。完整的Lean 4源码、CI配置和复现命令可在GitHub上获取。

该论文针对AMD SEV（安全加密虚拟化）技术缺乏形式化安全保证的问题，提出了一套形式化验证框架。AMD SEV是机密计算中的关键技术，通过硬件内存加密保护虚拟机内敏感数据。然而，现有实现缺乏对安全性属性的严格证明。研究首先对AMD SEV规范进行设计级和属性级抽象，建立精确的模型，然后通过属性检查（property checking）验证机密性、完整性和可用性（CIA三元组）。该方法为定义和验证执行环境的关键安全属性提供了严谨的数学基础。实验表明，该框架能够有效捕获规范中的安全约束，并发现潜在的安全缺口。该工作适用于安全架构师、云服务提供商和形式化方法研究人员，有助于提升对AMD SEV安全性的信任度。

该论文提出了一种全新的方法，用于形式化规范指令集架构（ISA）的安全保证。传统上，ISA的规范仅限于功能方面，且通常以非形式化的散文形式描述，缺乏对安全保证的精确刻画。作者引入了通用契约（universal contracts）的概念——这是一种软件契约，能够表达任意不可信代码的权限边界。通用契约独立于软件抽象层次，既能为软件推理提供必要的细节，又保留了ISA设计者和CPU实现者的实现自由度。论文的核心贡献包括：（1）提出了一种通用的、可平衡硬件实现与软件客户端需求的形式化安全保证规范方法；（2）开发了Katamaran工具——一个半自动化的分离逻辑验证器，用于Sail语言描述的ISA语义，能够生成机器可检查的证明；（3）通过两个差异显著的ISA实例验证了方法的通用性：自定义能力机ISA（MinimalCaps）和带有物理内存保护（PMP）的简化RISC-V。此外，作者还利用为RISC-V with PMP形式化的安全保证验证了一个femtokernel。实验结果表明，该方法能够支持在存在对抗代码的情况下对安全关键软件进行非形式化和形式化推理，同时确保硬件实现与安全契约的一致性。该工作为建立高置信度的处理器安全基础提供了形式化工具和方法论。

该论文提出了一种结合大型语言模型（LLMs）与形式化方法的智能合约验证新框架。当前智能合约验证面临两大挑战：自然语言表达的属性内在存在歧义，且LLM的答案缺乏正确性保证。作者通过两个创新点同时解决这些问题：1）设计了一种扩展Solidity语言的正式规范语言，支持抽象类型，使得属性表达无歧义；2）开发了一个工作流，将LLM与类型检查和具体执行相结合，自动生成并验证违规见证（即反例）。其核心思想是将规范编码为包含存在量化抽象类型变量的Solidity测试；通过为这些变量实例化具体值（符合正确类型），测试将转换为可执行的反例（概念验证），直观展示属性为何被违反。作者将该流程实现为工具Neuroforger，并在来自文献的智能合约验证数据集上实验评估，获得了有前景的结果，证明了其在真实场景中的潜在适用性。本文适合对智能合约安全、形式化验证及LLM应用感兴趣的读者。

该论文针对形式化验证工具ProVerif和Tamarin在安全协议验证中的使用门槛问题，提出了一种系统化的、基于证据的安全属性分类法。通过系统综述2022-2025年间使用这两种工具的53篇近期研究，论文提取并整理了当前被实际验证的安全属性集合，将其分为多个类别并给出非形式化的直观定义，同时用一阶逻辑给出了严格的形式化定义以确保清晰性和一致性。此外，论文还提供了在ProVerif和Tamarin中建模这些属性的通用模式，并在开放仓库中收录了可执行的示例代码，从而弥合了理论安全属性定义与实际可执行验证模型之间的鸿沟。该工作有助于安全协议设计者（而非形式化验证专家）更便捷地使用形式化工具来表达和验证协议的安全需求，对推动形式化验证在安全社区的普及具有重要意义。

该论文对国际智能卡支付协议标准 EMV（全球超过90亿张卡片在使用）进行了系统性安全分析。研究背景是EMV标准长达2000多页的规范中存在难以发现的逻辑缺陷，此前已有若干安全问题被披露。核心方法是对EMV协议进行全面的符号化建模，使用先进协议验证工具Tamarin，首次实现对EMV旨在提供的所有相关安全保证的细粒度分析。通过自动化验证，论文发现了两类关键攻击：第一类攻击允许犯罪分子使用受害者的Visa非接触式卡片进行需要持卡人验证（如输入PIN）的高额支付，而无需知道PIN；研究者开发了概念验证安卓应用并在真实支付终端上成功演示。第二类攻击允许犯罪分子诱骗终端接受未经认证的离线交易，随后发卡行应拒绝该交易，但犯罪分子已携带商品离开（由于伦理限制，未在实际终端测试）。针对上述攻击，论文提出了改进方案，并利用模型验证了这些方案能阻止攻击且不影响已发行的卡片；改进只需在终端侧实施，无需更新卡片。该工作的主要贡献包括：首个支持EMV完整安全属性细粒度分析的符号化模型；自动化发现并验证两个关键攻击；提出并验证可落地的修复措施。适合协议安全研究者、支付系统开发者和标准制定者阅读。

该论文针对高保证密码学在 Spectre 推测执行攻击时代下的安全性问题展开研究。传统的高保证密码学方法通过程序验证和密码工程提供内存安全、功能正确性、可证明安全性和无时序泄露的机器校验证明，但这些保证通常建立在顺序执行语义之上。然而，现代处理器广泛采用推测执行以提升性能，而 Spectre 类攻击正是利用推测执行的漏洞。这引发了疑问：高保证密码学的安全保证在推测执行下是否仍然成立？本文通过实验证明，高保证密码学的优势可以扩展到推测执行场景，且仅带来轻微的性能开销。具体而言，作者基于 Jasmin 验证框架，提出了一种端到端的方法，用于证明密码软件在推测执行下的安全属性。该方法对 ChaCha20 和 Poly1305 两种算法进行了实现，生成了高效且功能正确的汇编代码，同时能够防御传统的时序攻击和推测执行攻击。实验结果表明，该方法的性能损失较小。论文的主要贡献在于：1) 首次系统地研究了高保证密码学在推测执行环境下的适用性；2) 提出并实现了一个可扩展的验证框架；3) 提供了实际可用的、经过形式化验证的密码实现。本文适合密码学实现者、安全研究员以及形式化验证领域的从业者阅读。

本文针对大型语言模型从有限生成引擎向具有广泛执行权限的智能代理转型过程中出现的失控问题，提出了一种基于逻辑推理基本局限性的新型安全范式。现有防御架构主要依赖经验性语义护栏和概率性大模型裁决器，无法在复杂语义符号解耦攻击下提供确定性安全下界。为克服这一困境，作者提出了一种可执行证明约束动作（ePCA）框架，采用神经符号隔离架构。该框架放弃对自然语言的语义信任，强制代理在执行物理操作前将其意图无损形式化为一阶逻辑数学约束，从而确保决策的可验证安全性。在宏观和微观二维动态对抗系统中的实验评估表明，该形式化验证机制在评估场景中实现了零攻击成功率和零误报率，且计算延迟极低。本文为构建未来智能系统的底层防御基础提供了在明确系统假设下的条件形式化基础和工程范式。适合AI安全研究员、大模型应用开发者及安全架构师阅读。

本文针对操作系统内核中 I/O 分离不足导致的安全问题，提出了一种形式化的 I/O 分离模型。该模型基于 I/O 传输授权定义分离策略，与具体硬件无关，能够防止恶意驱动通过操控设备绕过 I/O 隔离。作者在 Dafny 语言中对该模型进行了形式化规约、精化以及在 Wimpy 内核设计中的实例化验证，并自动生成了经过验证的正确汇编代码。通过形式化建模，发现了原 Wimpy 内核中先前未知的设计与实现漏洞。最后，论文概述了该模型在其他 I/O 内核上的适用性。本研究为高可信的 I/O 安全内核开发提供了理论基础和自动化工具，适合操作系统安全、形式化验证领域的研究者阅读。

该论文聚焦于Linux内核扩展程序eBPF的安全迁移问题。eBPF程序被广泛用于网络、可观测性及安全策略执行，但其内核验证器仅检查低级内存安全和终止性，未强制许多高级源级属性，如初始化规则、schema一致性或错误处理。作者识别出六类源级bug，这些bug能够通过编译和内核验证，但会导致数据静默损坏、将先前跟踪的事件泄露至用户空间，或产生错误的执行结果。其中，作者发现了十款开源eBPF程序中此前未报道的信息泄露：这些程序中的环形缓冲区或栈驻留事件记录会将完全可解码的先前跟踪事件（包括用户标识路径和足以恢复每个事件KASLR偏移的内核返回地址）泄露到用户空间。为加固这些被验证器接受的缺陷程序并支持安全迁移，作者提出了Heimdall——一个自动化流水线，利用大语言模型（LLM）将遗留的libbpf C程序翻译为基于Aya Rust的eBPF程序。Heimdall迭代修复编译和内核验证失败，通过静态分析安全引擎拒绝Rust-Aya中不安全的逃逸机制，并借助符号执行和Z3等价性检查逐程序证明翻译后程序与原始程序行为等价。在102个eBPF程序上的实验表明，Heimdall成功生成了96个经形式化验证等价（94.1%）的翻译版本。Heimdall是首个能够自动化地将生产级eBPF程序迁移到内存安全语言，并为每个翻译程序提供形式化保证保持可观测行为的系统。

本文介绍了首个基于机械化证明的后量子安全协议验证方法。作者提出了PQ-BC，一种针对量子攻击者计算安全性的计算一阶逻辑，并实现了对应的机械化支持工具PQ-SQUIRREL。该工作基于经典的BC逻辑及其在SQUIRREL证明器中的机械化实现。PQ-BC的发展需要使BC逻辑对单一交互式量子攻击者保持完备性。作者通过修改SQUIRREL，依赖PQ-BC的完备性结果并强制执行一组语法条件，实现了PQ-SQUIRREL证明器；此外，还提供了新的策略来扩展工具范围。利用PQ-SQUIRREL，作者进行了多个案例研究，提供了首个机械化的后量子安全性证明，包括两个通用的基于KEM的密钥交换构造、IKEv1和IKEv2的两个子协议，以及Signal的X3DH协议的一个后量子变体。此外，他们用PQ-SQUIRREL证明了几个经典的SQUIRREL案例已经具有后量子安全性。这项工作的贡献在于将形式化验证扩展到后量子设置，为安全协议的后量子安全性提供了自动化的推理工具。

该论文提出了Pramana，一个用于自治代理网络中的声明验证的协议层解决方案。在受监管领域中，自主代理对每个关键输出必须产生一个可审计的验证工件，记录声明内容、来源、执行者、时间和方式。当前的生产验证分为两个未标准化的方向：概率性判决模式（如自一致性投票、评审LLM集成）产生判断而非工件；而工件产生模式（如RAG、工具增强轨迹、生成器-验证器循环）产生特定于供应商的记录，外部审计员无法在不进行定制集成的情况下重构。Pramana定义了缺失的线路格式：每个关键代理输出被封装在一个类型化的ClaimAttestation中，包含四种变体（测量、推理、类比、引用），每种都配有针对记录源的verify()操作。对于测量声明和引用声明，verify()是确定性的；对于推理声明和类比声明，确定性则取决于预言机（在LLM支持下可审计重放）。这种四类分类源于古典印度认识论（pramana，有效知识的来源）。生命周期在TLA+中指定，并通过TLC在三个对称缩减模型上进行了全面验证：总共38,563个不同的可达状态，零个不变性违反。Python参考实现通过了84个测试。一个A2A和MCP的线扩展清单层叠了三个部署级不变性：可达性、SLA边界和离线可重新验证。一个探索性试点（n=100，2,275次评审调用）探讨了LLM作为代码生成中的评判者。最显著的观察是跨越语料库的40个百分点的原始FPR差异，与参考解决方案质量显著一致。该试点本身并不验证Pramana；结构论证和形式验证做到了这一点。

该论文针对大型语言模型（LLM）生成代码中可能引入安全漏洞的问题，提出了一种基于自然语言的规约与验证方法。传统形式化验证需要严格的规约语言，而现有利用LLM生成规约的方法效果有限。作者另辟蹊径，探索让LLM同时承担规约生成和组合验证的任务，且规约以自然语言表达。初步实验结果表明，该方法在小型基准测试中展现了潜力，能够通过自然语言描述的功能性规约，指导LLM验证代码实现的正确性，从而在代码生成阶段预防漏洞。论文属于初步研究阶段，尚未在大规模系统上验证，但为后续结合LLM与形式化方法提供了新思路。

本文首次对主密码保护的密码管理协议（M3PM）进行了系统性的形式化安全分析。密码管理器（PM）帮助用户管理登录凭证，缓解记忆大量密码的负担，而M3PM协议描述了客户端与PM服务器之间的交互：客户端使用主密码进行身份验证，服务器协助跨设备检索凭证。随着PM数据泄露事件频发以及用户对服务器滥用的担忧，确保服务器对主密码和凭证不知情至关重要。作者通过文档分析、流量分析和逆向工程等方法，从43个行业和学术界的PM中识别出事实上的M3PM协议。为了形式化M3PM协议的安全属性，他们在通用可组合（UC）框架内提出了一组理想功能。根据对手的知识类型，他们将针对主密码的离线猜测攻击分为四类。分析表明，43个PM中有38个至少易受一种离线猜测攻击，揭示了各种单主密码保护的M3PM协议在不同条件下无法抵抗此类攻击的情况。此外，他们还发现了一种预言机攻击，使被攻陷的服务器能够学习知名开源PM Passbolt的加密密钥，并证明1Password的双密钥机制为用户的主密码和凭证提供了强保护。

该论文提出了一种名为μCFI（微架构控制流完整性）的形式化验证方法，旨在解决现有控制流完整性（CFI）机制在微架构层面的安全漏洞。传统的CFI仅在软件或ISA（指令集架构）层面保证控制流安全，但无法抵御利用微架构侧信道或瞬态执行攻击（如Spectre、Meltdown）的控制流劫持。作者通过形式化建模微架构状态（如分支预测器、缓存、乱序执行单元）与控制流之间的关系，定义了微架构层面的安全策略。μCFI基于模型检验技术，能够验证处理器设计是否满足该策略，从而确保即使在微架构优化（如预测执行）下，控制流也不会被恶意操纵。实验在RISC-V处理器核心上实现，验证了多个已知攻击变种（如Spectre v1、v2）的缓解效果，并发现了新的潜在攻击路径。该工作首次将形式化验证应用于微架构CFI，为安全处理器设计提供了理论保证。

本文针对蓝牙低功耗（BLE）安全连接配对协议进行了形式化安全分析。研究团队构建了包含形式化模型、验证脚本和攻击实现的分析工具套件，对BLE Secure Connections配对协议的安全性进行系统性检验。通过形式化方法，作者揭示了先前未被发现的“PE混淆攻击”（PE Confusion Attack），该攻击能够绕过配对过程中的安全机制。论文详细描述了攻击的原理、利用条件以及对协议安全性的影响。实验验证了该攻击在实际BLE设备上的可行性，并提出了相应的防御建议。这项研究为BLE协议的安全性改进提供了理论依据和实用工具，有助于蓝牙标准制定者和实现者修复漏洞。

形式化验证是确保软件正确性和安全性的最高保证，但将其应用于大规模、不断演变的系统仍面临重大挑战。尽管大语言模型（LLM）在自动证明生成方面展现出潜力，但由于无法处理复杂的跨模块依赖关系或代码库及验证工具链的变化，它们在实际应用中常常失败。本文识别出根本问题在于语义-结构鸿沟：LLM基于语义代码模式进行操作，而形式化验证受刚性结构依赖约束，这种脱节导致脆弱且不可持续的证明。为弥合这一鸿沟，作者提出了一种自适应性验证的新范式，并实现了KVerus——一个面向基于Verus的Rust验证的检索增强系统，能够适应不断演变的软件环境。KVerus构建了包含代码元数据、引理语义和工具链细节的动态知识库，通过结合依赖感知的程序分析、语义引理索引和错误驱动的自我精化，它能够导航复杂的跨文件依赖来合成证明，并在面对常见的演化变化时自动修复证明。在三个单文件基准测试中，KVerus验证了80.2%的任务，优于当前最先进的AutoVerus（56.9%），并且在破坏性的Verus更新下退化更少。在三个具有跨文件依赖的仓库级基准测试中，KVerus实现了51.0%的成功率，而多轮提示基线仅为4.5%。最后，在Asterinas Rust操作系统内核中，KVerus生成了被上游接受的证明，验证了内存管理模块中23个先前未验证的函数（占证明代码的21.0%）。KVerus标志着向使现代安全关键软件的形式化验证成为可扩展且可持续实践迈出的重要一步。

本论文提出了一种面向自主网络防御的工具中介LLM架构（Stable Agentic Control），旨在解决现有方法无法为高对抗压力下的自主系统提供形式化保证的问题。研究背景源于安全运营中心（SOC）在敌对压力下配置端点检测与响应（EDR）策略的实际需求。核心方法包括：LLM代理使用确定性工具（如Stackelberg最佳响应、贝叶斯观测更新、攻击图原语）并操作有限动作目录，通过工具输出接口强制执行。作者利用Lean 4证明助理机器检查了一个复合Lyapunov函数（零sorry），证明了系统的可控性、从非对称传感器数据中的可观测性，以及对智能对抗扰动的输入-状态稳定性（ISS）鲁棒性，并给出两个推论将认证扩展到目录中的任何控制器或对手。在282个真实企业攻击图上，所有声明均有裕量成立。在成对攻击/防御遥测上，使用工具中介的Claude Sonnet 4控制器相比确定性贪婪基线将攻击者的预期收益（博弈值）降低了59%，且在四个温度下的40次运行中方差为零。使用Claude Haiku 4.5的控制器收敛到次优博弈值，但在额外40次运行中仍保持在目录边界内，表明架构稳定性不依赖于控制器能力。LLM的非确定性有助于创造性策略探索，而工具中介架构确保了系统稳定性。适合对自主防御、形式化验证、LLM应用安全感兴趣的研究人员和工程师阅读。

本文对FIDO2、CTAP 2.1和WebAuthn 2这一现代无密码认证协议族进行了形式化安全分析，并提出了后量子安全的实例化方案。研究者首先构建了这些协议的符号模型，涵盖了注册、认证、凭证管理等多阶段交互，并利用Tamarin Prover工具进行了自动化安全验证。分析揭示了在标准安全假设下协议能够满足预期的安全属性（如抗钓鱼、密钥泄露保护、绑定认证等），但发现了在特定场景下存在的设计缺陷，例如CTAP 2.1中某些消息序列可能导致不安全的凭证共享。基于这些发现，论文提出了两方面的贡献：一是给出了一个增强的、可证明安全的协议规范修正；二是引入了后量子密码原语（如基于格的签名方案），对协议进行了后量子安全实例化，并证明了其在量子计算机威胁下的安全性。实验评估表明，后量子实例化在性能开销上可接受，兼容现有硬件。该工作为大规模部署无密码认证提供了坚实的理论基础和工程指导。

本文对IETF QUIC协议记录层的安全性进行了系统研究。QUIC是传输层协议，其记录层负责数据包加密和头部保护，IETF标准第30版相比Google原始协议和早期草案有重大变化。作者首先提出了一种新的安全定义——带半隐式nonce的认证加密（AE with semi-implicit nonces），以精确刻画QUIC的隐私保护目标。他们证明QUIC使用的加密构造是通用构造的一个实例，该通用构造以标准AEAD安全方案和PRF安全密码为参数。通过形式化验证工具F*，作者对该构造进行了安全证明，并发现了短头部可塑性以及数据包计数器最低有效位数选择导致nonce机密性受限于特定弱点，进而提出了增强鲁棒性的改进方案。除安全模型外，作者还给出了记录层的具体功能规范，修复了草案中的多处错误后，证明了正确解密等关键功能的正确性。最后，他们实现了经验证内存安全、符合规范且具备安全属性的高性能记录层，吞吐量接近2 GB/s。面向防御者的价值在于：该工作为QUIC记录层的安全性提供了严格的形式化基础，揭示潜在设计局限并提出改进，有助于构建更安全的QUIC实现，并预防未来因实现错误或设计缺陷引发的攻击。

该论文提出了一种名为 SPECA 的基于规范锚定的安全审计框架。传统代码审计工具主要关注代码层面的漏洞模式，但对于由自然语言规范驱动的系统（如协议栈、共识实现、密码库等），其安全约束和正确性条件定义在规范中，代码级工具无法检测此类漏洞。SPECA 框架从自然语言规范中提取显式、类型化的安全属性，并基于这些属性通过结构化证明尝试推理来审计实现。该框架具备三种代码驱动审计所不具备的能力：规范依赖的检测、在共享属性词汇下进行受控的跨实现比较、以及可将误报分解为可解释的管道阶段可追溯的根因。实验部分，在 Sherlock Ethereum Fusaka 审计竞赛（366 个提交、10 个实现）中，SPECA 恢复了所有 15 个范围内的漏洞，并独立发现了 4 个被开发者确认的 bug。在 RepoAudit C/C++ 基准测试（15 个项目）中，SPECA 达到最佳公布精度（88.9%），并发现了 12 个超出已有 ground truth 的候选 bug，其中两个被上游维护者确认。多模型分析表明，能力更强的模型在属性范围内审计更忠实，将检测瓶颈从模型推理转移到属性生成质量。所有误报可追溯至三种根因：信任边界误解、代码阅读错误和规范解释错误，每种都提供了可改进的目标。

本文（系列第6篇）聚焦后量子密码学中基于NTT（数论变换）硬件的算术掩码组合安全性。布尔掩码的组合理论（NI、SNI、PINI）已成熟，但素数域上的算术掩码（NTT后量子密码的基础）缺乏类似理论。作者提出并形式化证明了素数域上PINI（Prime-Field PINI）的组合定理。核心见解是“更新参数”（renewal argument）：当在两个流水线阶段间施加新的随机掩码时，中间导线无论第一阶段的防护参数如何都会变得完全均匀。对于两个PF-PINI gadgets（参数k1和k2），经新鲜掩码组合的两阶段流水线满足PF-PINI(k2)，阶段1的多重性被完全消除。无新鲜掩码时，中间导线多重性可达k1，构成差分功耗分析的必要条件。作者在Lean 4中形式化了两个定理，包含18个机器检查的证明，零个“sorry”存根。他们还形式化地桥接了Barrett约简的代数模型与硬件忠实算术模型，并实例化定理以正式诊断微软Adams Bridge PQC加速器：其缺失阶段间新鲜掩码导致Barrett输出导线在一阶探针模型下非均匀，这一架构缺陷与三个独立实证分析一致。计算证据进一步表明“1比特屏障”在Barrett和Montgomery约简中具有普遍性。本文适合对后量子密码侧信道防护、形式化验证与硬件安全感兴趣的研究者阅读。