Soft Contract Verification for Higher-Order Stateful Programs
软件契约允许程序员使用对象语言的全部表达能力来陈述丰富的程序属性。但是，由于它们是在运行时强制执行的，因此监视契约会带来显著的开销并延迟错误发现。因此，合约验证旨在提前保证所有或大部分这些属性，从而实现有价值的优化并产生更普遍的正确性保证。现有的静态契约验证方法满足了更受限制的目标语言的需求，但无法解决那些连接无类型，动态规划，高阶函数，模块化和有状态的独特挑战。我们的方法处理所有这些功能在一次，在完整的Racket系统的背景下-一个成熟的环境，有状态，高阶，多范式编程有或没有类型。使用一组纯测试和有状态测试来评估我们的方法，我们能够静态地验证99.94%的检查（49861个中只有28个除外）。有状态的高阶函数尤其对静态契约验证提出了重大挑战。在存在这些功能的情况下，模块化分析必须允许当前模块的代码永久地逃逸到一个不透明的上下文（来自当前模块外部的未指定代码），该上下文可能是有状态的，因此存储对逃逸闭包的引用。此外，合约本身，作为在不受限制的Racket中编写的谓词，可能会表现出有状态的行为;一个合理的方法必须对任意表达并与它们监视的代码交织在一起的合约具有鲁棒性。在本文中，我们提出并评估我们的解决方案的基础上高阶符号执行，解释我们用来解决这些棘手的问题，形式化的行为近似的概念，并用它来提供一个机械化的证明。
2017-11-09 cs.PL
Higher-order symbolic execution for contract verification and refutation
我们提出了一种新的方法来自动推理高阶程序赋予符号执行高阶，符号值的概念。我们的方法是健全的，相对完整的一阶求解器的基本类型值。因此，它可以为高阶程序的自动验证和缺陷查找工具奠定基础。为了验证我们的方法，我们用它来开发和评估一个系统，用于验证和反驳行为的软件合同组件的功能语言，我们称之为软合同验证。在这样做的过程中，我们发现了行为契约和高阶符号执行之间的互利关系。我们的系统使用高阶符号执行，利用合同作为符号值的来源，包括未知的行为值，并采用了一个可更新的堆合同不变的原因流敏感的事实。每当一个契约被反驳时，它会报告一个具体的反例来重现错误，这可能涉及到求解一个未知函数。该方法能够分析一级契约、递归数据结构、未知函数和控制流敏感的值的细化，这些在动态语言中都是惯用的。它有效地利用了现成的求解器来解决问题，而不需要大量的编码。这种方法在它们自己的基准测试上与广泛的现有工具（包括类型系统、流分析器和模型检查器）竞争。我们已经建立了一个工具，分析Racket编写的程序，并报告其在验证和反驳合同的有效性。
2016-03-20 cs.PL
Scilla: a Smart Contract Intermediate-Level LAnguage
本文概述了Scilla的关键设计原则--一种用于验证智能合约的中间级语言。Scilla在区块链上的智能合约的通信方面提供了一个清晰的分离，允许丰富的交互模式，以及一个编程组件，它享有原则性的语义，并且可以进行形式化验证。Scilla并不意味着是一种高级程序设计语言，我们将使用它作为高级语言（如Solidity）的翻译目标，用于在进一步编译为可执行字节码之前执行程序分析和验证。我们描述了基于自动机的模型的Scilla，提出其编程组件，并显示合同定义的自动机如何简化其安全性和时间属性的机械化验证过程。
2018-01-02 cs.PL
A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-based Service Smart Contracts
本文报告了一个正式的符号过程虚拟机（FSPVM）的开发，表示为FSPVM-E，用于在智能合约的源代码级别验证基于以太坊的服务的可靠性和安全性，并使用Coq证明助手来编程系统并证明其正确性。当前版本的FSPVM-E采用Curry-Howard同构的应用扩展--执行-验证同构作为其基本理论框架，将符号执行和高阶逻辑定理证明结合起来。FSPVM-E的四个主要组件包括通用的、可扩展的和可重用的形式存储器框架、表示为Lolisa的可扩展的和通用的形式中间程序设计语言（其是使用广义代数数据库的Solidity程序设计语言的大子集）、表示为FEther的相应的形式验证的Lolisa解释器以及辅助工具和库。所有组件的自正确性都经过Coq认证。目前，FSPVM-E支持ERC 20令牌标准，可以自动和象征性地执行基于以太坊的智能合约，扫描其标准漏洞，并使用Coq中的Hoare风格逻辑验证其可靠性和安全性。据作者所知，目前的工作代表了第一个在Coq中实现的以太坊智能合约混合形式化验证系统，该系统应用于Solidity源代码级别。
2020-01-23 cs.PL
SAFEVM: A Safety Verifier for Ethereum Smart Contracts
以太坊智能合约是公开的，不可变的和分布式的，因此，它们很容易出现源于开发人员编程错误的漏洞。本文介绍了SAFEVM，这是一个以太坊智能合约的验证工具，它使用了最先进的C程序验证引擎。SAFEVM将以太坊智能合约（以Solidity源代码或编译后的EVM字节码提供）作为输入，可选地带有assert和require验证注释，并在输出中生成带有验证结果的报告。除了一般的安全注释外，SAFEVM还处理数组访问的验证：它自动生成SV-COMP验证断言，以便C验证引擎可以证明数组访问的安全性。我们的实验评估已经对从etherscan.io（超过24，000个）中提取的所有合同进行了评估，使用CPAchecker，SeaHorn和VeryMax作为后端验证器。
2019-06-12 cs.LO cs.PL
Gradual Verification for Smart Contracts
针对外部合约实现缺失导致重入攻击难以验证的问题，本文提出结合静态与动态技术的渐进式验证方法，并通过 pyTEAL 上的 Algorand 原型验证其安全、灵活与资源优化效果。
2024-07-03 cs.CR cs.LO cs.PL
Solvent: liquidity verification of smart contracts
Università degli Studi di Cagliari（卡利亚里大学）；Università degli Studi di Modena e Reggio Emilia（摩德纳和雷焦艾米利亚大学）；Università degli Studi di Genova（热那亚大学）；Télécom Paris（巴黎电信学院）
针对现有智能合约验证工具无法有效验证加密资产交换相关流动性属性的问题，提出Solvent工具，可验证现有Solidity工具无法覆盖的该类属性，并通过通用基准测试集评估其有效性与性能。
2024-09-23 cs.CR cs.PL
Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification
渐进类型化程序设计语言允许将静态类型增量添加到非类型化程序中。为了保持可靠性，语言在类型化和非类型化代码之间的边界处插入运行时检查。不幸的是，性能研究表明，这些检查的开销可能高得惊人，这让人们对声音渐进式输入的可行性产生了疑问。在本文中，我们表明，通过建立在现有的工作软合同验证，我们可以减少或消除这种开销。我们的关键见解是，虽然非类型化代码不能被渐进类型系统信任，但在优化渐进类型化程序时，没有必要只考虑最坏的情况。相反，我们静态分析的非类型化的部分逐渐类型化的程序，以证明几乎所有的动态检查暗示逐渐类型边界不能失败，并可以在编译时消除。我们的分析是模块化的，可以应用于程序的任何部分。我们评估了这种方法对现有的十几个渐进式程序以前表现出令人望而却步的性能开销--与$3.5\times$的中位数开销和高达$73.6\times$在最坏的情况下--和消除所有的开销在大多数情况下，在最坏的情况下，只有$1.6\times$开销的痛苦。
2020-10-09 cs.PL
Teaching Design by Contract using Snap!
随着演绎程序验证研究的进展，新的工具和技术已成为可用于支持契约式设计推理的非平凡程序编写的广泛使用的程序设计语言。然而，演绎程序验证仍然是专家的活动，在编程，规范和验证方面有丰富的经验。我们想改变这种情况，通过开发程序验证技术，可用于更大的观众。在本文中，我们介绍了我们如何开发原型程序验证支持Snap！啪！是一种可视化的程序设计语言，特别针对高中生。我们以类似的视觉风格添加了规约语言构造，旨在使预期的语义从规范构造的外观和感觉中变得清晰。我们提供Snap的静态和动态验证支持！程序.特别注意错误消息，使其尽可能直观。
2021-07-12 cs.PL cs.SE
Formal Specification and Verification of Solidity Contracts with Events
Solidity语言中的事件提供了去中心化应用程序的链上服务与这些服务的用户之间的通信方式。事件通常被用作从用户的角度来看相关的合约执行的抽象。因此，用户必须能够理解所发出事件的含义并信任其有效性。本文提出了一种源代码级的方法，用于Solidity合同的形式化规范和验证，主要关注事件。我们的方法允许根据事件跟踪的链上数据来指定事件，以及定义区块链状态与事件提供的抽象视图之间的对应关系的谓词。该方法是在solc验证，Solidity的模块化验证，我们证明了它的适用性与各种例子。
2020-05-20 cs.LO cs.PL cs.SE
Neuroforger: certified violation witnesses for smart contracts verification via LLMs
University of Cagliari（卡利亚里大学）
针对自然语言属性歧义和LLM回答无正确性保证的问题，提出一种结合LLM、类型检查和具体执行的工作流，通过引入扩展Solidity的抽象类型形式规范语言，生成并验证违规见证（反例）。
2026-05-29 cs.CR cs.PL
Correctness Witnesses with Function Contracts
本文针对软件验证见证格式2.0无法表达函数契约的局限，提出扩展以支持ACSL风格的前置和后置条件，从而增强工具间信息交换能力。
2025-01-21 cs.PL cs.SE
Verification Modulo Tested Library Contracts
Indian Institute of Science（印度科学研究院）；University of Illinois Urbana-Champaign, Department of Computer Science（伊利诺伊大学厄巴纳-香槟分校计算机科学系）；University of Wisconsin（威斯康星大学）
本文提出了一种基于测试库合同的验证方法，通过合成模块化合同和上下文合同来确保客户端程序的正确性，并利用反例引导学习框架进行验证。
2026-05-07 cs.LG cs.LO cs.PL
Fast and Reliable Formal Verification of Smart Contracts with the Move Prover
Move Prover（MVP）是一个用Move程序设计语言编写的智能合约的正式验证器。MVP有一个表达性很强的规约语言，并且足够快速和可靠，开发人员可以在几分钟内例行运行它，并在集成测试中运行它。除了智能合约和Move语言的简单性之外，MVP的实用性还取决于三个转换：（1）无别名内存模型，（2）细粒度不变式检查，以及（3）单态化。Diem区块链的整个Move代码已经被广泛指定，并且可以在几分钟内由MVP完全验证。Diem框架中的更改必须在集成到GitHub上的开源存储库之前成功验证。
2022-02-13 cs.PL cs.SC cs.SE
Interaction Tree Semantics for RISC-V: Bridging Compiler and Hardware Verification
Barkhausen Institut（巴克拉森研究所）
该研究在Rocq中构建基于ITrees的RISC-V ISA形式化语义，实现编译器IR到硬件的跨层级验证，通过模拟器验证并经三项案例研究证明其有效性。
2026-08-26 cs.PL
Theorem-Carrying Transactions: Runtime Verification to Ensure Interface Specifications for Smart Contract Safety
针对智能合约安全，提出定理携带交易（TCT）技术，结合具体执行与符号证明，在运行时验证交易符合接口规范，开销极低，成功应用于代币合约和Uniswap。
2025-08-06 cs.CR cs.PL
Contract Strengthening through Constrained Horn Clause Verification
一个程序的函数属性通常通过为它的每个函数提供一个契约来指定。一个函数的契约由一对公式组成，称为前置条件和后置条件，它们分别在该函数执行之前和之后保持有效。可能的情况是，程序员提供的契约不足以允许验证系统证明程序的正确性，也就是说，对于每个函数，如果前置条件成立，并且函数的执行终止，则后置条件成立。我们解决这个问题，通过提供一种技术，可以加强后置条件的功能，从而提高验证程序的正确性的能力。我们的技术包括四个步骤。首先，翻译的给定程序，它可以操纵代数数据结构（ADT），其合同成一组受约束的霍恩条款（CHC）的可满足性意味着给定的合同的有效性。然后，通过由VeriCaT工具执行的CHC转换，导出一组新的CHC，这些CHC仅操作基本排序（例如布尔或整数），并且其可满足性暗示了原始子句集的可满足性。然后，使用CHC求解器SPACER为基本排序构造新的派生CHC的模型（如果有的话）。最后，将该模型转化为适当加强给定合同的后置条件的公式。我们将通过一个由Scala程序组成的用于反转列表的示例来展示我们的技术。请注意，当考虑给定的合同时，Stainless验证器无法证明该程序的正确性，而当考虑通过应用我们的技术构造的具有增强后条件的合同时，它成功了。
2022-11-22 cs.LO cs.PL
Extending Contract Verification for Parallel Programming Models to Fortran
TU Darmstadt University（达姆施塔特工业大学）
本文基于CoVer框架，扩展其至Fortran，实现多语言静态动态分析，验证了其在MPI-BugBench中发现bug的有效性，并优于MUST工具。
2026-04-22 cs.DC cs.PL
Contract Based Verification of Non-functional Requirements for Embedded Automotive C Code
KTH Royal Institute of Technology（皇家理工学院）；TRATON AB（特拉顿股份公司）
本文提出了一种用于验证嵌入式汽车C代码非功能需求的合同方法，通过设计通用规则和接口规范语言，结合Frama-C插件实现对控制流和数据流的检查，确保模块调用安全函数并避免未初始化变量。
2026-08-17 cs.PL cs.SE
Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?
Carl von Ossietzky Universität Oldenburg（奥尔登堡卡尔·冯·奥西茨基大学）
本文提出NL2Contract任务，利用大型语言模型将自然语言转换为形式化功能契约（含前置与后置条件），实验证明其生成契约健全且能减少验证误报，并有效捕获真实错误。
2025-10-14 cs.AI cs.PL cs.SE
solc-verify: A Modular Verifier for Solidity Smart Contracts
我们提出了solc-verify，一个以太坊智能合约的源代码级验证工具。Solc-verify采用Solidity编写的智能合约，并使用模块化程序分析和SMT求解器释放验证条件。建立在Solidity编译器之上，solc-验证在合约源代码级别的原因，而不是在以太坊字节码级别操作的更常见的方法。这使得solc-verify能够在精确建模低级语言语义的同时有效地推理高级契约属性。合约属性，如合约不变量、循环不变量和函数前置条件和后置条件，可以由开发人员在代码中作为注释提供。这为智能合约提供了自动化但用户友好的形式化验证。我们通过检查现实世界的例子，我们的工具可以有效地找到错误，并证明正确性的非平凡的属性，以最小的用户努力来演示solc验证。
2020-03-16 cs.LO cs.PL cs.SE
Towards Trace-based Deductive Verification (Tech Report)
合同规定了一个程序的行为方面的前置条件和后置条件是必不可少的可扩展的软件验证，但不能表达任何约束的过程中发生的事件执行。这就需要使用中间断言来注释代码，从而防止完整的规范抽象。我们提出了一个逻辑符号的痕迹能够指定递归过程中的模块化的方式，指的是指定的程序只在事件方面。我们还提供了一个演绎系统的基础上，我们证明是健全的相对于一个跟踪语义的符号执行和归纳。我们的工作将基于契约的演绎验证推广到基于迹的演绎验证。
2022-11-21 cs.PL cs.SE
A Complete Approach to Loop Verification with Invariants and Summaries
不变量是验证循环正确性的主要方法。作为一种替代，循环契约，它明确了基础归纳证明的前提和结论，有时可以更自然地捕获正确性条件。但是，尽管有这种优势，第二种方法得到很少的关注，这篇文章的目标是把它从它的利基。我们给出了循环合同理论的第一个全面的阐述，包括其完备性的表征。我们展示了标准算法的具体例子，展示了它们的相对优点。此外，我们展示了一个新的建设性的翻译之间的两种方法，这使得所选择的规范方法从验证后端。
2021-10-12 cs.LO cs.PL
Verification of PETSc with CIVL using LLM-generated ACSL contracts and deterministic driver generation
本文提出利用LLM生成ACSL契约和确定性驱动程序，结合CIVL验证器，对PETSc数值库函数进行形式验证，并成功发现MatAYPX中自1997年存在的未发现错误。
2026-09-29 cs.CL cs.MS cs.PL
