单测覆盖“买方付款、卖家交货、领取成功”，不代表订单状态机能抵御不同调用者、顺序、金额与时间组合。区块链（23）：外部调用前后的资产账本怎样保持一致的重入反例提示：不变量应覆盖全局义务，而不只是某个正常路径的返回值。

以原生资产托管为例，令每笔未支付订单的应退款额和所有卖家待领取额构成 liabilities。必要条件是合约可用余额不小于这些义务，并且从来不能由两个终态各登记一次同一笔金额。这里的比较需要明确强制转入等异常余额不会创造可领取债权；只检查 balance == liabilities 可能把合法的额外资产误报为漏洞。非授权地址不应使他人债权下降，错误分支不应悄悄修改订单状态。

flowchart LR
  SEED[固定 seed 与输入域] --> OPS[随机角色/订单/金额/时序]
  OPS --> EXEC[部署合约并逐步调用]
  EXEC --> INV[守恒、单次结算、权限不变量]
  INV -->|失败| SHRINK[缩小序列、保存重放轨迹]
  INV -->|通过| LIMIT[仅证明这些输入下未发现反例]

生成器必须造到拒绝路径：金额零、余额边界、重复 ID、错误角色、交付前提现、领取两次、外部调用失败；若只生成正常用户，fuzz 数量再大也测不到授权漏洞。回归先固定失败 seed、缩小后的调用序列与编译参数，再跑修复版验证攻击失败且合法领取仍能成功。invariant 持续成立与“所有性质被形式证明”不是同一句话；测试覆盖是程序、输入域与探索预算的交集。

怎样让性质测试确实碰到反例

先枚举具体义务：订单 A 可退款 70，订单 B 的卖家待领 20，合约中需有至少 90 的可支配余额。若漏洞允许 A 同时成为待领与可退款，义务增至 160 而真实资产仍为 90；断言 balance >= liabilities 应立刻失败。反过来，如果第三方强制转入 1，余额 91、义务仍 90，严格相等的断言会误报。测试还需有一个参考状态机，不允许单个订单出现在两个终态，也不允许未授权 caller 降低别人债权；资产不等式单独不足以覆盖权限。

输入生成器不能只随机构造金额，应覆盖合法的最小正额、零值、接近上界的整数、重复订单 ID 和不同执行顺序。让恶意收款地址在提现时回调，才能进入 23 篇最危险的路径；让合约升级后再重放旧调用，才能检查存储布局与签名 nonce 是否受损。examples/blockchain/models/escrow_state.py 的一订单、两种金额、无调用回调模型曾找到重复领取的短序列，说明规格如何暴露一类故障，但不是本篇 Solidity fuzz 或形式化证明。Forge 没有安装，测试 seed、覆盖度、修复回归仍为 NOT_RUN。

练习一：强制向合约额外转入 1 后，balance == liabilities 失败，必定有资产被盗吗？答案：不一定；更合适的债权安全下界是不少于义务，额外资产要规定归属。练习二：Fuzz 全用买方作为 caller，能证明卖家不能重复提款吗？答案：不能；要生成卖家、陌生角色与恶意接收合约并覆盖状态序列。Forge、seed、失败轨迹与升级回归均 NOT_RUN，不杜撰 fuzz 轮数。

可迁移原则：不变量先说明资产和角色范围，再谈探索方法。参考：Foundry invariant 测试、Solidity 安全说明（未核 release/SHA）；导航：区块链（23）：外部调用前后的资产账本怎样保持一致 · 24 · 区块链（25）：把 ERC-20 接进托管后，“收到 70”仍要核算。