该论文提出了一种名为“乐观可验证声明”(Optimistic Verifiable Claim, OVC)的区块链协议，用于解决去中心化制造中的预签约僵局：服务提供商若不查看设计文件就无法准确报价，而消费者若分享设计文件则会暴露知识产权。OVC允许消费者发布关于隐藏设计的可验证声明（例如材料消耗量），提供商无需看到设计即可据此定价和投标。该声明在服务发布时提交，除非被选中的提供商质疑，否则一直有效；质疑会触发确定性的链上检查，揭露任何不诚实行为，设计仅在解决争议时披露，在诚实路径上从不公开。作者在Solidity中实现了四项检查（授权密钥访问、交付通道完整性、语法一致性、声明材料消耗），并在真实6.41 MB的G-code文件（3DBenchy）上，于以太坊、Arbitrum和opBNB三个网络上进行了测量。结果显示，每项服务无论是否发生争议，都需要承担发布加密设计的成本。对于3DBenchy，无争议结果在以太坊上花费7207美元（最多9小时），在Arbitrum上花费288美元（3分钟），在opBNB上花费2.87美元（2分钟）；完全争议结果在以太坊上花费49660美元（最多57小时），在Arbitrum上花费1988美元（19分钟），在opBNB上花费19.73美元（13分钟）。成本和时间随文件大小增长：对于50 MB的工业设计，无争议服务在以太坊上达到56173美元和最多3天，而在opBNB上仅为22.36美元和16分钟；完全争议在以太坊上达到488440美元和最多18天，而在opBNB上仅为195美元和1.6小时。四项检查中，材料消耗检查成本最高，其谓词在链上评估最昂贵。OVC使得基于声明的机密投标在Arbitrum和opBNB上经济可行，但在以太坊上无法实现工业规模。该研究面向区块链系统设计者、去中心化制造平台开发者以及对隐私保护投标机制感兴趣的研究人员。

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

现有的基于学习的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%。每次预测都附带结构化的修复报告，将每个判定转化为可操作的、函数级别的审计发现。该研究对智能合约安全审计、自动化漏洞检测工具开发具有重要参考价值。

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