Card dispute workflow verification
In a synthetic post-forms workflow, a valid billing-error notice reaches a closed state on model day 6 without investigation. Dispute Workflow Verification explores every reachable route in that supplied model, checks its configured obligations, and shows the event path behind the failed property.
93
Reachable states explored
Bundled post-forms model
4 of 4
Configured properties fail
Same synthetic model
Day 6
Notice reaches a closed dead state
Model clock, not a customer case
These are results for authored JSON models and encoded demonstration rules, not a finding about a bank's live dispute operations.
A conventional tracker can report on the disputes it receives. It cannot show the route by which a valid notice was closed before investigation if that route is absent from its expected-case test.
The CFPB's October 2024 Apple consent order describes an added form after initial dispute submission and qualifying notices that were not forwarded when the form was not completed. Our post-forms case is an illustrative reconstruction of that failure mode, not Apple's state machine or a replay of consumer records.
The review question is precise: after a valid notice, can any modeled route reach a state from which investigation is no longer possible?
The state graph and rule results come from deterministic Python code over the supplied JSON workflow.
01 / MODEL
Locations, transitions, timing ranges, flags, and product or network labels define the four synthetic workflows.
02 / EXPLORE
Breadth-first search checks whether any valid-notice state can get trapped away from investigation and follows paths against configured timing flags.
03 / REVIEW
The result links a property verdict to the graph, the ordered counterexample with model clock values, and an exportable review certificate.
A property is COUNTEREXAMPLE when the checker finds a failing route, PROVEN when it holds across the explored finite model, or BOUNDED when the 200-calendar-day cap limits a timeline conclusion. Only the deterministic checker assigns these statuses. An optional model-synthesis agent can draft a model, but it does not verify one.
Inside the recorded walkthrough
These screens come from the supplied synthetic workflows. Start with the baseline's green result, then follow the branch it never checked. Each image opens at full size.
01 / COMPARE THE CHECKS
The standard tracker follows the completed-form route and reports COMPLIANT. State exploration asks whether another reachable branch can fail. On the same authored post-forms model it reports NON-COMPLIANT with the configured rules.
The two results answer different questions. The baseline says its chosen route passed; it says nothing about the notices that leave that route before investigation.
02 / FIND THE BRANCH
In the graph, a modeled notice moves from Messages Submitted to Secondary Form Requested. Completing the form continues toward routing and investigation. A timeout instead reaches Closed Incomplete. The checker explores 93 reachable states and finds four failed configured properties in this supplied model.
03 / INSPECT THE WITNESS
A failed property comes with an ordered counterexample. Here the modeled sequence records submission on day 0, the request for a secondary form on day 1, and timeout closure on day 6. The notice never reaches investigation on that path.
04 / CHECK THE CHANGE
The separate remediated model sends an incomplete-form notice into routing and investigation rather than closing it. With that route changed, all four configured properties are PROVEN across 153 reachable states. That conclusion belongs to the supplied finite model and its encoded properties.
A SECOND WORKFLOW / TIMING
The nightly-batch example tests a conditional provisional-credit assumption encoded in a separate synthetic model. One path first posts the modeled credit on business day 14, past that model's 10-business-day limit. The checker returns one counterexample among seven configured properties across 79 reachable states. Real Reg E exceptions and applicable periods require separate review.
The comparison is between an expected-route baseline and state exploration over the same authored workflow. It is not a benchmark against a deployed bank system.
| Review route | What it sees here | What it leaves open |
|---|---|---|
| Happy-path baseline | The anticipated route reports COMPLIANT. | It never explores the secondary-form timeout branch. |
| State exploration | 93 reachable states and a route to ClosedIncomplete without investigation in the supplied post-forms model. | Whether the supplied model matches a real workflow. |
| Remediated model | All four configured properties hold over 153 reachable states. | Whether those properties cover every applicable obligation or exception. |
The four workflows and ten benchmark fixtures are authored synthetic models. The page has no live bank, card-network, core-system, letter-generation, or consumer-data connector, and the certificate is a model review artifact, not regulator endorsement. The encoded Reg Z and Reg E clocks simplify the Reg Z billing-error rule and Reg E error-resolution rule; their notice conditions, exceptions, and real applicability need expert assessment. Visa and Mastercard windows are illustrative configured values, not verified current network rules.
A dashboard that tracks cases already in its queue may miss a valid notice that never entered that queue. In this synthetic post-forms model, the happy-path baseline reports COMPLIANT, while state exploration finds a route from valid notice to ClosedIncomplete on model day 6 without investigation. The counterexample shows each event on that route.
No. PROVEN means a configured property held over the explored states of the supplied finite model. Actual compliance depends on whether the model matches the live workflow, whether the notice qualifies, and which rules and exceptions apply. This demonstration is a review aid, not a legal opinion.
The recorded demonstration uses four synthetic JSON workflow models. It has no live connection to a bank queue, core system, notice generator, Visa or Mastercard system, or consumer records. A real assessment would first need a validated model of the actual process and applicable obligations.
For a failed configured property, the checker shows the state graph, an ordered counterexample trace with modeled events and clock values, and an exportable review certificate. In the post-forms example, the trace reaches ClosedIncomplete after the secondary-form timeout without investigation. The certificate records the checked model and limits; it is not regulator endorsed.
The demonstration uses simplified encoded clocks. Its Reg Z resolution check reduces the two-complete-billing-cycles condition to a 90-calendar-day ceiling, and its Reg E 10-business-day check uses a fixed 7/5 conversion without holidays. Exceptions, extended periods, and rule applicability need separate expert review.
Exploration is capped at 200 calendar days. If it reaches that cap without a counterexample for an applicable timeline property, the checker reports BOUNDED rather than PROVEN. A counterexample found within the explored path remains visible.
No. An optional model-synthesis agent can propose a workflow model when configured, but deterministic Python code explores its states and assigns PROVEN, COUNTEREXAMPLE, or BOUNDED. The four bundled cases run without an LLM or a live network connection.
Explore related research for broader context on this demonstration.
A useful first step is to map where a qualifying notice enters, waits, routes, and closes.
We can help frame the workflow model, choose the obligations to test, and review a counterexample with dispute operations, engineering, and compliance specialists before anyone treats the model as evidence about a live process.
