Guarantees

Tollgate makes specific claims: a strict account never spends past its allocation, a refusal never charges, every committed charge is billed once, and the ledger always balances. This page explains how each kind of claim is checked, maps the whole contract to its proofs, and states what is not established.

The contract itself is the invariants: 41 numbered statements, each naming how it is enforced and the tests that witness it. Violating one is a defect even if every test passes.

How an invariant is enforced

Every invariant states its enforcement, chosen from a ladder, highest first:

1. Unrepresentable by construction. Types and guards make the wrong state impossible to write. A Reservation can be committed or cancelled, not both, because each consumes it.
2. Enforced inside the owning component. The store, the runtime or the admission map refuses the violation, whatever its caller does.
3. A tested convention, hardened by mutation testing. Used only when neither of the above is possible, because a rule that relies on every caller's discipline drifts.

Tests verify enforcement; they don't replace it.

The evidence

Timed performance runs locally rather than in CI on purpose: shared runners can't produce comparable timings, and a gate that fails at random teaches people to ignore it. CI still compiles every benchmark and enforces the allocation counts.

The invariant map

Each invariant, and the Lean modules whose theorems it cites. 27 of the 41 rest partly on a machine-checked proof. The others are enforced by types, by their owning component, or by tested convention, as each one states. A dash means no proof is claimed, not that the invariant is unchecked.

This table is checked: a test fails if it stops matching INVARIANTS.md row by row, including which theorems each invariant cites, or if a module, theorem or invariant count stated on this page or in the README goes stale.

What the proofs cover, and what they don't

A proof is only as strong as what it states. So the models are themselves mutation-tested: check_lean_mutants changes one operator in one transition at a time, checks the mutated model with Lean, and requires a theorem to fail. Only definition bodies are mutated; signatures are types, and specifications (definitions of type Prop) are what the theorems claim, so weakening one would prove nothing. This pushes the proofs to pin down exact behaviour: not only that a limit refuses what exceeds it, but that it accepts exactly what fits. Every mutant that typechecks fails a theorem, apart from one that is equivalent by construction and is listed in formal/lean/mutants-allowed.txt with its reason.

The Lean models use exact integer arithmetic and atomic transitions. A green proof says that a modeled transition preserves its property. It does not say that the Rust or SQL implements that transition faithfully; the Rust property, backend-parity and mutation tests make that argument, and each invariant says which ones.

The models deliberately leave out scheduling, data-structure internals, finite-width overflow, SQL and the network. Those are separate Rust obligations, and the formal models README lists them module by module.

What is not claimed

• No end-to-end refinement proof. There is no machine-checked link from the Lean models to the Rust code. The connection is tests, and tests support a proof-to-code argument; they are not proof.
• Performance numbers are host-specific. They are microbenchmarks on a controlled host, not HTTP latency guarantees on yours. Ratios travel better than absolutes; performance records the conditions.
• Losing the process loses unflushed usage. A committed charge is emitted on every exit path Rust controls, including a panic that unwinds. A killed process, or a panic = "abort" build that aborts, loses what it had not flushed. Its leases are then forfeited as settlement loss, so the account is never credited for work that may have run. Invariants 9 and 13 state this boundary.
• Trusted inputs stay trusted. The proofs and tests assume what their invariants name: an atomic store transaction, accurate clocks, verified credentials, and correct cryptographic primitives.

Checking it yourself

cargo test --workspace --all-features         # tests, witnesses, parity, docs checks
./scripts/check_formal.sh                     # the Lean proofs
./scripts/check_formal_mutants.sh             # mutation testing of the Lean models
./scripts/check_mutations.sh --diff main      # mutation testing on a branch
./scripts/check_perf_thresholds.sh            # timed gates, on your own host

Contributing lists every gate.