The bug is between two individually correct operations.

The comment in the vulnerable version is not wrong. A refund may indeed never exceed what the customer paid. The bound simply does not enforce that sentence.

def refund(self, order_id, amount, actor):
    order = self._orders.get(order_id)
    if order is None:
        raise LookupError("unknown order")
    if amount <= 0:
        raise ValueError("amount must be positive")
    # A refund may never exceed what the customer paid.
    if amount > order["total"]:
        raise ValueError("refund exceeds order total")
    self._ledger.credit(order["customer_id"], amount)
    self._orders.append_refund(order_id, amount, actor)
    return {"order_id": order_id, "refunded": amount}

def refund(self, order_id, amount, actor):
    with self._orders.transaction() as tx:
        order = tx.lock_order(order_id)
        if order is None:
            raise LookupError("unknown order")
        already = sum(r["amount"] for r in tx.refunds_for(order_id))
        remaining = order["total"] - already
        # The invariant is cumulative, not per-request.
        if amount > remaining:
            raise ValueError("refund exceeds remaining refundable balance")

The same defect appears wherever a quantity accumulates: store credit, payout instructions, seat allocations, inventory decrements, and usage quotas. The tell is a comparison against a stored total rather than against a total minus what has already been consumed.

The second shape is a read that establishes a precondition and a write that never re-asserts it. Between those two statements, another request can do the same thing.

voucher = self._db.query_one(
    "SELECT code, value, redeemed_by FROM vouchers WHERE code = ?", [code]
)
if voucher is None:
    raise LookupError("unknown voucher")
if voucher["redeemed_by"] is not None:
    raise ValueError("already redeemed")

self._wallet.credit(user_id, voucher["value"])
self._db.execute(
    "UPDATE vouchers SET redeemed_by = ? WHERE code = ?", [user_id, code]
)

# Claim atomically: the WHERE clause carries the unused precondition.
claimed = self._db.execute(
    "UPDATE vouchers SET redeemed_by = ? WHERE code = ? AND redeemed_by IS NULL",
    [user_id, code],
)
if claimed.rowcount != 1:
    raise ValueError("already redeemed or unknown voucher")

• The guard is per-request rather than cumulativeIt bounds one operation instead of the sum of committed operations. Correct for one call, wrong for a sequence.
• The idempotency record is written after the external effectA window exists in which the charge happened and the record does not. The retry then charges again.
• The idempotency key is derived per attemptRetries present as new logical requests. The key has to identify the request, not the transmission.
• Timeout is treated as failureAn external call that timed out has an unknown outcome. Coercing unknown into failure duplicates a side effect that already succeeded.
• Uniqueness is enforced only in application codeA lookup with no constraint behind it in the store is a suggestion. Two processes can both pass it.
• Balances are mutable stored totalsWhen the total is updated in place, no derivation exists that can be checked against the underlying entries, so divergence is undetectable.

These defects live between two actions, so the review artifact is a transition table rather than a file list.

Preconditions

The states from which this transition is legal.

Actor

Which effective subject may trigger it, including services and provider callbacks.

Source of truth

Which system owns the answer when two records disagree.

Side effects

Provider calls, ledger writes, inventory decrements, notifications.

Idempotency identity

The key that makes a repeat of this transition a no-op.

Retry behaviour

What a client, a queue, and a provider each do on failure.

Partial-success behaviour

What is persisted when the second write fails.

Terminal behaviour

Whether the state can be left, and by whom.

Then look for the combinations, because that is where the invariant is missing. The two Gold Check Packs below turn that search into a written plan, and installing the skill is what puts them in the session.

refund + late provider success
delivery + cancellation
cost edit + finalized payout
two admins + one assignment
timeout + retry + delayed callback
partial fulfillment + "mark full"
seller A + seller B's object

Use SecHelix to audit business logic, payment/accounting truth, and concurrency.
Model state transitions and invariants for create/update/cancel/refund/approve/claim/redeem/
withdraw/transfer/purchase/webhook operations.
Test replay, idempotency, duplicate execution, partial success, late callbacks, negative/overflow
values, price tampering, stale state, TOCTOU, and double-spend windows in a safe environment.

Money pack

SEC-MONEY-INVARIANT-001

Money boundary

MONEY_CONSERVATION · action TRANSFER · sinks REFUND_CALL, LEDGER_WRITE, PAYOUT_INSTRUCTION, PROVIDER_EVENT_HANDLER

Money impact statement

Maximum excess value per captured amount and per unit of time. Not a severity word.

Race pack

SEC-RACE-IDEMPOTENCY-001

Race boundary

SINGLE_USE_TRANSITION · action CONSUME · sinks STATE_TRANSITION_WRITE, EXTERNAL_SIDE_EFFECT, COUNTER_DECREMENT, EVENT_CONSUMER

Race refutation tests

Inspect the schema and migrations for a unique constraint; run the reproduction against a known-correct path to confirm the harness can tell a real duplicate from a flaky fixture.

Default validation mode

LOCAL for both. Destructive actions and production mutation are forbidden by the schema.

Calibration

NOT_MEASURED, sample size 0, for both.

• The canonical fix is usually one exact-once merge rather than several dedupe rules, or one atomic operation rather than delete-then-insert.
• Preserve historical, accounting, and audit evidence during repair. A fix that rewrites ledger history is not a fix.
• Remediated variants must still complete the first legitimate execution, so a blanket denial cannot pass as a repair.

The last rule is not theoretical. In the published run, the regression suite asserts both that hostile input is refused and that legitimate input still resolves, precisely so a blanket denial could not pass as the fix.