What is Bounded

#One app, the complete stack

A complete Bounded app is more than its policy. Your coding agent owns the whole implementation across three connected layers:

• Client: a client-rendered web UI or React Native / Expo app using @bounded-sh/client for auth, data, files, Functions, subscriptions, and live state.
• Governed runtime: policy.json, optional Functions or long-running runtime code, search, payments, and the rules and invariants every write must pass.
• Delivery: a built static web client on a bounded.page URL or custom domain. React Native keeps native signing and app-store publication in its normal mobile toolchain.

bounded deploy --create --name my-app  # policy + governed data runtime
# optional: bounded functions deploy ... / bounded runtime deploy ...
npm run build                            # static or prerendered web client
bounded site deploy ./dist --app-id <id> # hosted UI on the same app

#The mental model

The governed data and authorization model lives in one file, policy.json. It has two kinds of guarantees, and keeping them straight is the whole game:

• Rules answer “who may act.” Each action (read/create/update/delete) is a boolean expression. A denied write is 403 policy_denied; a denied read is hidden as a successful empty 200 response. Omitted actions default to deny. A rule judges one request in isolation.
• Invariants answer “what must hold across every transaction.” Caps, conservation, bounds, tenancy. They are transaction postconditions: declared once on a collection, enforced atomically on every write path, single writes, set-many batches, hooks, ticks, schedules, even your own migrations. A violation is a 409 invariant_violation; full disclosure and the owner decision log also include the invariant’s declared name.

{
  "spend/$entryId": {
    "fields": { "amount": "UInt", "memo": "String?" },
    "rules": {
      "read":   "@user.id != null",
      "create": "@user.id != null",
      "update": "false",
      "delete": "false"
    },
    "tier": "durable",
    "invariants": [
      {
        "type": "rollingSum",
        "name": "spend_cap",
        "field": "amount",
        "windowSeconds": 3600,
        "limit": 100
      }
    ]
  }
}

That rollingSum invariant is the kind of property no single-write rule can express, it is about the history, not the payload. The prover discharges it once; the runtime then enforces it on every write, forever.

#The loop: declare → verify → deploy

The Bounded workflow has three steps, and the order is deliberate:

1. Declare

   Write (or have your agent write) a policy.json: collections, field types, rules, and invariants. This is the complete governed data and authorization definition, not the UI.

2. Verify

   bounded verify compiles the policy into proof obligations and discharges them with an SMT solver (Z3). It does not say “tests passed”, it proves a property over all inputs and, on failure, hands you the exact assignment that breaks your policy (counterexamples). You read the report and decide whether the policy expresses what you meant.

3. Deploy

   bounded deploy validates, compiles, and pushes the policy. The deployed runtime then enforces every rule and invariant atomically.

#What “fail-closed” means at runtime

The proof report guides you, the deploy gate blocks bad policies, and runtime enforcement is absolute. Once a policy is deployed, the runtime is strict:

Nothing partial is ever applied. The constraints the prover analyzed are the constraints the runtime enforces, because they compile to the same bytecode that executes in the realtime worker.

#The surface

Bounded is offchain-first. Onchain (Solana) is an optional compatibility surface. See the onchain coverage section of Invariants.