区块链（E08）：有限模型、fuzz 与形式化证明的边界

区块链（24）：fuzz 和 invariant 要围住哪笔资产给托管提出了“债权不超过资产”。把它写进有限模型时，需要列出订单状态、买卖角色、金额区间和动作集合。可达状态检查能穷举给定上界内的动作序列，找到重复领取等短反例；无法据此证明任意大金额、任意多订单、真实 EVM gas 或链外配送都正确。随机 fuzz 扩大输入探索但不承诺覆盖所有状态；形式化证明也仅证明规格陈述与工具假设之下的性质。

flowchart LR
  SPEC[明确规格: 单次结算/资产义务] --> MODEL[状态与有限上界]
  MODEL --> SEARCH[枚举/模型检查]
  SEARCH -->|违反| TRACE[最短反例: 状态/动作]
  SEARCH -->|无反例| BOUND[仅对此边界安全]
  SPEC --> IMPL[Solidity/客户端实现]
  IMPL --> GAP[还需实现符合规格的对应关系]

例如在只有 1 笔订单、2 个角色、金额取 {1,2} 的模型里，若状态是 FUNDED→CLAIMABLE→PAID，第二次领取仍从同一债权转账，可得到有界反例。但如果生产合约有另一条未建模的管理员强制提款，模型再充分也找不到它。无反例报告必须附输入上界、状态数、转移数、工具版本、代码 SHA；被杀死的测试或手写断言与机器证明不能互相冒名。

本系列在 examples/blockchain/models/escrow_state.py 给出实际可运行的穷举：State(phase, locked, owed, paid)；从 NEW 出发，只有存入后可以交付或退款，交付后只能领取。对每种金额，五个可达状态、四条转移，检查 owed ≤ locked 与 locked + paid ≤ amount 均未找到反例。打开故障开关，在 PAID 下仍准许 claim_again，穷举器走到第六状态并返回最短动作序列 deposit→deliver→claim→claim_again，此时 paid=2×amount。python3 examples/blockchain/run_state_evidence.py 保存原始测试、状态数、转移数、反例和完整代码 SHA。

练习一：只枚举金额 1–2，能推断 uint256 溢出永不会发生吗？答案：不能；需另外证明整数边界或引入专门约束。练习二：规格不含外部回调，模型检查“无重复提现”通过，对重入仍保证安全？答案：不能；回调转移未建模。Python 有界检查已运行，证据位于 examples/blockchain/evidence/E08/；形式化工具、真实合约规格、实现符合规格的映射与证明 NOT_RUN。

可迁移原则：先写与真实实现的对应关系，再讨论搜索范围和证明强度。参考：TLA+ 官方资源、Foundry invariant testing（未核工具版本）；导航：区块链（E07）：用 Polkadot 对照应用链与共享安全 · E08 · 主线入口区块链（00）：从中心化订单基线开始。