FORMAL MODEL EVIDENCE · V1

Make the execution invariants reviewable and executable.

A vendor-authored TLA+ specification documents the intended state machine. A separate TypeScript breadth-first explorer actually checks a bounded finite abstraction and verifies that eight unsafe mutations are detected.

EXECUTED BOUNDED RESULT

PASS: no modeled safe transition violated an invariant

The explorer visited 10,460 distinct states and evaluated 37,354 legal transitions through depth 9. Its frontier is intentionally truncated; this is bounded evidence, not exhaustive proof.

  • Two isolated tenants
  • Two cumulative-budget units per tenant
  • Purchase amounts of one and two units
  • Two retained receipt-signing key generations

CHECKED INVARIANTS

Eight properties, each paired with a rejected mutation

  • PASS budget_conservation — reserved + committed never exceeds the tenant budget
  • PASS consume_at_most_once — one authorization attempt has consume_count <= 1
  • PASS revocation_prevents_reservation — revoked authority cannot create a new reservation
  • PASS unknown_never_restores_authority — an unknown provider outcome never releases budget or restores submission authority
  • PASS release_requires_confirmed_non_success — RELEASED requires a confirmed NOT_SUBMITTED or FAILED outcome
  • PASS late_success_dominates_unknown — a late confirmed success resolves UNKNOWN to COMMITTED without returning budget
  • PASS retained_key_rotation_preserves_receipts — every historical receipt key remains in the retained verification keyring
  • PASS tenant_isolation — a tenant-scoped transition cannot mutate another tenant

MUTATION CONTROLS

The checker must fail when a safety rule is deliberately broken

The test runner injects overspend, double-consume, post-revocation reservation, UNKNOWN restoration, unsupported release, ignored late success, dropped historical keys and a cross-tenant write. Every mutation is required to trigger at least one named invariant.

  • DETECTED overspend_reservation → budget_conservation
  • DETECTED double_consume → consume_at_most_once
  • DETECTED reserve_after_revocation → revocation_prevents_reservation
  • DETECTED restore_unknown_authority → unknown_never_restores_authority
  • DETECTED release_without_confirmed_non_success → release_requires_confirmed_non_success
  • DETECTED ignore_late_success → late_success_dominates_unknown
  • DETECTED drop_retained_historical_key → retained_key_rotation_preserves_receipts
  • DETECTED cross_tenant_write → tenant_isolation

PUBLIC ARTIFACTS

Review the specification, result and result contract

HONEST BOUNDARY

This is executable evidence, not a mathematical proof

This release does not claim TLC execution, exhaustive state-space coverage, refinement checking against production code, mathematical proof or independent audit. The model abstracts away database failures, network behavior, payment-provider semantics, scheduler behavior and customer gateway implementations. Those remain subject to implementation tests, operational monitoring and external review.