A dispute team can measure the cases it resolved and still miss a valid notice that never entered its investigation queue. The question is where the measurement starts. If the denominator begins after intake and routing, a closure before investigation can leave the dashboard looking healthy.
That is the design problem I wanted our Dispute Workflow Verification demo to make inspectable. Its post-forms case is a synthetic reconstruction of a failure mode, not a customer record or a replay of a bank's actual systems. A modeled consumer submits a valid billing-error notice. The workflow requests a secondary form. If that form times out, the case reaches a closed state on model day six without an investigation. The expected route, which does reach investigation, still lets the demo's happy-path baseline report COMPLIANT.
A green baseline and a failed property can both be accurate descriptions of their respective checks. They answer different questions. The baseline asks whether one anticipated sequence completes. The state explorer asks whether a valid-notice state can reach a dead end with no path to investigation. In this model, it can.
The path is the finding
A failure label alone leaves a reviewer guessing what to change. The checker returns the ordered path: notice submitted, secondary form requested, timeout, then closure without investigation. That path makes the review specific. Someone can examine the timeout transition and decide whether a missing form should prevent an already valid notice from being routed to investigation.
In the synthetic post-forms model, the trace reaches ClosedIncomplete on day six without entering investigation. The screen shows a modeled counterexample, not a finding from a live bank workflow.
The distinction matters for the fix as well. In the supplied remediated model, an incomplete secondary form still routes the notice to investigation. The checker explores that new model and marks its four configured properties PROVEN. That is useful evidence that the proposed routing change removes this modeled dead end. It does not prove that a real institution has the same states, that its notices meet the relevant legal conditions, or that the encoded deadlines capture every applicable rule and exception.
What I would require before trusting the green result
I would first establish the intake boundary: which events count as a valid notice, and can any of them be closed before an investigator sees them? Then I would compare every modeled timeout and handoff with the actual process, including work handled outside the main case queue. Only after that would I treat a property result as evidence about operations. The path from notice to an appropriate handling outcome matters as much as the deadline the team monitors after intake.
The proof certificate records the checked model and assumptions for that discussion. It is a review artifact, not a legal or regulatory certificate. A PROVEN result covers the encoded property over the explored model; a capped run may instead be BOUNDED. Neither status supplies the missing evidence that the model matches production behavior.
That handling route need not always be an investigation. The CFPB’s Regulation Z interpretation permits correction of the asserted billing error without investigation, subject to the other applicable requirements. This demo checks for an investigation route in its configured model. A real workflow review must account for any valid correction route as well.
My position is straightforward: measure from the qualifying notice through its appropriate handling outcome, not merely from the cases that survived routing. The full demo breakdown shows the counterexample and the remediated model side by side.