Cloud spend caps example

Simon Willison argues that pay-per-use services should ship with hard budget caps on by default: when spending reaches the limit the service stops, and removing the cap takes an explicit opt-in. Coding agents make it easy to deploy things without thinking about cost, so a runaway service can run up a large bill overnight.

The provider enforces the cap at runtime. This example checks the agent's side before anything runs: every deploy carries a cap, the caps fit the user's budget, and the opt-out is not used without the user agreeing to it.

Trusted module

deploy requires a positive cap, so an uncapped deploy cannot be written. remove_spend_cap is the opt-out. Both declare successor-state axioms over a Capped fluent. estimate_monthly_cost is non-negative but unbounded above.

examples/cloud/tools/cloud/trusted/effects.py

import clauz3
from clauz3.fluent import effect, fluent

# Successor-state fluent: a service is capped unless this program removes its
# cap. ``deploy`` always installs a cap; ``remove_spend_cap`` is the explicit
# opt-out ("I will be responsible for subsequent charges"). Contracts in
# ``contracts.py`` query the final valuation, so an agent may lift a cap
# mid-program only if a later deploy restores one.
Capped = fluent("capped", key=str, value=bool, initial=True)


@clauz3.ensures(lambda result: result >= 0, message="estimate must be non-negative")
@clauz3.trusted
def estimate_monthly_cost(service: str) -> int:
    """MOCK trusted cost estimate for ``service`` in whole USD per month.

    Contract: the returned estimate is non-negative. Nothing bounds it from
    above, so a cap computed from it must be clamped by the agent.
    """
    return 0


@clauz3.requires(
    lambda service, spend_cap_usd: spend_cap_usd > 0,
    message="spend_cap_usd must be positive",
)
@clauz3.trusted
@effect(lambda service, spend_cap_usd: Capped.set(service, True))
def deploy(service: str, spend_cap_usd: int) -> None:
    """MOCK trusted deploy with a hard monthly spend cap.

    The provider halts ``service`` once its monthly spend reaches
    ``spend_cap_usd``. Contract: the cap is positive; how high it may go is
    an agent-stated guarantee. Records ``Capped[service] = True``.
    """
    pass


@clauz3.requires(lambda service: len(service) > 0, message="service must be non-empty")
@clauz3.trusted
@effect(lambda service: Capped.set(service, False))
def remove_spend_cap(service: str) -> None:
    """MOCK trusted removal of a service's hard spend cap.

    After this call the provider bills without limit and will not shut the
    service down. Records ``Capped[service] = False``.
    """
    pass

examples/cloud/tools/cloud/trusted/contracts.py

"""Cloud-spend predicates built from generic trusted effect facts.

Inspired by Simon Willison's case for hard budget caps on by default
(https://simonwillison.net/2026/Oct/3/default-hard-budget-caps/). The provider
enforces a cap at runtime; these contracts let a user check, before anything
runs, that an agent's deploys carry caps and that the caps are sane.
"""

from tools.cloud.trusted.effects import deploy, remove_spend_cap

from clauz3.spec import ContractSpec, contract, effect

from .effects import Capped

Deploy = effect(deploy)
RemoveCap = effect(remove_spend_cap)


@contract
def cap_at_most(max_usd: int) -> ContractSpec:
    """Guarantee every deploy's monthly spend cap is at most ``max_usd``."""
    return Deploy.all(lambda d: d.spend_cap_usd <= max_usd)


@contract
def total_caps_at_most(max_usd: int) -> ContractSpec:
    """Guarantee the deploy caps sum to at most ``max_usd``.

    The sum counts every deploy, so redeploying a service counts its cap
    again; that over-approximates and fails closed. This bounds the
    worst-case monthly bill only while every service stays capped: pair it
    with ``never_remove_caps()`` or ``all_services_capped_at_end()``, since a
    later ``remove_spend_cap`` is not visible to the sum.
    """
    return Deploy.sum(lambda d: d.spend_cap_usd) <= max_usd


@contract
def only_services(allowed: list[str]) -> ContractSpec:
    """Guarantee every deploy targets a service in ``allowed``."""
    return Deploy.all(lambda d: d.service in allowed)


@contract
def never_remove_caps() -> ContractSpec:
    """Guarantee no spend cap is ever removed, even temporarily."""
    return RemoveCap.empty()


@contract
def all_services_capped_at_end() -> ContractSpec:
    """Guarantee no service is left uncapped once the program finishes.

    A cap may be removed partway through as long as a later ``deploy``
    restores one before the end.
    """
    return Capped.final.all(lambda s: s.value == True)  # noqa: E712

Clamping a computed cap

A cap derived from the estimate must be clamped. Without the clamp the prover finds a counterexample: any estimate of 50 or more pushes the cap past the bound.

examples/cloud/cases/estimate_clamped_pass.py

# ruff: noqa: F821
from tools.cloud.trusted import contracts as cloud
from tools.cloud.trusted.effects import deploy, estimate_monthly_cost

import clauz3


@clauz3.guarantee(cloud.cap_at_most(100))
def main() -> None:
    headroom = 2 * estimate_monthly_cost("api")
    if headroom > 100:
        deploy("api", 100)
    elif headroom > 0:
        deploy("api", headroom)
    else:
        deploy("api", 1)

examples/cloud/cases/estimate_unclamped_fail.py

# ruff: noqa: F821
from tools.cloud.trusted import contracts as cloud
from tools.cloud.trusted.effects import deploy, estimate_monthly_cost

import clauz3


@clauz3.guarantee(cloud.cap_at_most(100))
def main() -> None:
    headroom = 2 * estimate_monthly_cost("api")
    deploy("api", headroom + 1)  # unclamped: a large estimate exceeds the cap

Per-service and total budgets

cap_at_most bounds each service. The user's budget is usually for the whole bill, which is what total_caps_at_most bounds. Four services capped at 50 each pass the first and fail the second:

examples/cloud/cases/total_caps_fail.py

# ruff: noqa: F821
from tools.cloud.trusted import contracts as cloud
from tools.cloud.trusted.effects import deploy

import clauz3


@clauz3.guarantee(cloud.cap_at_most(50))
@clauz3.guarantee(cloud.total_caps_at_most(150))
def main() -> None:
    # Each service's cap is within the per-service bound; together they are not.
    deploy("api", 50)
    deploy("worker", 50)
    deploy("scheduler", 50)
    deploy("cron", 50)

The sum counts every deploy, so redeploying a service counts its cap twice. That over-approximates the bill, which is the safe direction.

Cap bounds need an end-state guarantee

Bounding the caps does not stop the agent removing one afterwards. This program proves against both cap bounds, yet api ends up billing without limit:

examples/cloud/cases/cap_bounds_then_removed_pass.py

# ruff: noqa: F821
from tools.cloud.trusted import contracts as cloud
from tools.cloud.trusted.effects import deploy, remove_spend_cap

import clauz3


# Proves: cap bounds only constrain deploy caps. They do not see the later
# removal, so the service ends up billing without limit. See the paired
# _fail case for the guarantee that closes this gap.
@clauz3.guarantee(cloud.cap_at_most(100))
@clauz3.guarantee(cloud.total_caps_at_most(150))
def main() -> None:
    deploy("api", 50)
    remove_spend_cap("api")

Adding all_services_capped_at_end() (or never_remove_caps()) rejects it. State one of them whenever the user's budget must actually hold:

examples/cloud/cases/cap_bounds_then_removed_fail.py

# ruff: noqa: F821
from tools.cloud.trusted import contracts as cloud
from tools.cloud.trusted.effects import deploy, remove_spend_cap

import clauz3


@clauz3.guarantee(cloud.cap_at_most(100))
@clauz3.guarantee(cloud.total_caps_at_most(150))
@clauz3.guarantee(cloud.all_services_capped_at_end())
def main() -> None:
    deploy("api", 50)
    remove_spend_cap("api")  # the end-state guarantee rejects this

Removing a cap

never_remove_caps() forbids the opt-out anywhere in the trace. all_services_capped_at_end() is a state contract: a cap may be lifted for a one-off job as long as a later deploy restores one.

examples/cloud/cases/capped_at_end_pass.py

# ruff: noqa: F821
from tools.cloud.trusted import contracts as cloud
from tools.cloud.trusted.effects import deploy, remove_spend_cap

import clauz3


@clauz3.guarantee(cloud.all_services_capped_at_end())
def main() -> None:
    # Lift the cap for a one-off backfill, then redeploy with a cap.
    deploy("api", 50)
    remove_spend_cap("api")
    deploy("api", 50)

examples/cloud/cases/capped_at_end_fail.py

# ruff: noqa: F821
from tools.cloud.trusted import contracts as cloud
from tools.cloud.trusted.effects import deploy, remove_spend_cap

import clauz3


@clauz3.guarantee(cloud.all_services_capped_at_end())
def main() -> None:
    deploy("api", 50)
    deploy("worker", 20)
    remove_spend_cap("worker")  # worker is left billing without limit

Limits

The contracts cover the deploys in one program. A provider's cap applies to spending over a billing period across many runs, which needs state carried between runs. That is not modeled here.

All cases

Browse the full set on the all-cases page.

How they run

examples/cloud/Justfile

trusted := "tools/cloud/trusted"
prove := "uv run clauz3 prove --trusted-root " + trusted
# Proves each case in one process: *_pass.py must prove, *_fail.py must not.
prove-cases := "uv run python -m clauz3._prove_cases --trusted-root " + trusted

test: lint cases

lint:
    uv run clauz3 lint {{trusted}}/effects.py

cases:
    {{prove-cases}} cases/*_pass.py cases/*_fail.py