合约核心 = 状态机 (S, S₀, Next, Invariant)

S   = 所有可能状态的集合（合约变量赋值）
S₀  = 所有可能初始状态
Next ⊆ S × S  合法转移关系

Invariant ⊆ S  必须在所有可达状态中被满足的谓词

Safety 定理: ∀ s ∈ Reachable(S₀, Next), Invariant(s) = true

Coq 逻辑:
Theorem no_reentrancy:
  forall s s' old_bal caller target amount,
    old_bal = s.balances[caller] /\
    s.balances[contract] >= amount /\
    step(s, withdraw(caller, amount), s') ->
    s'.balances[caller] = 0.

Proof.
  intros. unfold step, withdraw.
  apply state_before_transfer.  // 核心：先扣减再转出的不变式
  contradiction.  // 任何重入路径都导致矛盾
Qed.

// 指定 ERC20 Transfer 语义
rule transfer_invariant {
    env e;
    address from; address to; uint amount;
    
    require e.msg.sender == from;
    mathint fromBal_before = balanceOf(e, from);
    mathint toBal_before = balanceOf(e, to);
    
    transfer(e, to, amount);
    
    mathint fromBal_after = balanceOf(e, from);
    mathint toBal_after = balanceOf(e, to);
    
    // 不变式：from 的余额减少 amount，to 的余额增加 amount
    assert from == to 
        => fromBal_after == fromBal_before,
        "transfer:self-transfer balance shouldn't change";
    assert from != to 
        => toBal_after == toBal_before + amount 
        && fromBal_after == fromBal_before - amount,
        "transfer:balance conservation";
}