Blind Tab
A Formally Verified Mechanism for
Opaque Dynamic Pricing in Prepaid Commerce
White Paper
February 2026
No Way Labs
Prepaid commerce platforms—from corporate meal programs to subscription-based retail—suffer from a structural misalignment between consumer budgets and merchant pricing. Consumers face stranded balances and budget exhaustion; merchants face unpredictable volume and limited pricing flexibility. We introduce the Blind Tab, an opacity-preserving bilateral pricing mechanism that dynamically allocates prices between merchant-defined bounds using real-time signals. The mechanism is formally verified using interactive theorem proving, establishing mathematical guarantees on budget safety, fairness, and resistance to strategic manipulation. Large-scale simulations demonstrate a 16.6 additional transactions per consumer per cycle improvement in consumer purchasing capacity while maintaining a budget-exhaustion rate below 1.3%. This paper presents the mechanism’s design philosophy, its verified economic guarantees, and empirical evidence of its impact—positioning the Blind Tab as infrastructure for the next generation of platform-mediated commerce.
Prepaid commerce is a multi-billion dollar segment spanning corporate dining programs, campus meal plans, food hall passes, subscription coffee services, and retail gift ecosystems. Despite their prevalence, these platforms share a common set of structural inefficiencies.
When consumers load funds onto a prepaid account, they enter a fixed-budget consumption cycle. Two failure modes emerge:
Stranded balances. Consumers under-spend and leave value on the table—a windfall for the platform, but a source of friction that erodes trust and discourages re-enrollment.
Budget exhaustion (“budget cliff”). Consumers spend aggressively early in the cycle, then hit a hard stop before the cycle ends. They lose access to merchants they frequent, and merchants lose volume in the final days of the period.
Both outcomes degrade the consumer experience and reduce merchant transaction volume.
Merchants in prepaid ecosystems typically post fixed prices. This rigidity creates missed opportunities:
During low-demand periods (e.g., mid-afternoon at a coffee shop, off-peak hours at a fast-casual counter), merchants cannot lower prices to attract volume without publicly discounting—which risks devaluing their brand and creating reference-price anchoring.
During high-demand periods, merchants cannot capture the willingness-to-pay of consumers with ample remaining budgets.
Loyalty goes unrewarded at the pricing layer. Repeat customers pay the same as first-time visitors, even though retention is cheaper than acquisition.
Dynamic and personalized pricing could solve these problems, but it introduces a new one: consumer backlash. Visible personalized pricing triggers fairness objections, strategic manipulation (consumers gaming signals to get lower prices), and regulatory scrutiny. The result is that most platforms avoid it entirely, leaving value on the table.
The Blind Tab resolves this tension through a single design principle: intentional opacity.
Each merchant defines two price points for their offerings:
A floor price—the minimum they are willing to accept for a transaction.
A target price—their preferred list price.
When a consumer initiates a transaction, the Blind Tab platform computes a personalized price between the floor and the target. The consumer does not observe this price at the point of sale. They see only that the transaction was approved and their balance was debited. The merchant receives at least their floor price, always.
This opacity is not incidental—it is the mechanism’s core innovation. By removing price visibility, the Blind Tab:
Eliminates reference-price backlash. Consumers cannot compare personalized prices, so fairness objections do not arise.
Prevents strategic manipulation. Consumers cannot reverse-engineer the pricing logic to game lower prices.
Enables genuine demand responsiveness. The platform can shift prices in real time based on market conditions without any participant needing to “accept” a visible price change.
The Blind Tab’s pricing engine ingests three real-time signals to determine where a given transaction’s price falls within the floor-to-target spread:
Consumer capacity. A measure of the consumer’s remaining spending power relative to their position in the budget cycle. A consumer with ample balance remaining relative to the time left in their cycle can absorb prices closer to the target; a consumer nearing exhaustion receives prices closer to the floor.
Merchant demand. A real-time indicator of the merchant’s current transaction load. During peak periods, prices shift upward to reflect scarcity; during off-peak periods, prices soften to attract volume.
Consumer loyalty. A measure of the consumer’s visit concentration with the specific merchant. Repeat customers receive preferential pricing as a retention mechanism; infrequent visitors pay closer to the target.
These three signals are combined through a proprietary dynamic allocation algorithm that outputs a price in the interval [floor, target] for each transaction. If the computed price would exceed the consumer’s remaining balance, the transaction is declined—the consumer is never overdrawn.
The platform captures a fee as a percentage of the spread—the difference between the transaction price and the merchant’s floor. This aligns the platform’s incentives with value creation: the platform earns more when it successfully matches consumers with merchants at prices that work for both sides, rather than by extracting from either party.
A critical product advantage: the Blind Tab does not require consumers to deposit their full budget upfront. The consumer (or their employer) commits to a cycle budget—say, $500 per month—but the platform only charges their linked payment method as transactions occur. Funds are drawn per-transaction or settled in periodic batches (daily, weekly), much like a standard debit card.
This works because the mechanism’s formal guarantees depend on the committed budget B and the remaining unspent amount bk = B − cumulative spend, not on whether dollars have been pre-deposited. The capacity signal, which drives pricing, needs only to know the consumer’s committed ceiling and how much of it has been consumed. Whether those dollars sit in an escrow account or are drawn from a bank account at settlement time is a payments-layer concern that does not affect the mechanism’s properties.
This eliminates a major adoption barrier. Traditional prepaid programs lock up hundreds of dollars on day one—money the consumer cannot use elsewhere for the duration of the cycle. The Blind Tab’s pay-as-you-go model means consumers commit to a spending ceiling, not an upfront deposit. For employer-funded programs, this further simplifies treasury: the company commits stipend amounts per employee, and actual payouts flow as employees transact, aligning cash outflows with real consumption.
The Blind Tab mechanism has been formally verified using interactive theorem proving—the same mathematical verification methodology used in aerospace, cryptography, and chip design. Six economic properties have been proven to hold for all possible inputs, not just tested on sample data, but mathematically guaranteed to hold in every scenario the mechanism can encounter.
P1: Budget Safety
No consumer will ever be charged more than their remaining balance.
Every transaction price is bounded above by the consumer’s current balance. If a transaction would result in an overdraft, it is declined. This is not a software check—it is a structural property of the pricing function itself.
P2: Sequential Budget Safety
Over any sequence of transactions within a cycle, the total amount charged will never exceed the consumer’s initial budget.
This extends P1 to the full lifecycle. Across an entire prepaid cycle—regardless of how many transactions a consumer makes, at which merchants, on which days—total spend is provably bounded by the loaded budget. No sequence of individually-safe transactions can combine to produce an unsafe outcome.
P3: Merchant Revenue Protection
Every approved transaction pays the merchant at least their stated floor price.
If a transaction is approved, the merchant is guaranteed to receive no less than their floor. The mechanism will decline a transaction rather than pay below the floor. Merchants can set their floor with confidence that it represents a hard minimum.
P4: Consumer Purchasing Advantage
In expectation, a consumer can afford at least as many transactions under the Blind Tab as they could under posted (target) pricing.
Because the mechanism’s average price is strictly below the merchant’s target price, consumers’ budgets stretch further. The same budget that affords N transactions at posted prices affords at least N transactions—and typically more—under the Blind Tab.
P5: Resistance to Consumer Timing Manipulation
A consumer who artificially delays transactions to concentrate spending at the end of their cycle faces weakly higher prices, making the strategy self-defeating.
The capacity signal is designed so that hoarding budget and spending late does not produce lower prices. A consumer who delays transactions reduces their remaining time window, which the mechanism interprets as higher capacity—resulting in prices closer to the target, not the floor.
P6: Resistance to Merchant Floor Inflation (Under Competition)
In a competitive market, a merchant who artificially inflates their floor price will see weakly lower revenue than one who reports truthfully.
Under competitive conditions—where consumers have substitute merchants available—inflating the floor raises the transaction price, which reduces volume. The volume loss weakly outweighs the per-transaction gain, making inflation unprofitable.
These properties were formalized and proven in Lean 4, a state-of-the-art interactive proof assistant, compiled against the Mathlib mathematical library. The verification covers the complete pricing function, all signal computations, and the sequential composition of transactions. This level of formal assurance is, to our knowledge, unprecedented in marketplace mechanism design.
To validate the mechanism’s practical performance beyond its theoretical guarantees, we conducted large-scale Monte Carlo simulations modeling realistic prepaid commerce environments.
The simulation models a population of consumers interacting with merchants across multiple categories (e.g., coffee, fast-casual, and specialty vendors) over repeated budget cycles. Consumer budgets, transaction frequencies, and merchant preferences are drawn from realistic distributions. Each experiment runs hundreds to thousands of independent cycles to produce statistically robust estimates.
| Metric | Result | 95% CI |
|---|---|---|
| Additional transactions per consumer per cycle | +16.6 | [16.4, 16.7] |
| Budget-exhaustion (“cliff”) rate | 1.29% | [1.28%, 1.30%] |
Consumers gain an average of 16.6 additional transactions per cycle compared to posted pricing. At the same time, the rate at which consumers exhaust their budgets before the cycle ends is held to just 1.29%—meaning over 98% of consumers maintain purchasing power through the entire cycle.
We mapped the mechanism’s budget-safety performance across a range of budget levels and cycle lengths:
| Budget Level | 7-Day Cycle | 14-Day Cycle | 30-Day Cycle |
|---|---|---|---|
| Conservative | < 0.1% | < 0.5% | < 3.5% |
| Standard | < 0.1% | < 0.1% | < 1.3% |
| Generous | < 0.1% | < 0.1% | < 0.5% |
The mechanism operates safely across a wide range of configurations. Even at conservative budget levels with 30-day cycles, the cliff rate remains manageable. At standard and generous budget levels, exhaustion is near-zero.
We tested two consumer manipulation strategies:
Front-loading (concentrating purchases early in the cycle): Consumers who front-load lose approximately 0.25 transactions per cycle. The strategy is self-defeating—early spending depletes the balance, triggering the capacity signal to restrict later purchases.
Back-loading (hoarding budget for late-cycle spending): The capacity signal adjustment makes delayed spending weakly more expensive, consistent with the formal guarantee (P5).
We also tested merchant floor inflation under varying levels of competition. Under competitive conditions with multiple substitute merchants per category, floor inflation converges to an equilibrium where the inflating merchant’s market share loss offsets any per-transaction gains—validating P6 empirically.
The platform generates sustainable revenue through its spread-based fee, producing consistent per-cycle income that scales with transaction volume. The fee structure creates no misalignment: the platform earns when consumers transact and merchants receive above their floor.
The simulation results reveal a mechanism that creates value for every participant in the ecosystem.
The Blind Tab stretches budgets. A consumer who could afford roughly 12 lunches per month at posted prices can afford closer to 29 under the mechanism—without sacrificing quality or choice. Budget exhaustion virtually disappears: over 98% of consumers maintain purchasing power through the entire cycle. And because pricing is opaque, consumers never face the anxiety of comparing prices or wondering if they got a fair deal. Every transaction is simply approved or declined—no sticker shock, no regret.
The pay-as-you-go funding model means consumers are never asked to lock up hundreds of dollars on the first of the month. They set a ceiling and spend as they go, exactly like a debit card with an intelligent budget assistant working behind the scenes.
Every additional consumer transaction is also a merchant transaction. The 16.6 extra transactions per consumer per cycle translate directly into increased foot traffic and volume for participating merchants—particularly during off-peak windows, when the demand signal softens prices to attract consumers who might otherwise skip a visit.
Merchants retain full control over their economics: they set the floor (their minimum acceptable price) and the target (their preferred price), and the mechanism never pays below the floor. This is a hard guarantee, not a policy—it is mathematically impossible for the mechanism to approve a below-floor transaction.
The loyalty signal rewards merchants who build repeat relationships. A consumer who visits the same coffee shop every morning receives progressively better pricing at that shop—driving retention without requiring the merchant to run visible promotions or punch-card programs that erode perceived value.
Critically, merchants can offer dynamic, demand-responsive pricing without any brand risk. Because consumers never see the price, a merchant can effectively run off-peak discounts without publicly advertising lower prices, avoiding the reference-price anchoring that makes traditional discounting a race to the bottom.
The platform earns a percentage of the spread on every transaction. Because the mechanism increases total transaction volume, the platform’s revenue grows with consumer engagement—not by raising take rates on merchants. The verified properties (budget safety, merchant floors, anti-gaming) serve as trust infrastructure that reduces churn on both sides of the marketplace and provides a defensible competitive moat.
While the Blind Tab is a general-purpose mechanism for any prepaid commerce environment, several domains present immediate opportunities.
Companies that provide meal stipends or cafeteria credits to employees can deploy the Blind Tab across food halls, on-campus vendors, or partner restaurant networks. The mechanism maximizes the number of meals each employee can afford from their stipend while ensuring every vendor receives at least their cost-plus floor.
Subscription coffee programs (e.g., monthly coffee passes) are a natural fit. The Blind Tab can dynamically price across a network of participating cafes, rewarding loyal customers with lower per-cup costs during off-peak hours while allowing premium pricing during the morning rush—all invisible to the consumer.
Multi-vendor food halls and fast-casual networks struggle with uneven demand distribution across vendors and time slots. The Blind Tab’s demand signal naturally shifts consumer traffic toward underutilized vendors and off-peak windows by making those transactions less expensive.
University and hospital meal plans typically offer fixed-price dining or declining-balance accounts. The Blind Tab transforms these into dynamic systems that stretch student and staff budgets further while giving campus vendors pricing flexibility they currently lack.
The mechanism generalizes to any prepaid marketplace: retail gift card ecosystems, wellness and fitness credit programs, transportation passes, or any environment where consumers load a fixed budget and transact across a network of merchants.
| Feature | Traditional Prepaid | Dynamic Pricing | Blind Tab |
|---|---|---|---|
| Personalized pricing | No | Yes (visible) | Yes (opaque) |
| Consumer backlash risk | None | High | None |
| Budget safety guarantee | None | None | Formally proven |
| Merchant floor protection | None | Varies | Formally proven |
| Anti-gaming guarantees | None | None | Formally proven |
| Verification methodology | Testing | Testing | Theorem proving |
The Blind Tab is, to our knowledge, the only marketplace pricing mechanism with formal mathematical proofs of its economic safety properties. This is not a claim of “tested on millions of transactions”—it is a guarantee that holds for every possible transaction, consumer, and merchant state the system can encounter.
The Blind Tab represents a new class of marketplace mechanism: one that is opaque by design, formally verified, and empirically validated. It resolves the fundamental tension between personalized pricing and consumer acceptance by making price discrimination invisible—and proves, mathematically, that this invisibility does not come at the cost of safety or fairness.
For platform operators, the Blind Tab offers a defensible, verifiable pricing engine that increases transaction volume, reduces budget-exhaustion friction, and generates sustainable platform revenue. For merchants, it guarantees a revenue floor while enabling demand-responsive pricing without brand risk. For consumers, it stretches prepaid budgets further without requiring any awareness of, or engagement with, the pricing mechanism.
The formal verification of six core economic properties—compiled and checked by machine, not asserted by hand—sets a new standard for trust in platform-mediated pricing. We believe this combination of opacity, verification, and empirical performance positions the Blind Tab as foundational infrastructure for the next generation of prepaid commerce.
For technical inquiries, partnership opportunities, or access to the formal verification certificates, please contact No Way Labs.