The approve-then-act state machine — the most repeated flow in all of web3. Every ERC-20 interaction (deposit, stake, swap, lock…) is really two transactions gated by an allowance read, and every dapp hand-rolls the same fragile ladder. This is that ladder, once, with the guards proven by fuzz tests (ApprovalFlowTest) and modeled in proofs/tla/ApprovalSpec.tla.

┌──────────────────┐  insufficient   ┌────────────────┐
│ CheckingAllowance├────────────────▶│ ApprovalNeeded │
└───────┬──────────┘                 └───────┬────────┘
        │ sufficient                 startApprove
        ▼                                    ▼
┌──────────────┐   approve confirmed ┌────────────┐
│  ReadyToAct  │◀───(via re-check)───│  Approving │
└───────┬──────┘                     └────────────┘
   startAction
        ▼
┌──────────────┐    tx confirmed     ┌────────────┐
│    Acting    ├────────────────────▶│  Completed │
└──────────────┘                     └────────────┘

Design choices, deliberately:

• A confirmed approval re-checks the allowance instead of optimistically assuming it. Non-standard tokens (USDT's approve-to-zero-first rule, fee-on-transfer tokens) make optimism a lie; the chain is the truth.
• Wallet rejection is not failure. Rejecting the approve returns to ApprovalNeeded; rejecting the action returns to ReadyToAct — the user changed their mind, nothing is broken.
• The two transactions cannot cross. ApproveTx messages are ignored while Acting, ActionTx messages while Approving — a late confirmation from one leg can never corrupt the other (the same no-cross-confusion rule elm-web3's SignSpec proves).

Wire-up sketch:

-- fire the allowance read, then:
ApprovalFlow.update { required = amountWei } (AllowanceLoaded current) step


-- user clicks approve:
( { model | step = ApprovalFlow.startApprove model.step }
, web3Cmd approveCall
)


-- port messages for the approve tx:
ApprovalFlow.update req (ApproveTx txMsg) step