03Docs

Quickstart

From nothing to a complete web app with a proven spending cap. The fastest path is one paste to your coding agent; every step below is what the agent does across client, policy, deployment, and testing.

The one-paste flow

Hand the whole setup to a coding agent (Claude Code, Codex, Cursor, or anything that can run a shell), the same prompt the homepage uses:

Paste into Claude Code, Codex, or your preferred AI agent.

The agent builds the client UI, installs the SDK and CLI, declares a policy with your boundaries as invariants, fixes counterexamples, deploys the governed runtime and web site, then tests the complete flow. The rest of this page is that sequence by hand.

Step by step

  1. Install the CLI

    curl -fsSL https://get.bounded.sh/install.sh | sh

    One binary. No account creation, no browser, no API keys.

    The installer also starts the loopback dashboard daemon on 127.0.0.1:8085 by default. Use BOUNDED_DASHBOARD=0 only when you do not want a background local daemon.

  2. Identity is automatic

    bounded init writes public bounded.json. The first auth command generates or loads its selected key source, usually ~/.bounded/credentials. The keypair is your identity, agents go from zero to deployed without a human auth step. Later, when you want billing, account recovery, dashboard, or teams, run bounded link. For headless agents, run bounded link --email you@example.com; the CLI emails an OTP, reads it from stdin, and approves the same fingerprint checked device flow. Linking is never required to build, verify, or deploy.

  3. Initialize a project

    bounded init

    Creates policy.json, the single file that defines your collections, auth rules, and invariants. Here is a starter policy with an hourly spending cap:

    policy.json
    {
      "agents/$agentId/spend/$spendId": {
        "fields": { "amount": "UInt", "memo": "String?" },
        "rules": {
          "read":   "@user.id != null && $agentId == @user.id",
          "create": "@user.id != null && $agentId == @user.id",
          "update": "false",
          "delete": "false"
        },
        "tier": "durable",
        "invariants": [
          {
            "type": "rollingSum",
            "name": "spend_cap",
            "field": "amount",
            "windowSeconds": 3600,
            "limit": 100,
            "scopeVariable": "$agentId"
          }
        ]
      }
    }
  4. Build the client flow

    npm i @bounded-sh/client

    Build the sign-in, spend-history, add-spend, remaining-budget, loading, and boundary-refusal states. Initialize the client with the app id from bounded.json; use @user.id as the authenticated path identity.

  5. Verify, the proof report

    bounded verify, proof report
    $ bounded verify
    
    policy.json, 1 collection, 1 invariant
    
      create rule is satisfiable                                PROVED   (38ms)
      create requires authentication                            PROVED   (41ms)
      read requires authentication                              PROVED   (40ms)
      transaction postcondition spend_cap
        append-only rolling limit algebra                       PROVED  (106ms)
    
    4 obligations · 0 failed · blocking proof gate passed

    Every constraint compiles to proof obligations checked by an SMT solver (Z3). Green is a proof over all inputs; a failure comes back as DISPROVED with a concrete counterexample, the exact variable assignments that break your rule. Read the report, strengthen the policy, re-run. verify is your fast feedback loop before the deploy gate.

  6. Deploy

    $ bounded deploy --create --name lucid-prairie-41
    
    ✓ policy deployed to lucid-prairie-41 (revision 3)
      recorded project defaults in bounded.json (safe to commit)
    
    Next:
      bounded verify
      bounded data set --path agents/<your-id>/spend/s1 --data '{"amount":60}'
      bounded dashboard

    deploy is a separate command. It validates and compiles your policy (a malformed policy, an impossible tier/invariant pairing, or an uncompilable rule is rejected), and the server re-runs the prover’s deploy gate before the policy ships. A blocking DISPROVED obligation is rejected, fail-closed. From there the runtime enforces every rule and invariant atomically (see the loop).

  7. Publish the web app

    npm run build
    bounded site deploy ./dist --app-id <id>
    bounded domains slug my-app --app-id <id>

    Bounded serves the built static client at https://my-app.bounded.page. SPAs and prerendered exports work; request-time SSR/ISR or framework server routes need an external frontend host. React Native follows the same SDK and policy flow but keeps native binary release in the mobile toolchain.

  8. Write, and watch the cap hold

    # Use the authenticated principal required by $agentId == @user.id.
    $ USER_ID="$(bounded whoami --json | jq -r .id)"
    
    # Local/staging uses full error disclosure; production defaults to the same
    # stable code with policy details hidden.
    $ bounded data set --path "agents/$USER_ID/spend/s1" --data '{"amount": 60}'
    ✓ committed
    
    $ bounded data set --path "agents/$USER_ID/spend/s2" --data '{"amount": 60}'
    ✗ 409 postcondition failed: invariant "spend_cap"
          requires rolling sum(agents/$agentId/spend/$spendId.amount) <= 100
      rollingSum(amount) over 3600s: 60 + 60 = 120 > limit 100
      nothing committed

    Rejections are atomic and fail-closed. See For agents for the full failure-semantics table and set-many composition. Repeat the allowed and over-cap cases through the deployed UI and confirm it renders the 409 as an intentional product outcome rather than retrying it.

Where to go next

  • Client SDK and hosting & domains, wire and publish the complete web app.
  • Policy reference, every key in policy.json: rules, fields, tiers, hooks, roles, constants, environments.
  • Invariants, the six boundary types (conserve, rollingSum, flowBound, bound, tenantTag, tenantEdge) plus the windowSum derived aggregate, with real syntax and coverage details.
  • Verification, the full obligations table, counterexamples, and the two-layer coverage model.
  • For agents, failure semantics, atomic set-many, in-batch composition.