以太坊智能合约的重入漏洞曾导致巨大的经济损失，为此社区开发了多种自动化重入检测器。然而，这些检测器因检测规则过于粗糙而频繁产生大量误报，常将已采用防重入模式（如互斥锁、检查-生效-交互模式等）保护的合约误判为存在漏洞。现有代码分析技术在识别这些防重入模式时面临挑战，主要原因是防重入模式的特征复杂且多样，且缺乏对这些特征的先验知识。本文提出 AutoAR，一个自动化识别系统，用于探索和识别以太坊合约中普遍存在的防重入模式。AutoAR 利用一种专门的图表示 RentPDG（Reentrancy Protection Dependency Graph），结合数据过滤方法，从大量合约中有效捕获与防重入相关的语义信息。基于从合约中提取的 RentPDG，AutoAR 采用一个集成图自编码器与聚类技术的识别模型，专门用于精确识别防重入模式。实验结果表明，AutoAR 能够帮助现有检测器识别 12 种常见的防重入模式，准确率达到 89%；将其集成到检测流程后，误报率降低了超过 85%。该工作为提升智能合约安全检测的准确性提供了有力工具。

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