Off-chain differential (real-node bindings): the Agda-extracted §6 handler decisions (Hydra.Agda.OffChainReference) checked against the REAL update outcomes, not against transcriptions of the figure. This extends OffChainLeaderSpec (which binds leaderRef to the real isLeader) to three more decisions, closing the figure↔Agda↔Haskell loop:

• signEligibleRef vs onOpenNetworkReqSn: we drive update with a ReqSn over an open state with version v̂ and a settled snapshot ŝ (confirmed = seen, nothing in flight) and binarise the outcome: ACCEPT iff the node reaches the signing continuation (SnapshotRequested + an AckSn effect). The node splits the figure's single require into an Error (number: ReqSnNumberInvalid, leader: ReqSnNotLeader) and a Wait (version: WaitOnSnapshotVersion, so a follower behind on the version bump does not drop the message); Error and Wait both map to non-accept. The reference's leader input is resolved by the EXTRACTED leaderRef (itself bound to the real isLeader in OffChainLeaderSpec), so the composed decision is fully Agda-derived.
• reqDecEligibleRef vs onOpenNetworkReqDec: ACCEPT iff the node records the decommit (DecommitRecorded). A PENDING deposit makes the node WAIT (WaitOnUnresolvedCommit) at ttl > 0, and so does an in-flight decommit (WaitOnNotApplicableDecommitTx with DecommitAlreadyInFlight); both are non-accept. The commit axis is the reference's HsPendingCommit, not a Bool, so this test cannot decide which commits count: an expired or already-recovered deposit is a state the node reaches (it clears currentDepositTxId on neither) and the reference is what says those do not block.
• reqSnNotBothRef reqSnDecommitOutputsRef reqSnDepositSettledRef vs onOpenNetworkReqSn's incremental-action guards: a request carrying both a deposit and a decommit is ReqSnBothCommitAndDecommit; a decommit producing no outputs is ReqSnDecommitNoOutputs; and settling a same-version pending commit requires the request to name the deposit bound into the confirmed snapshot by tx-id (ReqSnCommitNotSettled otherwise) - the look-alike-deposit case, where content matches and only identity differs.
• depositStatusRef vs the deposit-status transition the node applies on a chain Tick (onOpenChainTick via determineNextDepositStatus): starting from a fresh Inactive deposit, one tick at time t yields DepositExpired DepositActivated no status event, mapping to ExpiredS ActiveS InactiveS.
• notAlreadySignedRef vs onOpenNetworkAckSn's requireNotSignedYet: over a directly constructed in-flight SeenSnapshot whose signatories map holds REAL signatures, an AckSn from a sender already in the map is the node's SnapshotAlreadySigned; a fresh sender is not.
• allSignedRef vs the round completion of onOpenNetworkAckSn: a fresh sender's ack CONFIRMS (the node aggregates the real signatures in order and verifies the real multisignature before emitting SnapshotConfirmed) exactly when it completes the n-of-n signer set; the composed decision is notAlreadySignedRef ∧ allSignedRef (sender ∷ Σ̂).
• contestEligibleRef vs onOpenChainCloseTx: observing a close of snapshot s_c while our confirmed snapshot is S̄.s posts a ContestTx exactly when S̄.s > s_c.

Domain note (deposit status): the extracted decision uses Nat truncated subtraction for deadline − T_deposit whereas the node subtracts over UTCTime; the two agree whenever deadline ≥ T_deposit, which the protocol guarantees (an observed deposit deadline sits a full deposit period after creation). The property therefore quantifies over that domain, with all times as whole POSIX seconds (exact in both representations).

Scope note (ackSn): the extracted guards model the COUNTING decisions (who signed, n-of-n); the collected signatures themselves are held healthy, exactly as the on-chain reference holds crypto conjuncts healthy. The real node additionally verifies the aggregate multisignature at confirmation; a corrupt collected signature makes it reject (InvalidMultisignature) where the counting reference alone would accept, demonstrated as a validator-only rejection below.