Promises are prose. These are proofs.
Every gateway says it meters exactly, bills fairly, and fails over safely. Sage is built so those claims are machine-checked on every change — proven with a model checker, explored exhaustively over a bounded universe, or swept over thousands of adversarial inputs. Nothing on this page is merely asserted; each property names the artifact that discharges it, and a change that weakens one fails the build. The full specification and mapping live in the repository at services/proxy/specs/SPEC.md.
Your money, conserved.
The prepaid credit lease — every admission, settlement, refund, timeout, top-up, and account close — is model-checked with TLA⁺/TLC over all interleavings of concurrent replicas, the payments service, and the stale-lease reconciler. The Stripe cents boundary is proven with Kani for all inputs, symbolically.
| Property | Claim | Discharged by |
|---|---|---|
| Conservation | Money is never created or destroyed: credits ≡ balance + live reservations + kept charges, under every interleaving. | TLC, full state space |
| Exactly-once | Settle, release, and timeout are mutually exclusive per request — a worker's settle racing another replica's reconcile has exactly one winner. | TLC, mutation-tested |
| Charge-exact | The ledger keeps exactly the metered actual — an under-run refunds precisely the unused reservation, never a silent undercharge. | TLC + 20k seeded pairings |
| Cents boundary | The Stripe cents→micros conversion is exact, sign-preserving, monotone, and saturates instead of wrapping — for all 64-bit inputs. | Kani bounded proof |
Failover that cannot overstep.
Every request's failover plan is decided by one pure routing kernel, checked exhaustively over its whole bounded universe — 69,984 routing decisions, every small route table × entitlement × wire. The proactive circuit breaker is a pure state machine checked over all 390,625 bounded event sequences against an independent reference model.
| Property | Claim | Discharged by |
|---|---|---|
| Entitlement | Failover never widens entitlement: no org is ever served — or billed for — a model outside its allowlist, not even via a fallback. | 69,984 decisions, exhaustive |
| Protocol-true | No hop ever crosses provider protocols; a cross-protocol fallback is dropped, never translated. | same enumeration |
| Residency | An org pinned to data-residency regions provably cannot reach an upstream outside them — across failover too; undeclared upstreams are excluded fail-closed. | 1,176 decisions, exhaustive |
| Breaker safety | The circuit breaker only reorders work away from a struggling upstream — it can never turn a servable request into an error, and a recovered upstream is always probed back in. | 390,625 sequences vs. reference model |
Byte-for-byte in. Exactly metered out.
The claim behind everything Sage bills: your bytes pass through untouched while usage is read from the frames flowing past. That relay, the rate limiter's arithmetic, and the deploy-time drain are pinned the same way.
| Property | Claim | Discharged by |
|---|---|---|
| Byte-transparency | The streamed body the client receives is byte-identical to what the provider sent — chunk boundaries included — for adversarial chunkings, split characters, and invalid UTF-8. | driven through the real stream |
| Metering exactness | Metered usage is invariant under every re-chunking of the wire: a split mid-frame or mid-character can never change what is billed. | every single cut, exhaustive + 2k multi-cuts |
| Rate-limit bound | Over every sub-interval of adversarial arrival schedules, admissions never exceed burst + rate × window. | seeded sweeps, all-pairs windows |
| Receipt chains | Every settled call appends a payload-free receipt to its org's SHA-256 hash chain — any alteration of the history behind the chain head is detected on read. | 6,400-tamper sweep |
| Streaming-safe drain | A deploy never refuses a routed request and never severs a stream mid-generation; every SIGTERM reaches a clean stop. | TLA⁺/TLC, mutation-tested |
Honesty is part of the method.
A verification page that hides its edges is marketing. These are ours, verbatim from the specification: the TLA⁺ layers are design-level — they check the protocol as mapped from the implementation's guarded atomic operations, and that mapping is itself executed: a differential harness drives the real conditional writes against a real DynamoDB engine on every relevant change and re-derives the model's invariants from the stored state. What remains assumed is the production fleet's behavior under throttling and partial availability — DynamoDB Local is the reference engine for the API, not the fleet. Float-domain arithmetic is sweep-discharged, not symbolically proven — Kani is reserved for the integer money boundary. Exhaustive checks cover bounded universes, chosen so contention and interleaving are forced, and mutation-tested so a weakened guard cannot pass silently. The drain model covers the cooperative shutdown path; the platform's kill grace period is sized around it, not proven within it.