本文研究去中心化自治组织（DAO）中治理权力的行使机制及其安全影响。DAO 是一种通过智能合约管理区块链协议的治理实体，其治理合约明确规定了利益相关者如何提出、表决和执行协议变更。作者指出，治理合约的设计选择对 DAO 及其管理的智能合约的安全性和隐私性具有深远影响，不当设计可能引入关键漏洞。论文首先阐述了实现 DAO 时设计选择带来的信任与透明度权衡；其次，通过真实案例强调了糟糕的设计选择如何导致严重漏洞。为此，作者分析了 48 个公开且活跃的基于以太坊的 DAO，这些 DAO 控制着大量资本。他们将设计选择分类为几个关键维度，简洁地描述了 DAO 利益相关者如何发起协议变更、投票以及根据投票结果执行变更。分析揭示了一类新型攻击——治理攻击，这类攻击直接利用 DAO 治理机制的基本设计缺陷，即使智能合约实现无 bug 也无法避免。文章的核心贡献在于系统化地分类 DAO 治理设计选择，并提出治理攻击的概念，为 DAO 安全研究提供了新视角。适合区块链安全研究者、DAO 开发者和智能合约审计人员阅读。

本文是DeFi '24研讨会的会议报告，聚焦于去中心化金融（DeFi）及其安全性问题。研讨会汇集了学术界和工业界的研究人员，旨在探讨DeFi生态系统中的新兴安全威胁、漏洞模式、攻击案例以及防御机制。主要讨论主题包括：智能合约漏洞（如重入攻击、闪电贷攻击、预言机操纵）、经济安全（如MEV、套利策略）、跨链桥风险、以及去中心化治理安全。此外，还涉及了形式化验证、运行时监控和异常检测等安全分析技术。会议强调了DeFi安全面临的独特挑战，例如代码不可变性与经济激励的复杂交互。该报告为DeFi安全社区提供了当前研究方向和关键问题的全面概述。

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

该论文提出了 DeFiScreener，一种基于历史攻击案例匹配的高效 DeFi 攻击预筛查框架。背景：截至 2026 年 1 月，已有超过 5,200 个 DeFi 项目部署在主流区块链上，但现有检测工具通常仅覆盖特定攻击类型，检测覆盖范围严重不足。核心观察：作者发现一种称为“危险时间不对称”的现象，即攻击者在时间上倾向于利用某些特定函数调用模式。基于此，DeFiScreener 通过以下步骤实现预筛查：首先，从目标项目的完整源代码中构建函数调用树（FCT），并使用大语言模型（LLM）为每个函数生成语义嵌入，融合程序结构和函数意图。然后，实施双层筛查：函数层将函数嵌入与历史攻击函数库中的攻击模式进行匹配；序列层利用提出的基于攻击模式的蒙特卡洛树搜索（APO-MCTS）高效探索 FCT，筛选出易受攻击的调用序列。最后，将候选结果传送给 LLM 进行进一步解释和安全分析。实验基于 207 个真实世界 DeFi 攻击事件的数据集，结果显示 DeFiScreener 在攻击预筛查中达到了 98.55% 的召回率和 84.30% 的精确率。该方法显著扩展了检测覆盖范围，为 DeFi 智能合约的自动化安全审计提供了新的思路。

该论文针对以太坊非同质化代币（NFT）智能合约中的漏洞检测问题，提出了一种结合漏洞导向代码切片、ERC-721 知识库和受限大语言模型（DeepSeek）分析的方法。研究背景是：现有静态分析工具（如 Slither、Mythril）基于规则高效，但难以处理特定应用逻辑；而自由形式的大模型分析可能被无关代码干扰或输出不一致。作者通过正则表达式模式定位重入、整数溢出/下溢和时间戳依赖等漏洞的候选语句，利用结构感知的上下文窗口算法提取带行号的代码切片，然后让 DeepSeek 基于显式决策规则和固定输出模式分析每个切片，最后支持自动批量处理。在 450 个 NFT 合约样本上，完整配置产生了 437 个阳性标签（阳性率 97.1%）；去除外部知识库后阳性率降至 87.11%；分析完整合约（无知识库）则降至 73.78%。实验表明，聚焦的代码上下文和领域约束显著影响检测器的输出效果。该方法为智能合约漏洞检测提供了一种结合专家知识与大模型能力的新范式，适用于安全审计人员和研究机构。

该论文研究了区块链智能合约中依赖外部报告的问题。现有机制在安全性与性能之间存在权衡：依赖少量受信报告者会引入中心化风险，而允许开放报告则导致链上报告数量过多。作者指出，根本原因在于对称奖励设计，即对所有报告一视同仁。论文证明，任何对称奖励机制都无法克服这一权衡。为此，他们提出了 Prrr（Personal Random Rewards for Reporting）协议，该协议为报告分配随机的、非统一的奖励值，引入了一种新型机制设计概念——事前合成不对称性（Ex-Ante Synthetic Asymmetry）。据作者所知，Prrr 是第一个有意构建参与者不对称性的博弈论机制（在任何领域中）。Prrr 采用类似第二价格拍卖的结算方式分配奖励，确保激励兼容性，并同时实现安全性和效率。遵循该协议构成子博弈完美纳什均衡，能够抵御合谋和女巫攻击。Prrr 适用于众多依赖及时报告的智能合约。

本文提出Jigsaw系统，旨在实现双重隐私保护的智能合约，即同时保护合约的输入数据和合约逻辑（代码）的隐私。传统的智能合约在区块链上公开执行，导致交易数据和合约代码对所有节点可见，存在隐私泄露风险。Jigsaw结合了安全多方计算（MPC）和零知识证明（ZKP）等密码学技术，设计了一种新的协议，允许合约参与方在不泄露各自输入和合约逻辑的情况下协同执行计算，并验证结果的正确性。系统架构采用分片（sharding）和秘密共享机制，将合约状态分割成多个秘密份额，分布在不同节点上，任何单个节点无法获取完整信息。实验评估表明，Jigsaw在以太坊测试网络上运行具有可接受的性能开销，相比现有完全同态加密或MPC方案，在延迟和吞吐量方面有所优化。本文的主要贡献在于提出了首个同时满足输入和代码隐私的智能合约系统，并给出了形式化安全证明和原型实现，为区块链隐私保护研究提供了新的方向。

本文提出了一种名为 KASS（知识增强攻击合成与仿真）的多智能体框架，旨在解决现有智能合约安全工具仅停留在漏洞检测、无法验证漏洞可利用性及攻击过程的问题。KASS 将自动利用生成分解为规划、生成和测试三个阶段，并融合三种互补机制：基于检索增强的现实审计知识规划、将攻击计划绑定到可执行概念验证测试的形式化生成与验证约束，以及修复代码级错误并在攻击假设失败时触发策略级重规划的分层双循环优化过程。评估在包含 104 个合约的 SmartBugs-Curated 数据集上进行，涵盖四种漏洞类型。结果显示，KASS 对 94.23% 的测试合约成功生成了可执行利用，该比率高于先前 REX 和 AdvSCanner 在类似子集上的报道结果，也高于同等评估协议下复现的 Claude Code 基线。在 11 个真实世界 CVE 标记合约上，KASS 成功验证了 9 例。除生成利用外，KASS 还输出结构化攻击计划，记录利用流程、量化潜在资产损失，并可作为静态分析工具的语义误报过滤器。该工作为蓝队和审计人员提供了自动化验证漏洞可利用性的能力，有助于区分真实威胁与误报。

传统智能合约在区块链上执行的成本高昂，尤其是在以太坊等平台上，随着费用飙升，复杂应用变得不切实际。链下执行是一种有前景的解决方案，但现有方案存在诸多缺陷，如昂贵的区块链交互、缺乏数据隐私、资本成本高（因需要锁定抵押品）或仅支持有限的应用场景。本文提出了一种实用的链下智能合约执行协议POSE（Practical Off-chain Smart Contract Execution），通过利用可信执行环境（TEE）池高效执行计算，并能够快速从意外或恶意故障中恢复。POSE提供了强大的安全保证，即使大量参与方被攻破也能保持安全性。作者对概念验证实现进行了效率和有效性评估。该协议适用于需要高吞吐量、低成本和隐私保护的智能合约应用场景，如金融产品、拍卖和游戏等。

该论文针对以太坊上最流行的智能合约编译器——Solidity编译器中的误编译漏洞（miscompilation bugs）进行了系统性的发现与分析。智能合约编译器的正确性对于保证区块链上不可篡改的开源代码的正确执行至关重要。作者开发了SolSmith，一种语义感知的差分模糊测试工具，在三年内持续检测Solidity编译器，发现了25个未被发现的误编译漏洞，其中一些已存在多年。SolSmith通过生成有效的测试程序，压力测试编译器的代码生成和优化组件，从而发现常规测试无法捕获的缺陷。论文的贡献包括：1）使编译器测试更加严格，减少因编译器错误导致的智能合约缺陷；2）对发现的误编译漏洞进行了定性和定量分析，按其性质、根本原因和最终用户影响进行分类，揭示了优化编译器的一些常见陷阱。该研究对于提升Solidity编译器的可靠性和安全性具有重要意义。

本文提出了 Crossroads，一个用于链抽象资产的智能合约层。在 Crossroads 中，来自几乎所有链的资产都在单个后端区块链上以 ERC-20 代币的形式表示。因此，任何资产都可以在单一统一平台上参与基于智能合约的交换、借贷或隐私应用。虽然 Crossroads 提供了跨链桥接功能，这是当前缓解区块链生态系统碎片化的一种常见部分方法，但这只是 Crossroads 通用链抽象模型中的一项服务。Crossroads 依赖于密钥加密：一个门限签名委员会持有加密密钥，控制着每个集成链上的资产，仅在后端区块链上的智能合约授权时才签署交易。资产移动具有费用效率，因为所有权变更记录在后端区块链上，用户可以为提款设置交易费用。Crossroads 使用可插拔的预言机（zkBridge、基于 TEE 的、混合的）实现了新区块链的无许可、模块化集成，并具有灵活的设计选项。存入 Crossroads 的资产受益于强大的、特定链的最终性保证，最大限度地降低了重组攻击的风险。然而，与现有桥接器不同，Crossroads 中的第三方智能合约可以在最终性完成之前提供快速的乐观资产访问。作者证明了 Crossroads 满足可靠性：给定一个诚实的签名委员会成员法定人数，任何用户都可以单方面生成一笔提款交易，将其净余额转移到集成链上的一个账户。作者在多个公共区块链（比特币、以太坊和 Solana）上实现了概念验证。他们还列举了 Crossroads 支持的一系列应用，包括通用钱包、跨链质押和借贷、隐私保护支付以及公共区块链资产的私有管理。

该论文提出 EvoVuln，一个自动生成智能合约漏洞检测程序化知识的框架。现有基于大语言模型（LLM）的方法存在局限：基于提示的方法依赖人工设计的检测规则，而微调则需要大量标注样本，这在智能合约领域难以获取。EvoVuln 将漏洞检测重新定义为程序化知识进化问题，仅需极少量标注样本即可合成并精炼检测逻辑。其核心机制包括两个部分：一是运行时反转控制（IoC）架构，将检测规则编译为可执行策略，严格解耦确定性控制流与 LLM 语义推理，确保忠实遵循逻辑并产生密集的诊断遥测用于精确定位错误；二是两阶段进化流水线，通过溯因语义调试在没有参数更新的情况下精炼规则：冷启动阶段利用自动生成的边缘案例初始化并压力测试初始规则，少样本进化阶段仅使用每种漏洞类型 5 个漏洞样本和 5 个安全样本将策略锚定到真实世界语义。在五种真实漏洞类型上的评估显示，EvoVuln 达到 71% 的宏平均 F1 分数，优于所有基线。进化得到的程序化知识可跨模型迁移：使轻量低成本模型超过更大的零样本模型 19 个百分点，且无需重新训练即可迁移到其他 LLM，单次进化成本低于 50 美元。该研究适合安全研究员、智能合约开发者及 LLM 应用开发者阅读。

该论文提出了一种基于语料库驱动的以太坊智能合约反编译方法，名为Code HarvETHter。反编译是以太坊安全分析的关键步骤，因为智能合约通常以字节码形式部署，难以直接分析。现有的反编译工具往往依赖于静态规则或模式匹配，存在精度低、可移植性差等问题。本文的创新点在于利用大规模智能合约字节码语料库来训练或指导反编译过程，从而自动学习字节码与高级语言结构之间的映射关系。该方法首先从公开的区块链数据集中收集大量已验证的智能合约字节码及其对应的源代码（如有），构建配对语料库。然后，设计了一种基于序列到序列学习的神经网络模型（或类似方法），将字节码序列映射为伪源代码。此外，论文还探讨了如何利用控制流和数据流分析来增强反编译结果的语义正确性，例如识别函数边界、变量类型和数据结构。通过在一个包含2000多个真实以太坊智能合约的数据集上进行实验，与现有工具（如Porosity、Vandal、Rattle）相比，Code HarvETHter在函数识别准确率、类型恢复和反编译代码的可读性方面均有显著提升。该研究对于智能合约安全审计、漏洞检测以及恶意合约分析具有潜在价值。

智能合约是区块链上执行各种商业活动的软件程序。近年研究发现了一类新的“机器不可审计”漏洞，它们源于源代码未能满足底层交易上下文。现有检测方法需要人工理解交易逻辑并手动推理不同上下文来源（即模态），例如代码和描述预期交易行为的自然语言。为了自动化检测这类漏洞，本文提出了SmartInv，一个准确且高效的智能合约不变量推断框架。核心洞见在于，智能合约的预期行为（通过不变量指定）依赖于跨模态信息的理解和推理，如源代码和自然语言。作者提出了一种新的基础模型微调和提示策略——Tier of Thought (ToT)，用于在智能合约的多个模态间进行推理并生成不变量。SmartInv随后通过检查这些生成不变量的违反情况来定位潜在漏洞。实验评估基于过去2.5年（2021年1月1日至2023年5月31日）导致财务损失的真实世界智能合约漏洞，结果表明SmartInv能生成有效不变量，准确定位“机器不可审计”漏洞，共发现119个零日漏洞。从中采样了8个漏洞报告给相应开发者，其中6个被迅速修复，5个被确认为“高严重性”。该研究展示了利用多模态大模型自动推理智能合约安全性的可行性和有效性。

该论文提出了CyberChainBench，一个用于评估基于大型语言模型（LLM）的智能合约安全代理的基准测试。基准测试涵盖三个互补任务：漏洞检测、利用生成和补丁合成。它基于来自DeFiHackLabs的541个真实世界利用事件构建，跨越9个EVM兼容链。每个案例锚定到特定区块，包含结构化真实数据（漏洞类型、定位、攻击者利润）。代理通过Harbor编排的隔离评估环境与历史区块链状态交互，使用工具读取代码、追踪交易并在主网分叉上验证利用。利用按历史分叉上的经济影响分级；补丁通过在可代理升级的子集上重放历史攻击和合法交易作为失败测试预言机进行验证。论文定义了五类漏洞分类法，并评估了多种代理-模型配置。结果显示明显难度梯度：最佳配置在检测上得分37.5%，利用上43.7%，但补丁上仅23.4%。顶级代理（Codex with GPT-5.5）在200个利用案例中实现总计5740万美元的利用利润，每个案例成本2.39美元。该基准为智能合约安全研究提供了标准化评估平台，揭示了当前LLM代理在自动化安全任务中的能力与局限。适合安全研究员、智能合约开发者和AI安全交叉领域从业者阅读。

本文提出Zapper，一个旨在为智能合约提供数据和身份隐私保护的系统。在区块链环境中，智能合约的执行数据通常对所有节点公开，这导致敏感信息（如交易金额、用户身份）面临泄露风险。Zapper通过集成先进的密码学技术（如零知识证明、同态加密或安全多方计算），实现合约状态的加密存储与计算，同时允许验证者在不泄露具体数据的情况下确认合约的正确执行。此外，Zapper还支持匿名认证机制，隐藏交易参与方的身份，从而增强用户隐私。该工作可能设计了一套新的编程模型或编译器，使开发者能够便捷地编写隐私保护智能合约，并在以太坊等平台上部署。实验评估可能展示了其在计算开销、交易成本和可扩展性方面的权衡。该研究对区块链隐私保护领域具有重要参考价值，尤其适用于金融、供应链和身份管理等对隐私敏感的应用场景。

该论文提出了 GiANT 自动化框架，旨在解决智能合约审计数据集构建中的人工可扩展性瓶颈以及数据粒度和多样性不足的问题。GiANT 采用分治策略结合思维链技术，从 Code4rena 平台上的真实审计报告中提取结构化漏洞信息，并通过 LLM 作为裁判机制进行严格的质量保证。研究者在 388 份真实审计报告上运行 GiANT，生成了包含 7,711 个漏洞发现、覆盖五个严重级别的 GiAnt Corpus 数据集。手动评估显示信息提取可靠性极高，平均质量得分 4.76/5，评分者间一致性 κ=0.88。进一步，他们使用该数据集对四个最先进的 LLM 在漏洞检测、代码摘要、缓解建议和自动 Gas 优化任务上进行基准测试，建立了性能基线，为自动化智能合约审计的未来研究提供了宝贵的数据基础。

现有的基于学习的Solidity智能合约漏洞检测器通常将检测简化为单函数内的语法模式匹配，但许多重大利用（如The DAO、Cream Finance）并不存在于单个函数中，而是存在于函数间的关系以及使攻击可行的条件组合之中。为此，本文提出AttackPathGNN，一种将检测重新定义为对显式攻击路径推理的图神经网络（GNN）。其两个架构创新区别于先前的GNN检测器：（1）状态干扰图（State Interference Graph），该图通过带类型和权重的边以及由显式五条件谓词定义的有向重入路径边，连接共享可变存储的每对函数；（2）合取池化（conjunction pooling），一种对八个命名利用前提条件的可微AND聚合器，其log-sigmoid形式使得当任一缓解措施（如重入守卫、访问控制修饰符或SafeMath）到位时，每个函数的利用评分会骤降。在五个独立训练运行中，AttackPathGNN在SmartBugs Wild保留测试集上达到92.3±0.2%的F1分数（假阴性率4.3±0.3%，在独立人工标注的SmartBugs Curated基准上检测率90.8±2.5%），并在每个种子上以100%恢复6/10个DASP10类别，重入检测达到98.7±1.8%。每次预测都附带结构化的修复报告，将每个判定转化为可操作的、函数级别的审计发现。该研究对智能合约安全审计、自动化漏洞检测工具开发具有重要参考价值。

该论文提出了Bastet，一个面向去中心化金融（DeFi）智能合约漏洞检测的细粒度专家标注数据集。2024年，DeFi协议因智能合约漏洞累计损失超过14.9亿美元，基于大语言模型（LLM）的漏洞检测成为有前景的应对方案，但现有评估数据集存在三大问题：基于过时的Solidity版本（如v0.4），无法反映现代DeFi合约；依赖自动化或LLM生成的标注，引入幻觉导致的标签噪声；采用粗粒度的单层标签，难以捕获真实业务逻辑漏洞的语义复杂性。Bastet通过以下方式解决这些问题：数据来源为2021-2024年的真实审计发现；由人类专家通过讨论达成共识进行标注；采用两层分类体系，包含46个标签和77个子标签。数据集包含从394份Code4rena竞争性审计报告中收集的4,402个发现（时间跨度为2021年4月至2024年11月），其中849个发现由DeFiHackLabs社区的白帽安全研究人员完全标注。所有标注均通过双标注者共识工作流程生成，确保了基于真实漏洞根因的标签准确性。该数据集的主要贡献在于：提供高质量、精细化的基准，以推动LLM在DeFi安全领域的应用研究，并促进可复现的实验评估。适合智能合约安全研究人员、LLM应用开发者及DeFi协议审计人员阅读。

本文提出了一种名为ESCORT的深度学习框架，用于检测以太坊智能合约中的多种漏洞类型。传统检测方法通常只针对单一或少数漏洞类型，且扩展到新类型时需要大量重新设计。ESCORT采用通用特征提取器学习合约字节码的通用语义，并针对每种漏洞类型设置独立分支，实现多标签分类，可同时检测多个漏洞。更重要的是，ESCORT利用迁移学习，当出现新的漏洞类型时，只需在预训练的特征提取器上添加新分支，并用少量数据微调即可，避免了重新训练整个模型的开销。实验基于361万个真实智能合约数据集，初始阶段在六种漏洞类型（如重入、时间戳依赖等）上平均F1分数达98%；迁移学习阶段对另外五种新漏洞类型平均F1分数达96%。与现有非机器学习工具相比，ESCORT可处理任意复杂度的合约，实现100%合约覆盖，并支持多漏洞并发检测，显著缩短检测时间。该研究是首个将迁移学习应用于智能合约漏洞检测的深度学习框架，并将开源数据集和标注工具链以促进后续研究。

该论文提出了一种轻量级的智能合约安全审计框架，利用经过蒸馏和聚合的开放源码大语言模型（LLM）来应对现有基于LLM的审计方法存在的计算开销大、缺乏严重性评估以及可操作修复建议等问题。框架将审计任务解耦为四个独立模块：漏洞检测、漏洞解释、严重性分类和修复建议。通过采用秩稳定低秩适配器（rsLoRA）、知识蒸馏以及定制的链式验证（CoVe）聚合策略，模型在保持高精度的同时显著降低了参数量（0.6B-4B参数）。实验表明，该轻量级流水线在漏洞检测上达到98.25%的准确率，在生成解释任务中对齐得分为0.4375，优于参数量7B-34B的密集编码器LLM。消融实验验证了解耦审计流程相比统一提示的优势，并发现了新颖的严重性中心偏差，为未来LLM辅助审计研究建立了基准。

该论文提出了一种名为 Unicity 的代币所有权模型的泛化版本，将传统简单的所有权条件扩展为可编程的支出条件，称为“谓词”（predicates）。这些谓词允许在链下执行类似智能合约的功能，而无需共识参与者（如矿工或验证者）直接执行，而是由依赖方（如交易接收者）自行验证。作者证明，Unicity 执行层的安全属性可以归约到谓词族不可伪造性（predicate family unforgeability），从而保证了在添加可编程条件后，系统的安全基础不受损害。为了展示该模型的实用性，论文详细描述了如何利用谓词实现无信任的原子交换（atomic swap），即两个互不信任的参与方在不依赖第三方中介的情况下安全交换代币。原子交换的实现通过构建特定的谓词条件，使得交易要么全部执行，要么全部回滚，避免了部分执行的风险。该研究为区块链和去中心化金融领域提供了一种新的链下智能合约范式，降低了链上计算和存储开销，同时保留了安全保证。

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

智能合约反编译旨在从字节码恢复高级语言源代码，但现有评估方法存在数据集狭窄、指标不一致、语义一致性检查有限等问题。随着大型语言模型（LLMs）开始生成看似合理但语义可能偏离原始合约的Solidity代码，这一问题变得日益重要。本文提出SCDBench，一个基于LLM的智能合约反编译器数据集和评估基准。数据集包含600个真实Solidity合约，配有其字节码输入、真实源代码和可重放的语义检查点。SCDBench通过四个递进阶段评估反编译输出：格式完整性、可编译性、应用程序二进制接口（ABI）恢复以及通过差分重放实现语义一致性。作者在零样本反编译设置下评估了Claude Opus 4.7、GPT-5.3-Codex和GLM-5（包括有无扩展推理的变体）以及零样本编译修复设置。结果表明，前沿LLM通常能生成结构清晰且可编译的Solidity代码，但实现语义一致性仍远未解决：最佳模型仅完美反编译42/600个合约。进一步实验表明，引入同模型编译修复以适度成本显著提升了性能。SCDBench为严格且可重复的评估建立了共同基础，旨在加速开发用于区块链安全与透明性的可靠智能合约反编译器。

该论文针对基于大型语言模型（LLM）的静态分析在智能合约安全开发中的可靠性和局限性进行了系统基准测试。研究背景是区块链交易的不可逆性使得智能合约漏洞检测成为安全开发的必备环节，而LLM虽被越来越多地集成到开发者工作流中，其作为自主安全审计工具的可靠性尚未得到证实。研究者评估了当前生成模型能否替代传统的静态分析工具，或仅作为其补充。实验发现，LLM的效果受到词汇偏差和缺乏外部数据输入严格验证的削弱，这种对非语义启发式（如标识符命名）的依赖导致高误报率。此外，不同的提示技术在精确率和召回率之间呈现权衡。研究结果基于自定自动化框架得出，该框架在分类模型输出时达到了92%的准确率。论文核心贡献在于量化了LLM在智能合约漏洞检测中的局限性，并提出混合解决方案的可能性。适合安全研究人员、智能合约开发者以及LLM应用开发者阅读。

本文提出了一种基于大语言模型（LLM）的智能合约漏洞检测框架。智能合约因其不可篡改特性，易遭受多种安全漏洞攻击，导致重大经济损失。现有检测方法通常依赖人工制定的专家规则，缺乏对不同漏洞类型的灵活适应性。为此，作者构建并公开了一个大规模数据集，包含来自15个主流区块链平台、超过3200个真实项目的31165个专业标注的漏洞实例。该框架利用基于抽象语法树（AST）的精确上下文提取和漏洞特定的提示设计，为13种常见漏洞类型实例化定制检测器。实验结果表明，该方法平均正样本召回率达0.92，平均负样本召回率达0.85，展示了精心设计的上下文提示在实现可扩展、高精度智能合约安全分析方面的潜力。该研究为智能合约安全检测提供了新的思路，特别适合安全研究人员和区块链开发者关注。

本文提出 GoAT-X 框架，旨在解决跨链桥合约安全审计中的语义复杂性问题。跨链桥作为多链生态的关键基础设施，因实现缺陷已造成超过28亿美元损失。现有防御手段如字节码级静态分析难以处理跨链交互的语义复杂度，而基于大语言模型（LLM）的方法虽能理解源代码，但在复杂多合约依赖上容易出现幻觉推理。GoAT-X 将审计过程建模为“审计思维图”（Graph of Auditing Thoughts），模仿人类专家分解、推理和验证安全逻辑的方式。通过将LLM推理锚定在静态提取的数据流上，并将抽象安全属性显式链接到具体代码实现，该框架将语义约束在良定义的结构和状态边界内。在此受限空间中，GoAT-X 将跨链逻辑中的缺失约束和对抗绕过路径作为首要漏洞目标，动态探索推理路径以识别可被利用的语义鸿沟。在涵盖所有已知跨链代币交易攻击的综合基准测试中，GoAT-X 在细粒度审计点上达到92%的召回率，对存在漏洞的项目覆盖率达95%，并在实际场景中识别出117个经确认的风险，且运营成本较低，为可扩展的、逻辑驱动的跨链安全审计建立了新标准。