# Retention/LTV Verification Results

Status: **checked 2026-09-23 — all safety properties hold in the bounded model;
all four reachability probes produced their exact expected counterexample.**

## Expected verification matrix

| Configuration | Purpose | Required result |
|---|---|---|
| `Model.cfg` | All safety invariants | ✅ 9,239,617 generated / 1,796,432 distinct / depth 15 |
| `ReachRequired.cfg` | Required update is reachable | ✅ exact violation; 2 states / depth 2 |
| `ReachOptional.cfg` | Optional update is reachable | ✅ exact violation; 4 states / depth 3 |
| `ReachCore.cfg` | Accepted free core action is reachable | ✅ exact violation; 516 generated / depth 6 |
| `ReachPremium.cfg` | Accepted authorized premium action is reachable | ✅ exact violation; 1,269 generated / depth 6 |

The runner treats parse errors, timeouts, different invariant failures, and
unexpected passes as failures. Logs are written to
`formal/retention-ltv/out/*.log` and remain untracked.

## Implementation obligations derived from the model

Passing the model only supports the design if implementation preserves these
refinement points:

1. Compare ordered build/version values on the server; do not compare semantic
   version strings lexicographically.
2. Once a required policy is applied at a safe point, block all new mutations,
   not merely navigation to selected screens.
3. Use a unique `eventId` index and atomic upsert/insert behavior before any
   aggregate consumes the event.
4. Reserve/debit premium usage atomically on the server with an idempotency key.
5. Keep core-action code paths independent of the AI wallet.
6. Treat subscription webhooks as idempotent entitlement facts; analytics events
   cannot grant access.
7. Derive cohorts only from accepted events and publish metric definitions.

## Required implementation verification

Before launch, add contract tests for every event producer, concurrency tests for
duplicate ingestion and wallet debits, endpoint tests for all version boundaries,
mobile UI tests for optional/required/safe-point behavior, and end-to-end tests
using real non-admin accounts. Production canaries must confirm dashboard counts
against raw events before product decisions use them.

## Evidence record

| Evidence | Value |
|---|---|
| Run date | 2026-09-23 |
| Model checker | TLC2 2.19, TLA+ tools v1.7.4; jar SHA-256 verified |
| Runtime | Eclipse Temurin OpenJDK 21.0.12.1, Windows x86_64, 8 workers |
| Command | `npm run verify:retention` |
| Spec SHA-256 | `3eb2ed25d15d045725ed1196269828abc38982fe8852c2ea6e3e510c2280dc96` |
| Concatenated config SHA-256 | `e38023432a116b1dcd51ecc295789c1f410e59b4ef759097b2af4638bec58a6d` |
| Logs | `formal/retention-ltv/out/*.log` locally (ignored generated evidence) |

The main configuration exhausted its finite state graph with no error. That is
strong evidence for the specified control-plane design within the documented
bounds; it remains neither an unbounded mathematical proof nor verification of
future production code.