An agent proposes.
It chooses an approved action and a quantity. The pool’s owner defines the rules; agents cannot rewrite them.
Open-source Rust / NEAR contract
A formally verified contract for shared resources.
Independent agents book capacity from one shared pool: GPU time, power, inventory, budget. The contract admits a booking only if hard limits hold and the pool’s combined commitments do not get worse. Owners write the policy as one JSON file. Agents cannot rewrite it.
Lean model proofsTLA+ safety checksKani on the Rust coreConformance traces
The verification found two high-severity settlement bugs in v1.0.0. v1.1.0 fixes them. Multi-level verification ↓
EXAMPLE 1 OF 6 · SPACE STATION SYSTEM ONLINE
Awaiting requestsCLEARANCE REQUIRED
12 MW total. 4 MW protected. Every ship must pass the same gate.
WINDOW 010 / 8 MW docking
4 MW life support
01 / The ProblemLocal decisions. Shared consequences.
Everyone follows their own limits.
The pool still runs out.
An agent can have permission to act and still make the shared situation worse. Even well-behaved agents can overbook the same capacity. Our security boundary checks authority and the combined consequences—including commitments that have not finished yet.
The lock checks.
The contract evaluates the resulting shared state, including pending commitments. Hard limits must hold and the configured error score must not increase.
Resources are reserved.
An allowed action reserves capacity before dispatch. A denied action can be revised and checked again. Unknown execution outcomes keep their reservations.
What is “system energy”? A policy-defined measure of imbalance: unmet work, excess bookings, uneven stock, or stress-loss exposure. The Lyapunov-style check asks whether an agent’s commitment makes that score worse. It does not predict every future event.
V(next) ≤ V(now)02 / Explore the scenariosSix situations. One decision kernel.
See the shared
consequences.
Start at the space station: a ship must wait because docking would consume protected power. Then explore compute, delivery capacity, inventory, worker budgets, and risk headroom—all using the same Rust gate.
01 / The conflict
Research reserves 4 blocks. Evaluation reserves 2. Data asks for 4 more.
02 / The denial
10 fits the hard ceiling of 12, but energy would rise 20 → 44. The pool stays at 6.
03 / The revision
Run the next decision: Data explicitly requests 2. Energy falls 20 → 8; bookings reach 8.
01of 06 scenarios
Connecting to the explorer…Synthetic resources. No real funds or jobs.
Up next
Loading the first request…
The shared pool
Run the first decision to see what the lock checks.
System energy
—Lower means less imbalance under this policy. Denied requests do not change the pool.
Decision trail
Most recent firstEach request leaves an explanation here.
Why the shared check mattersThis is the illustrative failure the scenario addresses, not an unguarded execution mode.
Go further Try your own request
A suggestion changes nothing until you explicitly submit it.
Execution controls
Turn this off to inspect pending commitments. Completion and confirmed nonexecution are simulated provider evidence.
Inspect commitments & execution
Pending work already counts. An unknown outcome retains its reservation until the registered executor confirms what happened.
| ID | Action | Units | Status | Simulate evidence |
|---|
03 / Under the contractSmall enough to inspect.
A simple gate.
An explicit boundary.
NEAR holds the shared policy and reservation ledger. Each submission checks the authenticated caller and current state, then reserves capacity in one contract call. Cross-contract dispatch and authenticated callbacks connect that decision to execution.
Why put the gate on NEAR? Independent agents share one contract-owned ledger and a common execution authority. The synthetic executor rejects direct agent calls: changing a browser or skipping a client-side check cannot authorize execution. Real providers would need the same enforced adapter boundary.
Admission ruleConceptual pseudocode
// A proposed commitment
check_authority(caller, recipe);
check_version_and_freshness(request);
next = reserve(state, recipe, quantity);
require(hard_constraints_hold(next));
require(energy(next) <= energy(state));
// Reserve first. Dispatch second.
commit(next);Recovery from an externally disturbed state has additional checks. See the full specification for exact semantics.
A pure Rust core
Bounded data, checked integer arithmetic, fixed recipes. No NEAR dependency in the core’s default build.
A NEAR execution boundary
The synthetic adapter accepts execution only from the lock. Callback failure does not automatically release a commitment.
A precise claim
Accepted reservations do not increase the configured potential. External events can. Lean model proofs, TLA+ checks, and Kani verification of the Rust core target v1.1.0. Explore the formal verification.
Make it yours
Configure it for your own contention problem. Deploy it on NEAR.
Everything that makes the six scenarios different is data. Describe your shared resource in one JSON policy, then deploy the same tested Wasm.
- 01
Name what is scarce.
Each
metricis a quantity the pool tracks, with hardminandmaxbounds: GPU blocks, MW, inventory, budget.Add one metric per window or bucket you need to protect separately. A protected reserve is simply a lower
maxon the shared bucket. - 02
Say what “worse” means.
Each
termscores imbalance:Targetdistance,Excessover a line, orDeficitbelow one. Admission requires the total never rises.Weights decide which problems matter most. Hard bounds and the score are separate checks; a lower score never buys a breach.
- 03
Give each agent a recipe.
A
recipefixes who may ask (actor), who executes (executor), what is reserved, and what completion changes. Agents choose only a recipe and a quantity.requireschains recipes, so a later step can need an earlier one to finish first. - 04
Build, deploy, initialize.
Policy is immutable once
newruns, so review it first. Deploy and initialize in one transaction from the contract’s own account.Then check the code hash, preview as an agent, and submit.
Shape of a policyconfig.json
{
"name": "api-budget",
"owner": "you.near",
"max_age_seconds": 0,
"metrics": [{ "name": "Requests booked", "unit": "req/min",
"initial": 0, "min": 0, "max": 100 }],
"terms": [{ "metric": 0, "target": 80,
"weight": 10, "shape": "Excess" }],
"recipes": [{ "name": "Crawler: batch", "actor": "crawler.near",
"executor": "api-gateway.near",
"reserve": [1], "complete": [0],
"max_units": 40, "requires": [] }]
}Build and deploy commands
# 1. Build both Wasm contracts and a provenance manifest
./scripts/build.sh
# 2. Deploy and initialize the lock in one transaction
# (near-cli-rs syntax; check `near contract deploy --help` for your version)
near contract deploy pool.you.near \
use-file target/wasm32-unknown-unknown/release/pool_contract.wasm \
with-init-call new json-args "$(jq -c '{config: .}' config.json)" \
prepaid-gas '100 Tgas' attached-deposit '0 NEAR' \
network-config testnet sign-with-keychain send
# 3. Deploy and initialize the executor named in each recipe's "executor"
# field (api-gateway.near in the example). The bundled pool_executor.wasm
# is synthetic; use your own adapter for real resources. Without an
# initialized executor, the first dispatch ends in an "unknown" outcome
# and the reservation stays held.
near contract deploy api-gateway.near \
use-file target/wasm32-unknown-unknown/release/pool_executor.wasm \
with-init-call new json-args '{"lock":"pool.you.near","operator":"you.near"}' \
prepaid-gas '100 Tgas' attached-deposit '0 NEAR' \
network-config testnet sign-with-keychain send
# 4. Read the pool back and compare the code hash to your build manifest
near contract call-function as-read-only pool.you.near get_pool \
json-args {} network-config testnet nowUse the deployment checklist for account setup, then open the NEAR console with your account and expected code hash.
Before you deploy for real
Replace every executor with an adapter you control. The bundled executor is synthetic: it proves the gate, not a connection to your GPUs, warehouse, or funds. A real adapter must implement the execute and status protocol, idempotency, and authoritative cancellation, and it must leave agents no route around the lock.
Policy and principals cannot be edited after initialization. A pool holds at most 32 metrics and 32 recipes, and keeps its 256 most recent commitments; a new one replaces the oldest once that has ended. The contract is not independently audited. Formal verification of v1.0.0 found issues; v1.1.0 fixes them. Future versions are likely to add more capabilities, check that the contract version you use has the capabilities you want (sometimes simpler is better). Test on testnet first.
What exactly does an agent submit?
A recipe ID, an exact integer quantity, the state version it reviewed, and a short expiry. Recipes fix the actor, executor, effects, and prerequisites. The agent cannot supply its own risk estimate or ledger delta.
{
"recipe": 0,
"units": 2,
"version": 4,
"expires_at": "current time + 10 minutes"
}Illustrative request: the real expiry is an integer timestamp. A stale version is rejected and must be reviewed again.
What happens after approval?
Reserved→Dispatched→Active→Completed
Unknown execution outcomes keep their encumbrance. Before dispatch, the actor or owner can cancel. After dispatch, release requires definitive nonexecution evidence from the registered executor.
What is—and isn’t—guaranteed?
The kernel checks the configured bounds and potential against a modeled state. It does not guarantee fairness, profitable trades, truthful external observations, or eventual completion. The immutable policy and registered evidence authorities are part of the trust boundary.
Compute jobs, deliveries, worker payments, and financial positions in this explorer are synthetic. Real-world enforcement requires an adapter without a route around the lock. Dedicated multi-level verification of v1.1.0 includes model proofs, checks, and Kani on the Rust core. The verification PR reports settlement/liveness findings. v1.1.0 fixes them (findings). The contract is not independently audited.
Inspect the selected scenario’s policy
Inspect the last Rust decision
Run a scenario decision to inspect its response.
04 / Evidence for reviewRun it. Inspect it. Check the boundary.
A visible decision.
A testable claim.
The deliverable is an MIT-licensed contract for the NEAR ecosystem. Fork it, define the shared resources and policy for your application, and connect an enforced executor. The six scripted scenarios show how the same admission rule applies across businesses.
Reject the harmful commitment.
The GPU trace includes a request that passes hard capacity bounds but raises energy. It is denied without reserving resources.
Inspect the Rust-generated trace ↗Try going around the gate.
NEAR sandbox tests attempt direct executor calls and agent-authored settlement. Both fail; registered execution evidence is required.
Inspect the bypass tests ↗Keep uncertain work reserved.
Sandbox tests exercise stale requests, unknown execution outcomes, and reconciliation. A failed callback alone does not free capacity.
Inspect the verification handoff ↗Formal verification, with evidence you can inspect
Dedicated multi-level verification of the contract includes Lean model proofs, bounded TLA+ checks, Kani on the Rust core, and conformance traces against the Rust core. The work targets v1.1.0, source revision 57b3f02. Verification found high-severity settlement/liveness findings F-1 and F-2. v1.1.0 fixes them and the lower-severity findings (findings).
What you can verify today
Rust kernel, NEAR lock and synthetic executor, six deterministic scenarios, local Wasm integration tests, and a static explorer. The browser demo is a simulation or recorded replay—not a public-chain transaction.
Where you can go from here:
Integrate into your systems, real payments, live LLM agents, or NEAR Intents integration. Note that this contract has been formally verified but has not been independently audited. Review the contract mechanics to adapt them to your use case.
Open source · MIT licensed · Built for the NEAR ecosystem
Your shared resources.
Your deployed contract.
Modify the contract and policy for your application. Review the verification findings, connect your execution adapter, and deploy a gate your agents share.
Get the contract