Payment authorization hold behavior modeled and tested across providers
HoldSpec: A Machine-Checked Model and Conformance Suite for the Payment Authorization Hold Lifecycle
Software Engineering
Summary
When people pay with cards, sometimes money is 'held' but not fully taken right away, causing confusion about what happens to that money. The authors created a precise model describing all the steps and rules for handling these holds, based on rules from big payment companies. They then made a set of automatic tests to check if different payment providers follow these rules correctly. Their tests found all known errors in simulated systems and highlighted important differences between providers that could cause problems in software that tries to work with both. They share their model and tests for others to use and improve.
What this means in practice
- •For payment service developers: Validate and standardize card authorization hold handling in payment platforms using a machine-checked model and test suite.
- •For financial compliance teams: Identify discrepancies in payment provider hold lifecycle policies to ensure regulatory and operational alignment.
Authors
Abhishek Sharma
Abstract
When a merchant authorizes a card and captures the funds later, the money sits in a state that neither party fully controls: held on the cardholder's account, not yet taken, and due to lapse on a deadline set by the card network. What a merchant may do to that hold, capture part of it, capture again, void it, raise it, let it expire, is business logic that every payment service provider implements slightly differently and none of them specifies formally. We give the lifecycle a state machine in TLA+, parameterized by a provider capability profile, and check eight safety invariants and three liveness properties over 6 profiles, five of them built from Stripe's and Adyen's published documentation. From the same machine we generate a conformance suite that runs black-box against a provider API. Against 61 seeded defects that are distinguishishable from a correct implementation, the generated suite detects 100%, where random sequences with the same call budget reach 56% and a hand-written integration suite reaches 69%; random sequences given ten times the budget still reach only 67%. Running the same suite between two providers turns the comparison into a search, and it returns short executable witnesses for divergences the two documentation sets imply but neither states, including one that breaks the common assumption that a single adapter interface can sit over both, because closing a hold and releasing its remainder is a capture on one provider and a cancel on the other. We report what we could not do: no provider sandbox credentials were available, so every result here concerns documented behavior, and the suite that would test the providers themselves is part of what we release.