本文提出了首个经过机器检查的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上获取。

以太坊智能合约的重入漏洞曾导致重大经济损失，为此社区开发了多种自动化重入检测器。然而，这些检测器由于检测规则粗糙，频繁产生大量误报，常将受抗重入模式保护的合约误判为存在漏洞。因此，迫切需要开发专门的自动化工具来辅助检测器准确识别抗重入模式。现有代码分析技术虽在特定任务上有潜力，但在识别抗重入模式时仍面临挑战，主要因为抗重入模式的特征复杂多样，且缺乏对这些特征的先验知识。本文提出 AutoAR，一种自动化识别系统，用于探索和识别以太坊合约中常见的抗重入模式。AutoAR 利用专门的图表示 RentPDG，结合数据过滤方法，从大量合约中有效捕获与抗重入相关的语义。基于提取的 RentPDG，AutoAR 采用集成图自编码器和聚类技术的识别模型，专门用于精确识别抗重入模式。实验结果表明，AutoAR 能以 89% 的准确率辅助现有检测器识别 12 种常见抗重入模式；集成到检测流程后，误报率降低超过 85%。该工作为智能合约安全分析提供了新的思路，有望提升重入漏洞检测的精度，减少人工审计负担。