A grain is admitted under explicit budget and hosting terms.
Worlds agents
Will under law
An agent may be uncertain. Its authority need not be.
A model proposes intentions inside a confined body. Capabilities define what it may attempt. The kernel decides what happened, and a receipt makes the accepted turn independently checkable.
01
The grain
A hosted agent has a lifecycle, a budget, and a body.
Tools and network exits are mediated by the host rather than inherited from the model process.
A brain selects a capability-scoped affordance; proposal is not execution.
The accepted action becomes the same receipted turn used by every other world object.
Usage, payment, sleep, wake, and reap are world transitions rather than an operator’s private ledger.
02
Verification ladder
Each rung answers a stronger question.
R0
Signed receipt
The agent host attests to an action with a persisted receipt key. This identifies the host’s statement; it does not yet bind the kernel.
R2
Committed turn
The action is witnessed as a real kernel turn, and verification binds the agent receipt to that committed transition.
R2 + attestation
Confined execution rail
A hardware attestation can bind the host and execution environment to the receipted action path.
R3 conditional
Whole finalized history
The implementation folds finalized turns, light-verifies the aggregate, and calls the exported Lean verifier. Its soundness is conditional on the named recursion and FRI engine floor.
03
Where it stops
Receipts limit authority; they do not manufacture judgment.
The agent platform implements rent, host, drive, verification, billing, sleep, wake, and reap; the confined host can run live model brains behind controlled egress. A passing receipt says that the permitted operation happened. It does not say the model’s plan was wise, kind, or complete.
Implemented: lifecycle, confined tools, live model seam, kernel-turn binding, attestation binding, whole-history verifier path.
Not claimed: a generally available hosted-agent cloud, unconditional recursive soundness, or semantic correctness of arbitrary model intentions.