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
        v                                    v
+--------------+   approve confirmed +------------+
|  ReadyToAct  |<---(via re-check)---|  Approving |
+-------+------+                     +------------+
   startAction
        v
+--------------+    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