Generated code reproduces the shape of a control, not its property.

The vulnerable version below is what an idempotent charge handler looks like if you have read about idempotent charge handlers. It has the lookup, the early return, and the bookkeeping call. It is not idempotent.

def charge(request, provider, db):
    if db.was_processed(request.id):
        return db.result(request.id)
    result = provider.charge(request.amount)
    db.mark_processed(request.id, result)
    return result

def charge(request, provider, db):
    with db.idempotency_lock(request.id) as claim:
        if claim.completed:
            return claim.result
        result = provider.charge(request.amount, idempotency_key=request.id)
        claim.complete(result)
        return result

A reviewer skimming for missing controls will not flag the first version, because the control is present. The question that finds it is different: name the invariant, then show the path that enforces it.

The second recurring shape is a check on the wrong noun. Here the code validates that the coupon is active. The invariant is that a coupon is redeemable once.

def apply_discount(order, code):
    if code['active']:
        order['total'] -= code['amount']
    return order

def apply_discount(order, code):
    if not code['active'] or code['id'] in order['redeemed_codes']:
        raise ValueError('not redeemable')
    order['total'] -= code['amount']
    order['redeemed_codes'].add(code['id'])
    return order

• Authorization enforced where the caller is notThe interface hides the action; the endpoint does not check. Generated code follows the visible flow, and the visible flow is the browser.
• Client-provided state overruling stored truthA price, a role, a status, or a quantity arrives in the request and is written without being re-derived from the server-side record.
• Null coerced into safeA missing owner, an unresolved tenant, an empty result, or an unparsed value silently becomes zero, false, free, or allowed.
• Tests that assert the wrong layerThe test calls the service function directly and passes. The defect is in the route, the worker, or the database policy that the test never touches.
• A success message covering a failed second writeThe first write commits, the second fails, and the interface reports success. Observability honesty is its own review lens for this reason.
• A green typecheck read as a green buildTypes compiling says nothing about what the built artifact serves. One recorded audit nearly accepted a fix that a stale prerender cache had silently reverted.

The coverage model crosses 21 security families with 26 verification lenses, producing 546 hypothesis records. Four of the lenses are unusually productive against generated code, because each asks about a property rather than about a missing line. Where a lens keeps returning the same class, the matching Gold Check Pack carries the deeper investigation plan.

Use SecHelix to review this repository. Treat generated and hand-written code identically.
Map trust boundaries first, then select applicable hypotheses.
For each control you find, state the invariant it is supposed to enforce and show the path that
enforces it. Where a pattern is present but the invariant is not enforced, raise a candidate.
Do not report anything as VERIFIED without an independent refutation attempt.

The prompt assumes the skill is already loaded; installation covers the path for each host, and the fixtures behind the two examples above are in the open repository.

The same discipline that keeps a plausible pattern from passing also keeps a plausible accusation from sticking. In the one published run, a candidate that any scanner would report as high-severity cross-site scripting did not survive the verification pass.

The candidate

Remote configuration values flowed into href and src attributes with only whitespace trimming applied.

The reproduction

A local mock configuration API served a javascript: payload into three separate sinks.

What the document contained

href="javascript:throw new Error('React has blocked a javascript: URL as a security precaution.')"

Why it was refuted

No script execution was achievable, and attacker control was never established: the configuration source is the operator’s own API.

Recorded outcome

FALSE_POSITIVE, with the refutation reason retained rather than deleted.

What still shipped

A scheme allowlist at the trust boundary, labelled as hardening rather than as a vulnerability fix, because depending on a renderer internal for URL safety is fragile.

• The verifier receives the candidate as a claim to disprove, without the narrative that produced it and without the severity it is expected to defend.
• Two models agreeing is correlated output, not independent confirmation.
• A refuted candidate is a successful outcome. FALSE_POSITIVE, LIKELY_BUT_UNPROVEN, and BLOCKED_BY_ENVIRONMENT are all valid states in the schema.