Tests sample the inputs you thought of. A proof checks every input there is. Here is how Bounded turns a spend cap or a conservation rule into a thing a solver signs off on before it ships.
poof.new, our consumer builder, runs on Bounded. When someone builds an app on Bounded that holds a balance or caps a spend, the rule that protects the money is not a line in our code that a reviewer has to remember to keep. It is a property a solver checked against every possible input before the app shipped. This post is about why that distinction is the whole game, and how it works.
Tests sample. Proofs quantify.
A unit test is one example. You pick an input, run the code, assert on the output. Good tests pick good examples. But a test that passes only tells you the code works for the cases you thought of. The bug is in the case you didn't.
Money bugs live in the cases you didn't think of. The concurrent refund. The negative amount. The transfer that credits before it debits. The off-by-one at the exact edge of a rolling window. You can write a hundred tests and still ship the one input that drains the account.
A proof does not sample. It quantifies over every input there is. "For all sequences of writes, the total balance is unchanged" is either true, or the solver hands you the exact sequence where it is false. There is no case you forgot, because "for all" has no exceptions. Bounded is built on that difference.
You declare the guarantee, not the enforcement
In Bounded you write the guarantee once, on the collection, as an invariant in policy.json. Here is a per-agent hourly spend cap:
policy.json
"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": "spend_cap",
"field": "amount", "windowSeconds": 3600, "limit": 100,
"scopeVariable": "$agentId" }
]
}
That says: sum the amount field over any 3600-second window, per agent, and it never exceeds 100. The collection is append-only (update and delete are "false"), so the history the cap is computed from cannot be rewritten. There are six boundary types, plus the windowSum derived-aggregate declaration. Two boundary types with PROVED obligations used below:
- conserve: the total of a field across the collection never changes. Value can move between accounts in one atomic batch, but nothing mints it and nothing burns it.
- rollingSum: the sum over a sliding time window stays under a limit. Add
scopeVariable and every agent gets its own budget instead of sharing one pool.
The other four boundary types (flowBound, bound, tenantTag, tenantEdge) cover cumulative inflow/outflow limits, hard ceilings, and multi-tenant isolation. Proof coverage varies by type and shape: flowBound reports UNKNOWN despite runtime enforcement, and a .values map bound reports UNKNOWN. windowSum is best-effort derived maintenance, not a write-gating cap or proof. Read each verifier item’s proofStatus.
What the solver actually proves
Run bounded verify and it compiles the policy into proof obligations and discharges them with Z3, an SMT solver. A clean run for the cap above:
terminal
$ 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 · holds for all inputs
Read the last line. It is not "we ran some tests." It is a statement about every possible sequence of appends: if the runtime admits only nonnegative records and the projected window sum is within the limit, the resulting sum stays within the limit, for all appends.
When an obligation fails you do not get a vague warning. You get the counterexample, the exact assignments that break the property:
terminal
checkAuthRequired(create) DISPROVED (52ms)
counterexample: @user.id = null,
@newData.ownerId = null
null == null satisfies "ownerId == @user.id"
suggestion: add "@user.id != null" before the ownership check
That is a real class of bug. An ownership rule like ownerId == @user.id looks airtight until an unauthenticated caller writes ownerId: null and null == null is true. The solver finds it and tells you to prepend @user.id != null. You do not fix it by deleting the check. You fix the property. The counterexample is showing you a write production would have accepted.
The gate is not advisory
This is the part that makes it load-bearing. bounded verify is the loop you run at your desk. bounded deploy runs the same gate again, server-side, and fails closed. A policy whose blocking obligations fail is rejected:
It never ships. You cannot deploy a backend the prover can break. The guarantee is checked at the boundary where code becomes production, not left as a comment that says "be careful here."
And then, at runtime
Proof at deploy is half of it. The other half is enforcement on every write. Invariants are transaction postconditions. They bind every write path: direct writes, functions, scheduled jobs, hooks, and multi-document batches, where the whole batch commits or nothing does. The spend cap at runtime:
terminal
set amount=60 ✓ committed (window 60/100)
set amount=60 ✗ 409 spend_cap (60+60 = 120 > 100)
set amount=40 ✓ committed (window 100/100)
set amount=1 ✗ 409 spend_cap (100+1 = 101 > 100)
The second 60 is byte-identical to the first and still rejected, because the cap is about the window, not the write. A violation is a 409 that names the invariant. Nothing partial is applied. There is no admin flag that turns it off and no server-side path that skips it. conserve has no privileged mint even for the owner, even server-side, because a mint escape hatch is exactly the hole you are trying to close.
Why I care
I have shipped backends where the money rule was a function three call-frames deep that someone could forget to call. Bounded moves that rule to a place where forgetting is impossible: it becomes a property of the data, proven before deploy, enforced on every write, failing closed. Tests told me my code worked on Tuesday. The proof tells me it works for every input, including the ones I will never think of.
If your backend touches balances, spend, or anything that has to conserve, that is the guarantee worth having. Bounded is where I put it, and it is what poof.new is built on.