Invariants

#Common keys & naming

Every declaration has a type and a field, plus a name and type-specific keys. scope and onchain are available only where that type supports them. A violated invariant’s name is a stable client branch key in both disclosure modes and is also recorded in the owner decision log, so name it like an error code: spend_cap, no_minting, task_tenancy.

#conserve, sums don’t change

The total of an Int/UInt field across the collection is preserved by every transaction. A set-many that debits one document must credit another in the same batch.

{
  "accounts/$accountId": {
    "fields": { "balance": "Int", "owner": "String!" },
    "tier": "durable",
    "rules": {
      "read":   "@user.id != null",
      "create": "@user.id != null && @newData.owner == @user.id && @newData.balance == 0",
      "update": "@user.id != null && @newData.owner == @data.owner && @newData.balance >= 0 && (@data.owner == @user.id || @newData.balance > @data.balance)",
      "delete": "false"
    },
    "invariants": [
      { "type": "conserve", "name": "no_minting", "field": "balance", "materialization": "direct" }
    ]
  }
}

What gets proven: the runtime postcondition is equivalent to “affected after-sum == affected before-sum” (delta equivalence), plus an induction step over arbitrary multi-document write sets, so no batch, of any size, can change the total.

Genesis and transfers: a non-negative fixed-supply ledger must be seeded before the conserve invariant goes live, then redeployed with this final policy. The update rule lets an owner debit their own account or any caller increase another account; conservation forces that credit to be matched by a debit in the same batch, while a non-owner decrease is denied.

#rollingSum, caps over time windows

The sum of a UInt field over a sliding window of the last windowSeconds never exceeds limit. Capped collections are append-only event logs: updates and deletes are rejected (409 append_only), so the history a cap is computed from cannot be rewritten. Platform creation time is the clock.

{
  "agents/$agentId/spend/$spendId": {
    "fields": { "amount": "UInt" },
    "tier": "durable",
    "rules": { "read": "@user.id != null", "create": "@user.id != null", "update": "false", "delete": "false" },
    "invariants": [
      { "type": "rollingSum", "name": "per_agent_hourly_cap",
        "field": "amount", "windowSeconds": 3600, "limit": 100, "scopeVariable": "$agentId" },
      { "type": "rollingSum", "name": "global_daily_cap",
        "field": "amount", "windowSeconds": 86400, "limit": 1000 }
    ]
  }
}

rollingSum requires tier: "durable". Multi-window: declare several rollingSum invariants on the same field with different windows (hourly and daily above), each is tracked and proven independently.

What gets proven: if the runtime admits only nonnegative appended records and the projected window sum is within limit, the resulting sum stays within limit, for every possible sequence of appends.

#windowSum, a readable sliding-window aggregate

Where rollingSum rejects a write that would cross a cap, windowSum is intended to maintain a readable target field on its documented runtime paths. A create in an append-only event collection schedules an addition to target.targetField and a later decrement after windowSeconds. The target can be read, subscribed to, indexed, and sorted for best-effort leaderboards and trending feeds.

{
  "trades/$marketId/events/$eventId": {
    "fields": { "size": "UInt!" },
    "tier": "durable",
    "rules": { "read": "true", "create": "@user.id != null", "update": "false", "delete": "false" },
    "invariants": [{
      "type": "windowSum", "name": "volume_10m", "field": "size",
      "windowSeconds": 600, "target": "markets/$marketId", "targetField": "volume10m"
    }]
  },
  "markets/$marketId": {
    "fields": { "volume10m": "UInt?" },
    "tier": "durable",
    "rules": { "read": "true", "create": "@user.id != null && @newData.volume10m == null", "update": "false", "delete": "false" }
  }
}

Both collections must be ordinary durable, non-session, offchain collections. The event collection is append-only, and the maintained target field should not be user-writable. bounded verify reports proofStatus: UNKNOWN: the declaration is structurally validated and runtime-maintained, but it is not a write-gating cap, an exactness proof, or an SMT proof obligation in this version.

#flowBound, outflow never exceeds inflow

For each value of scopeVariable, cumulative outflow must stay less than or equal to cumulative inflow across two collections. Declare it on the outflow leg; an escrow can then reject releases that exceed that user’s deposits, including both legs staged in one atomic set-many.

{
  "vault/$user/deposits/$id": {
    "fields": { "amount": "UInt!" },
    "tier": "durable",
    "rules": { "read": "@user.id != null && $user == @user.id", "create": "@user.id != null && $user == @user.id", "update": "false", "delete": "false" }
  },
  "vault/$user/releases/$id": {
    "fields": { "amount": "UInt!" },
    "tier": "durable",
    "rules": { "read": "@user.id != null && $user == @user.id", "create": "@user.id != null && $user == @user.id", "update": "false", "delete": "false" },
    "invariants": [{
      "type": "flowBound", "name": "released_le_deposited", "field": "amount",
      "scopeVariable": "$user",
      "inflow": { "collection": "vault/$user/deposits/$id", "field": "amount" }
    }]
  }
}

Both legs are append-only, ordinary durable offchain document collections. Session, storage, and onchain collections are unsupported in v1. The runtime enforces the inequality per partition and rejects an over-release with 409 invariant_violation, but bounded verify reports proofStatus: UNKNOWN as a non-blocking runtime-enforced advisory. Structural validation is not an SMT proof of the flow-bound algebra.

Enabling flowBound validates the declaration, not any pre-existing corpus, and v1 evaluates partition sums from retained append-only rows. Keep partitions bounded operationally and validate or repair inherited data before relying on a newly enabled boundary. Keep both cumulative sums within Number.MAX_SAFE_INTEGER too: individually valid UInt rows can still accumulate past safe integer arithmetic and wedge later evaluation.

#bound, hard ceilings / floors (anti-cheat)

On an offchain authoritative collection, a numeric field must satisfy a fixed comparison against a constant limit. The runtime checks durable writes and the live checkpoint, so a server-authoritative game’s score, a counter, or a level cannot be stored out of range on those surfaces.

{
  "rooms/$roomId": {
    "tier": "checkpointed",
    "fields": { "score": "UInt", "tick": "UInt" },
    "rules": { "read": "@user.id != null", "create": "@user.id != null", "update": "false", "delete": "false" },
    "session": {
      "live": { "module": "pong", "everyMs": 33, "maxLifetimeSec": 1800 },
      "intentRule": "@user.id != null"
    },
    "invariants": [
      { "type": "bound", "name": "score_ceiling", "field": "score", "op": "<=", "limit": 11 }
    ]
  }
}

Proof and runtime coverage: an ordinary scalar offchain bound has an SMT-proved field-bound postcondition (proofStatus: PROVED) and is enforced on durable writes and live checkpoints. A .values map bound checks all map values at runtime but remains UNKNOWN because the verifier does not yet model the universal quantifier. An onchain bound is not enforced; its verifier row is an UNKNOWN warning, not a boundary. See Realtime & live.

#tenantTag, documents carry their tenant

Binds a String field to a path variable: every accepted write to tenants/$tenantId/tasks/$taskId has tenant == $tenantId, always. This is the anchor of tenant isolation, once tagged, data cannot be written under one tenant while claiming another.

What gets proven: an accepted write implies the tag field equals the declared path variable, there is no payload that tags a document with the wrong tenant.

#tenantEdge, references stay inside the tenant

Protects a reference field: the document it points at must live in targetScope and carry the same tenant tag as the source. References can be exact document paths, or bare ids resolved via targetPathVariable.

{
  "tenants/$tenantId": {
    "fields": { "name": "String", "owner": "String!" },
    "rules": {
      "read": "@user.id != null && (@data.owner == @user.id || get(/tenants/$tenantId/members/@user.id).tenant == $tenantId)",
      "create": "@user.id != null && @newData.owner == @user.id",
      "update": "@user.id != null && @data.owner == @user.id && @newData.owner == @data.owner",
      "delete": "@user.id != null && @data.owner == @user.id"
    }
  },
  "tenants/$tenantId/members/$memberId": {
    "fields": { "tenant": "String", "role": "String" },
    "rules": {
      "read": "@user.id != null && (get(/tenants/$tenantId).owner == @user.id || get(/tenants/$tenantId/members/@user.id).tenant == $tenantId)",
      "create": "@user.id != null && get(/tenants/$tenantId).owner == @user.id",
      "update": "@user.id != null && get(/tenants/$tenantId).owner == @user.id",
      "delete": "@user.id != null && get(/tenants/$tenantId).owner == @user.id"
    },
    "invariants": [
      { "type": "tenantTag", "name": "member_tenancy", "field": "tenant", "pathVariable": "$tenantId" }
    ]
  },
  "tenants/$tenantId/tasks/$taskId": {
    "fields": { "tenant": "String", "assigneeRef": "String", "title": "String" },
    "rules": {
      "read": "@user.id != null && get(/tenants/$tenantId/members/@user.id).tenant == $tenantId",
      "create": "@user.id != null && get(/tenants/$tenantId/members/@user.id).tenant == $tenantId",
      "update": "@user.id != null && get(/tenants/$tenantId/members/@user.id).tenant == $tenantId",
      "delete": "@user.id != null && get(/tenants/$tenantId/members/@user.id).tenant == $tenantId"
    },
    "invariants": [
      { "type": "tenantTag", "name": "task_tenancy", "field": "tenant", "pathVariable": "$tenantId" },
      { "type": "tenantEdge", "name": "assignee_same_tenant",
        "field": "tenant", "referenceField": "assigneeRef",
        "targetScope": "tenants/$tenantId/members/$memberId",
        "targetField": "tenant", "targetPathVariable": "$memberId" }
    ]
  }
}

What gets proven: an accepted reference write implies source and target tenant tags match, a task can never reference another tenant’s member. Tag both ends: source and target scopes each need their own tenantTag.

#proofs.attestations, global claims

Invariants attach to one collection. Some guarantees are global: they span every collection and every read or write surface in the policy. Declare those proof-only claims in proofs.attestations. They add bounded verify obligations, but they do not change runtime authorization or invariant enforcement.

{
  "proofs": {
    "attestations": [
      { "claim": "admins cannot read projects they are not a member of",
        "kind": "roleGatedRead", "scope": "projects/$projectId", "role": "members/$memberId" },
      { "claim": "no agent can exceed its daily spend cap",
        "kind": "rollingSum", "scope": "agents/$agentId/spend/$spendId",
        "field": "amount", "windowSeconds": 86400, "limit": 1000, "scopeVariable": "$agentId" }
    ]
  }
}

The older top-level attestations array is still accepted for compatibility, but new policies should use proofs.attestations.

#onchain, coverage claims are verified, not trusted

Each invariant may declare "onchain": "offchainOnly", "onchainUnsupported", or "onchainSupported". Coverage is per type and shape; there is no blanket parity claim between the offchain and onchain runtimes.

The source program implements additional v2+ forms, but the current capability registry marks the known deployed Solana programs as v1. The deploy helper therefore rejects v2 metadata before it can make a path unwritable. Today’s registered onchain subset is direct conserve plus tenantTag. Never treat source support, an onchain bound, or an UNKNOWN advisory as a deployed onchain guarantee. See the full report semantics on the Verification page.

#When not to use an invariant

If the property is about who may act, or about a single write in isolation, it is a rule, not an invariant:

• “Only the owner can update”, a rule (authorization).
• “Balance never goes negative”, a create/update rule (@newData.balance >= 0); pair with conserve if the total must also hold.
• “An agent spends at most 100/hr”, an invariant (rollingSum): no single-write rule can see the history.

Rule of thumb: use read and write rules for who may see or act. Use boundary invariants for cross-write integrity such as caps, conservation, tenant tags, and tenant-safe references; use windowSum only for best-effort derived display data. Complete tenant isolation needs both: membership-gated reads and writes plustenantTag/tenantEdge integrity.