本文提出了 EVM bytecode 的第一个完整的小步语义，形式化验证了这些程序的语义和关键安全属性，并识别了现有语义和验证工具的各种错误和不精确性，为智能合约的安全验证提供了严谨的语义基础。
Feb, 2018
本文对 2008-2020 年间智能合约的相关文献和在线资源进行了综述，分为三类：合约设计范例、设计工具和扩展以及替代方案。对最新的执行机制进行了分类，介绍了一些解决方案，并总结了几个挑战和未来的研究方向。
Aug, 2020
Securify 是一个安全分析器，可以自动化地证明以太坊智能合约的行为在特定属性上是安全 / 不安全的，通过符号分析和合规 / 违规模式检查来实现，已经得到专家广泛使用。
Jun, 2018
在此研究中，我们提出了一种新的模糊测试工具 ContractFuzzer，用于测试以太坊智能合约的安全漏洞，该工具已经成功检测出了 6991 个智能合约中 459 个高风险漏洞，包括导致 6000 万美元损失的 DAO 合约漏洞和导致 3 亿美元冻结的 Parity Wallet。
Jul, 2018
本研究提出了一种使用长短期记忆（LSTM）的序列学习智能合约弱点以便更快地发现新的攻击趋势以实现更安全智能合约的方法，对 620,000 个智能合约的实验研究表明，该模型具有接近于恒定的分析时间并可以正确分析符号工具造成的假阳性（FP) 错误。
Nov, 2018
分布式不可变账本或区块链，在不依赖可信第三方的情况下，允许安全地数字化证据交易。智能合约作为去中心化和复制执行的程序，为区块链上的证据协议提供了机制，但需要解决信任和责任的问题。
Mar, 2024
提出了针对量子软件的设计合同框架，使用 python 嵌入式语言编写有关某些程序构建的所有量子电路输入和输出状态的断言，并提供了一种方法来写统计处理断言，以确保获取最终结果的程序的正确性。通过量子计算机模拟器自动检查这些断言，评估结果表明，该框架具有足够的表达能力来验证量子软件的整个程序。
Mar, 2023
针对并发程序的定量、性能感知综合算法，以一个非确定性部分程序和一个参数化性能模型为输入，用加权自动机捕捉系统体系结构，通过 2 - 人图游戏解决良性性能最优化问题。我们提出了一种算法方法和实现原型工具，可用于构造各种性能模型和编程模式的有限状态机并发程序。该综合问题 NEXP 完备，但通过引入博弈理论方法可解决。
Apr, 2011
使用区块链技术，创建智能合约以通过交换奖励来训练特定数据集的机器学习模型，这为各方提供了直接获取好的机器学习模型的市场，取代传统 AI 解决方案的需求。
文章提出了一种新颖的概率程序分析技术，并将其应用于量化决策程序中的偏差，开发了第一个量化程序偏差的验证工具 FairSquare，并在一系列决策程序上进行了评估。
Feb, 2017