本论文针对区块链智能合约的安全漏洞研究缺乏结构化真实数据的问题，基于公共 CVE 数据库构建了一个专门面向以太坊智能合约的漏洞数据集 CVE-Smart-Contracts。作者从 CVE 记录中筛选出截至 2026 年 7 月与以太坊智能合约相关的所有条目，并通过自动化流水线完成漏洞记录的检索、补充证据收集、记录与代码工件的对应关系验证、分类标签标注和函数级漏洞定位，过程中仅约 15% 的记录需要人工介入。为了保证数据集的可靠性，作者保留了所有外部输入数据，使得重新执行处理管线可以得到完全一致的输出。需要特别指出的是，该数据集并不对 CVE 中原始漏洞声明的真实有效性进行验证，而是仅从结构化和可复现的角度进行整理，同时将若干明显错误的记录标记为 'refuted'。最终数据集共包含 491 条与已部署合约相关的漏洞记录、26 条指向项目（主要是函数库）的记录、45 条因代码工件缺失或不可用而无法验证的记录，以及 6 条被驳斥声明的记录。每一个有效记录都提供了漏洞代码源码与运行时字节码、采用三种漏洞分类体系（如 CWE、SWC）的标签信息，以及具体到函数级别的漏洞位置。该数据集的主要用途是支持智能合约安全实证研究，特别是对已有漏洞代码分析工具、检测模型和自动修复技术进行统一评估与横向对比。通过本数据集，研究者可以更真实地检验工具在现实漏洞案例上的表现，也便于开展漏洞模式、漏洞分布和智能合约代码质量方面的量化分析。

该论文针对安全代币（Security Tokens）标准中监管操作语义不明确的问题，提出了一种机械化（machine-checked）的参考执行语义。安全代币标准通常暴露特权转移、冻结、恢复和合规机制，但机制本身并不标识其执行的法律效果或附带的证据与撤销义务。作者在 Isabelle/HOL 中形式化定义了 ERC-8319 中提出的六种监管行动：FREEZE、SEIZE、CONFISCATE、LIQUIDATE、RESTRICT 和 RECOVER。模型区分了应用（applied）、拒绝（rejected）和操作失败（operational-failure）三种结果，并机械化验证了撤销（reversal）、重放（replay）、纪元（epoch）、框架（frame）、案例局部终态（case-local terminality）和收据（receipt）等性质。构建过程中没有未证明的占位符或额外公理。论文证明了外部事实边界：两个在所有权、结算和权益上存在分歧的具体世界会产生相同的核观察结果，因此这些外部事实不能从受限输入中建立。通过构造性见证和直接变异展示了可达性和故障集的伪造（falsification）。针对一个 ERC-TRUST Solidity/EVM 候选实现，论文分别报告了 Foundry、Certora、Kontrol/KEVM、变异测试、确定性构建和运行时身份的证据。当前发布概况满足全部 7 个证据包、49 个 Core 和 24 个强制性 Supporting 义务，且无部分学分；6 个可选义务未声明。在固定运行时前提下，机械化抽象关系被证明是唯一且函数的，包和行推论从哈希绑定证书产生条件性的、概况范围的细化定理。作者明确声明，这些结果并不构成完整的 Isabelle 到 Solidity 到 EVM 的细化定理、编译器正确性、审计、生产就绪或部署验证。其贡献在于一种机器检查的领域语义，以及一张可证伪的地图，说明对于受监管代币执行标准，什么是已证明的、什么是有界证据、什么是假设的、什么是开放的。该研究面向智能合约形式化验证、安全代币标准和监管科技领域的研究者与工程师。

本文针对加密资产领域争议解决的困境展开研究。随着加密资产广泛使用，相关争议频发，然而传统法律救济机制难以适应其去中心化、跨境及法律规则碎片化等特点。特别是缺乏法律和技术专长的用户，往往难以识别自身权利、组织证据并寻求有效救济，从而加剧数字排斥现象。为此，作者提出一种融合人工智能与区块链智能合约的混合在线争议解决（ODR）框架。在该框架中，AI主要在链下运行，负责自然语言交互、争议分类、证据组织以及提供通俗易懂的法律信息；智能合约则承担有限的链上功能，包括争议登记、时间戳、验证、托管管理以及在适宜场景下执行协商结果。整个框架强调以人为中心，注重可解释性、程序指引和复杂案件中的人类监督。文章通过加密资产扣押、交易所失败和跨境诈骗三类争议案例对该模型进行剖析，认为只要明确划分自动化与人工角色的边界，混合架构就能提升可访问性、透明度、效率和可执行性。同时，论文还探讨了算法偏见、责任归属、数据保护、智能合约可执行性以及遵守欧盟《人工智能法案》和《加密资产市场监管条例》等法律治理问题。最终，该研究为加密资产环境中更具包容性和健壮性的争议解决机制提供了法律根基和设计蓝图，适合法律科技、区块链治理及数字权利保护领域的研究者和从业者阅读。

动态频谱共享（DSS）是下一代无线系统的关键，但现有方案如频谱接入系统（SAS）依赖集中式管理员，暴露敏感操作元数据且缺乏加密交易问责性。尽管SAS管理员（如Google）引入了按需付费定价模型，但随着DSS向更开放和大规模的频谱市场演进，这些方法仍面临隐私和问责挑战。本文提出SpexPay，一个隐私保护且可审计的按需付费频谱使用框架，能在不泄露用户身份的情况下实施细粒度、与使用量挂钩的支付。SpexPay集成BBS+可验证凭证、不可链接会话假名和选择性披露证明，实现隐私保护访问授权，同时利用基于Solidity的智能合约实现自动且不可否认的托管结算。系统仅在链上记录假名使用证据和哈希链计量数据，实现强不可链接性，同时保持可验证的问责性和可审计性。完整原型展示了低端到端延迟（约150毫秒）和适中的链上成本（约603K gas或约0.9美元），表明SpexPay在实际DSS部署中是可行的。还在Raspberry Pi 5上评估了用户端密码操作，以评估可扩展性和对边缘级硬件的适配性。代码和工件公开可用。

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