安全还不够：让智能合约从规格中生成

一个永远拒绝所有交易的智能合约，可能非常“安全”。它不会重复提款、不会错误转账，也不会违反交易顺序约束——因为任何交易都无法执行。但这样的合约显然毫无用处。

这揭示了智能合约自动生成中的一个核心难题：安全不等于可用。

我们的论文 Smart Contract Synthesis via Multi-modal Specifications 已被 ASE 2026 接收。论文提出的 SmartSpec 探索了一种不同的开发方式：开发者先写下“合约应该做什么”和“绝不能发生什么”，系统再从这些规格出发构造 Solidity 实现，并把验证器的反馈用于迭代完善代码。

这篇文章介绍 SmartSpec 的问题意识、完整工作流程，以及它当前能做什么、还不能做什么。

为什么不能只靠“写完再查”

智能合约直接管理资产，且部署后的修复代价很高。传统流程通常是：

写 Solidity → 测试/验证 → 发现问题 → 修改代码 → 再测试/验证

静态分析、模糊测试、模型检查和形式化验证已经能发现许多问题；但合约业务逻辑中最棘手的错误，往往只会在多笔交易组成的历史中显现。

以一个简化的质押合约为例。下面只展示提款函数；每笔质押由 (用户地址, id) 唯一标识：

struct Stake { uint256 amount; uint256 unlockAt; bool unstaked; }
mapping(address => mapping(uint256 => Stake)) public stakes;
 
function unstake(uint256 id) external {
    Stake storage s = stakes[msg.sender][id];
    require(s.amount > 0);
    require(block.timestamp >= s.unlockAt);
    // 若遗漏 require(!s.unstaked)，会发生什么？
    s.unstaked = true;
    payable(msg.sender).transfer(s.amount);
}

如果遗漏了对 s.unstaked 的检查，攻击者可以连续两次调用 unstake(id)。第一次调用看起来完全正常；问题只在第二次调用、并且依赖第一次留下的状态时才出现。

我们真正想表达的并不是“某个函数的输入要落在什么范围内”，而是一个跨交易的性质：

对任意用户 p 的任意质押 i，成功提款最多只能发生一次。

沿用论文的过去时序逻辑记号，并把调用者补入事件标识，这条性质可以写成 □(¬(•(♦unstake(p,i)) ∧ unstake(p,i)))，对所有 p,i 成立。这里 unstake(p,i) 表示用户 p 的一次成功提款；□ 表示“始终”，♦ 表示“当前或此前曾经发生”，• 表示“上一步”。因此，如果这笔质押此前已经被提取，当前就不能再次成功提款。

如果开发者能够直接写下这类性质，并让系统据此构造实现，就可以把精力更多放在业务意图和安全边界上，而不是反复手写、调试和修补守卫条件。

SmartSpec：两类规格，各司其职

论文标题里的 “Multi-modal” 不是指图像、文本或语音，而是指两类互补的逻辑规格：

1. 关系式功能规格：描述合约状态如何从交易历史中推导出来。
2. 时序安全规格：描述一段交易序列中绝不能发生什么。

前者给出状态的含义，系统由此推导更新；后者限定允许出现的执行历史。质押例的“最多提款一次”就是后一类规格。后面会用论文中的众筹合约展示两者如何共同参与生成。

两类规格缺一不可。只有状态关系，系统可能生成能更新状态、却允许危险交易顺序的合约；只有安全性质，系统又不知道余额、额度等状态该如何维护。

从 DeCon、DCV 到 SmartSpec

SmartSpec 建立在我们此前的两项工作之上，但三者承担不同角色：

DeCon：先让开发者说明“状态意味着什么”

DeCon 提供了一种声明式的合约表示：开发者不用把状态更新分散写在各个 Solidity 函数里，而是用接近 Datalog 的关系式规则定义状态的含义。例如，余额可以直接定义为历史收入减去历史支出，编译器再确定性地生成相应的 Solidity 状态维护逻辑。

它解决了“如何从高层规则得到实现”的问题，但交易的前置条件仍需由开发者写出。仅有“不能重复提款”这一安全性质时，DeCon 不会自动补出缺失的 require(!unstaked)。

DCV：再回答“这个合约是否真的安全”

DCV 面向 DeCon 合约，让开发者用“违例查询”（violation query）描述不应出现的状态，再用数学归纳法证明这些状态始终不可达。为了完成证明，它会自动寻找辅助的归纳不变式，减少手写证明注解的工作。

按照 DCV 原论文的接口，证明成功时返回安全证明；无法完成证明时返回 Unknown，并不能据此断定合约存在漏洞。它的任务是验证给定实现，尚不负责自动补全交易守卫。

SmartSpec：把生成与验证闭合成一个循环

SmartSpec 复用 DeCon 的状态更新推导与 Solidity 生成能力，结合 DCV 的归纳验证后端、时序规格处理和有界反例搜索来综合交易守卫。每轮求解既要排除已知反例，也要尽量保留合法行为；验证反馈因此直接参与下一版实现的构造。

从规格到 Solidity：完整的生成与验证循环

图 1：SmartSpec 的端到端流程。图源：论文 overview figure。

图 1 中有两个主要阶段：先由功能规格推导状态更新骨架，再循环综合并验证交易守卫。许可性目标在每轮求解中生效。下面用众筹合约把这个过程走一遍。

1. 开发者提供什么：状态规则与安全要求

众筹合约支持投资 invest、关闭募集 close、退款 refund 和受益人提款 withdraw。目标金额 target、管理员 owner、受益人 beneficiary 是配置；closed 记录募集是否关闭。

论文中的四条功能规则把投资相关状态定义为交易记录上的关系：

raised(s)       :- s = sum m: invest(_, m).
investTotal(p,s):- invest(p, _), s = sum m: invest(p, m).
refundTotal(p,s):- refund(p, _), s = sum m: refund(p, m).
balanceOf(p,s)  :- investTotal(p,i), refundTotal(p,r), s := i - r.

这四条规则没有描述“给变量赋什么值”，而是声明：raised 是所有投资之和；某个参与者的 balanceOf 是其投资减去退款。规则从右向左阅读：当右侧条件成立时，左侧关系被推导出来。

与之配套的一条时序安全规格是：受益人提款与投资者退款不能在同一份众筹历史中同时发生。

□(¬(♦withdraw ∧ ♦refund))

这是完整规格中的一条性质。众筹示例还包含“只有管理员可以关闭募集”“未达目标时不能提款”“只有受益人可以提款”“募集关闭且未达目标时才允许退款”等要求。后面的权限和金额守卫来自这些完整要求与采样轨迹，不能仅由上面这条互斥性质推出来。

2. 从状态含义推导更新骨架

SmartSpec 不在所有可能的 Solidity 程序中盲目搜索。它沿着关系依赖生成状态维护指令：invest → raised，以及 invest → investTotal → balanceOf。对于一笔 invest(p, n)，骨架中已经能得到类似更新：

invest(p, n):
    raised <- raised + n
    balanceOf[p] <- balanceOf[p] + n
    // 交易守卫待综合

上面是骨架伪代码，省略了声明和其他交易。确定的状态更新由规则推导，搜索集中在交易前置条件上；编译器还会沿依赖链消除不必物化的中间关系，例如 investTotal。

3. 每轮如何选守卫：阻止反例，同时保留正常交易

SmartSpec 从无守卫骨架开始。系统从关系、交易参数和比较运算中枚举候选谓词，例如 closed(false)、raised(r), target(t), r < t、balanceOf(p,n) 和 n > 0。变量必须来自交易参数或已绑定的状态；系统在这些可求值的谓词中选择合取组合。

为了看清反例如何变成约束，先只观察“提款与退款互斥”这一条性质。下面是按骨架语义构造的教学轨迹，金额单位任意，不是工具运行日志：

target = 100，raised = 0，closed = false
1. Alice 投资 40                         → raised = 40
2. owner 调用 close()                    → closed = true
3. beneficiary 调用 withdraw(20)         → 已发生提款
4. Alice 调用 refund(20)                 → 提款与退款同时出现在历史中

初始骨架还没有检查提款门槛与身份、退款条件等守卫，提款金额也尚未被约束为全部筹资额，因此能够表示这条轨迹。完整验证还会更早指出第 3 步“未达目标却提款”的问题；这里单独看互斥性质，是为了说明一条反例如何被排除。

综合器把反例加入集合，并要求新候选至少拒绝其中一步。这并不自动意味着它一定拒绝最后一步：禁止所有退款，甚至禁止投资，都能阻止这条历史。

因此，每轮求解还会同时最大化被接受的采样合法轨迹数量。假设样本里有两种正常情形：

T退款：投资 40 → 关闭募集 → Alice 退回 40
T提款：Alice 投资 60 → Bob 投资 50 → 关闭募集 → 受益人提取 110

仅比较以下两种修改，其他守卫保持相同：

在这组样本上，B 比 A 接受更多正常行为，因此得分更高。这只是一次局部选择的示意；完整系统要比较整个样本集，并把选出的候选重新交给验证器，不能凭阻止了一条反例就宣告安全。

同样地，质押反例 stake(Alice,0) → unstake(Alice,0) → unstake(Alice,0) 可以通过禁止全部提款来阻止。若样本包含“到期后成功提取一次”的正常历史，!unstaked(Alice,0) 就比“禁止提款”保留更多正常行为。采样轨迹因此不只是测试数据，也直接影响候选守卫的选择。

这种策略称为轨迹有界的最大许可性：优化范围限于采样轨迹和给定的守卫搜索空间，不代表所有可能执行上的全局最大许可性。

4. 求解器怎样处理这些轨迹

图 2：候选守卫的编码。图源：论文 encoding figure；图中使用的是通用谓词示例。

对于已经固定的反例和样本，SmartSpec 先回放骨架，再记录候选谓词的真假值。守卫取值于当前交易执行前：第一个交易配对初始状态，第二个配对执行完第一个交易后的状态，依此类推。

例如，在两次投资后由管理员关闭募集、再由受益人提款的轨迹中，可以得到如下表格。这里假设投资者和受益人都不是管理员：

close() 执行前 closed 仍为假；只有后续交易才看到真。这个时点很关键：在质押例中，首次提款前 unstaked 为假，提款后才变真，因此 !unstaked 能接受第一次、拒绝第二次。

图 2 的位向量编码“每个守卫选中哪些谓词”；选中谓词按逻辑与组合。一次调用通过守卫，需要所有选中的谓词都在调用前为真；整条轨迹通过，需要每一步都获准。求解器由此能把“拒绝每条反例”编码为硬约束，把“接受尽量多的合法样本”编码为优化目标。

对于这些固定轨迹，Z3 主要搜索谓词选择，不必在每次选择时重新符号化完整状态转移。新候选的安全性仍由验证后端检查，具体回放没有替代验证。

5. 重新验证，再组合成 Solidity 输出

新候选交回验证器后，若出现另一条反例，系统继续累积约束并求解。达到迭代上限仍未找到候选时，系统报告未找到；如果停止于没有新反例，则输出仍需按验证器所提供的保证理解。

在完整众筹规格下，论文给出的中间验证规则如下。为与前文统一，这里把原图的关闭状态更新写成触发它的 close() 交易守卫；其余保留关系式表示：

invest(p,n)  -: msgSender(p), msgValue(n), closed(false),
                raised(s), target(t), s < t.
close()      -: msgSender(s), owner(s).
refund(p,n)  -: msgSender(p), closed(true), raised(r),
                target(t), r < t, balanceOf(p,n), n > 0.
withdraw(p,r)-: msgSender(p), beneficiary(p), raised(r), target(t), r >= t.

符号 -: 表示交易获准所需的条件，closed 在 close() 提交后更新为真。比如，提款条件中的 beneficiary(p) 约束调用者角色，r >= t 检查目标是否达到；这些都有前面列出的完整业务要求作为依据。

守卫与状态更新骨架组合后，才编译成 Solidity。以投资入口为例，其含义可以用下面的伪代码说明；实际生成代码还包含关系存储与参数绑定细节：

invest(p, n):
    require p == msg.sender 且 n == msg.value
    require closed == false 且 raised < target
    raised <- raised + n
    balanceOf[p] <- balanceOf[p] + n

读者由此能追溯两类代码的来源：状态更新来自功能规则，守卫来自候选谓词、规格约束和轨迹选择。归纳证明成功时，安全保证覆盖任意长度的历史；若仅通过界限内的模型检查，保证就只覆盖该界限。 论文实验的反例搜索界限是 5 笔交易。

如果合法交易仍被误拒绝，开发者怎么修正

有限采样可能漏掉边界行为。例如，假设退款候选要求 balanceOf[p] > n，Alice 投资 40、在募集失败并关闭后申请退回全部 40，就会被拒绝。如果这笔交易在业务上应该允许，开发者可以提供这条带有投资和关闭操作的具体正例。

系统把人工正例加入“必须接受”的硬约束，再重新综合和验证；它不同于只用于打分的随机采样轨迹。这样，开发者能够用业务例子修正过度限制的行为，同时保留已有安全要求。论文中需要交互的 4 个案例，都在最多 4 轮这类反馈后得到符合预期的结果。

实验结果说明了什么

我们在 27 个合约上评估 SmartSpec，观察的不只是“能否跑通”，还包括交互成本、运行时间、代码开销和支持范围：

这里的“语义一致”不要求生成代码在文本上与手写 Solidity 完全相同。我们关心的是它是否满足相同的关系式与时序规格，并经人工检查和测试确认与参考实现的预期行为一致。

论文还比较了具体轨迹编码与符号编码。表中的符号编码对照有 5 个案例达到 20 分钟超时，而具体编码在这些案例上均完成；也有小合约的符号编码耗时更短。收益随案例而变化，这里的历史对照也不是固定随机轨迹、同版本实现下的新配对实验，因此不使用一个平均加速倍数概括。

边界同样重要

SmartSpec 当前面向核心逻辑可由关系式规则表达的独立 Solidity 合约。它支持 ETH 转账、有限循环和固定、无副作用的辅助函数；目前不直接处理外部合约调用或预言机交互、合约创建与销毁、递归，以及复杂密码学逻辑（例如 Merkle tree 验证）。

在按交易数选取的 Top-50 Ethereum 合约样本中，22/50（44%）可直接落入当前片段；将跨合约调用用轻量 assume 块抽象后，这一数字为 38/50（76%）。这不是“已经覆盖 76% 的生产合约”，而是对一个明确样本和明确语言片段的覆盖分析。

从“写完再验证”到“让规格驱动实现”

传统流程中，规格和验证常在代码完成后才介入：先写实现，再问它对不对。SmartSpec 尝试反转这个顺序：先写下状态的含义与不可逾越的安全边界，再让工具生成、验证和迭代实现。

这并不意味着系统已经可以自动生成任意智能合约。更现实的价值在于，它提供了一条可验证的开发路线：

• 用关系式规则说明状态“是什么”；
• 用时序性质说明什么“绝不能发生”；
• 用反例帮助系统修正交易守卫；
• 在安全之外，尽量保留正常行为。

我们希望未来的安全关键程序开发，不只是在代码写完后检查漏洞，也能从清晰的规格出发，让生成与验证共同参与实现过程。

相关链接

• SmartSpec 论文
• SmartSpec artifact（代码、数据和复现实验脚本）
• DeCon
• DCV