Deposit Dispute

A landlord withholds part of a rental deposit and itemizes why. A tenant disputes some of it. The question a model is asked here is never “what is this worth” — it is “did the landlord establish this deduction on the evidence”, once per line item, yes or no. The model never touches a number. The five amounts were fixed when the contract was deployed, before any evidence existed and before any adjudicator was asked anything; the contract sums the established items, caps the total at the deposit, and gives the tenant the remainder.

Base Sepolia · testnet only

This demo is read-only and takes no input at all — no field, no slider, no query parameter. There is no wallet to connect and nothing to sign.

Every figure on this page is transcribed from one completed run on 5 August 2026, not read live. That is a deliberate difference from the other demos here: both disputes are settled and drained, and the contract has no owner, no setter and no upgrade path, so a dispute settles exactly once and no later state exists to read. Each figure is checkable against the linked transactions, which is the provenance that matters.

Dispute A 0x025A2A50…CddD9410 · Dispute B 0x6698DfB8…2Ff501F2 · Source on GitHub

---

The argument this demo makes

A model that can answer with a number can be argued into any number. So it is not allowed to produce one.

1. The schedule is fixed at deployment. Five line items, each a description hash and an amount, set in the constructor. There is no owner, no setter and no admin function to change one afterwards. An operator who could edit an amount after seeing the findings could produce any split it wanted, and no process around such a function would make its absence provable. Absence is provable.
2. The adjudication is per item, never per dispute. Five items across three slots are fifteen separate calls, never batched. A batch would let a strong-looking case drag a weak item along with it, and would produce five findings that were never five independent decisions while presenting them as if they were.
3. The burden sits with the landlord. NotEstablished is the contract's zero value and there is deliberately no abstain state. An item the evidence does not carry is an item the tenant keeps the money for, so a refusal, a silence or a model that cannot be reached can only ever make it harder to take money from the tenant — never easier.
4. The evidence is committed before it is judged. The published bundle is committed as a merkle root and each finding is bound to the leaf for its own item, so a finding cannot be offered against a different deduction than the one it answered.

What the two disputes settled at

A dispute settles exactly once, so it can demonstrate a partial split or the cap and never both. That is why there are two.

Dispute A — the split. The five items cannot reach the deposit even if every one is established, so both sides are credited whatever the panel decides — provided it establishes at least one item. Establishing nothing was a real possible answer and would have been reported as one.

Dispute B — the cap. Any single established item already puts the claim over the deposit, so the landlord is capped at the deposit and the excess is recorded as a debt nowhere. The tenant's withdrawal reverted on a zero balance, which is the contract being right rather than a failure.

In both, landlord plus tenant equals the deposit exactly, and both contracts now hold zero: every wei that went in came out to one of the two parties. That conservation is asserted deterministically by the test suite and driven by two independent fuzzing engines — it is a property of the contract, not something confirmed by looking at it afterwards.

The cap, and what it deliberately does not do

Established items may sum to more than the deposit, and dispute B's do. The landlord takes the deposit and the excess is recorded as a debt nowhere — not stored, not accruing, not recoverable through this contract. That is a limit by choice rather than an omission: a deposit contract holds a deposit, and pursuing a shortfall beyond it is a court's job, not a smart contract's. Dispute B's tenant withdrawal reverted on a zero balance, which is the contract being correct; a withdrawal that had succeeded on a zero award would have been the bug.

---

The panel

Three slots, each pinned to a different model identifier by the constructor, which rejects a duplicate. Different models and, as configured here, more than one vendor — the contract can enforce the first and cannot see the second, because it holds hashes and has no idea which company serves them. Three models from one vendor share a tokenizer, a safety layer, a serving stack and an outage, which is a correlation a 2-of-3 threshold silently assumes away.

Before any model is called, the adjudicator reads each slot's model-identifier hash back off the chain and compares it against what it is configured with. A mismatch stops the program. Otherwise it could publish findings under a slot naming a different model than the one that answered, and a third party re-running the work would re-run the model the chain named — a discrepancy nothing on chain could reveal.

Two things asking revealed, neither of them assumed

An identifier asymmetry. Both Anthropic identifiers came back exactly as requested. The OpenAI one was an alias that resolved to a dated snapshot. That matters more here than it usually would, because keccak256 of the identifier is stored in the constructor and published beside every finding: an alias makes that hash a pointer to a moving target. Someone re-running this next month would get whatever the alias points to then while the chain still names the alias, and nothing would reveal the difference. So the snapshot is pinned, and the accepted cost is that a rotation means a redeployment.

Two of the three models reject the temperature field outright. Not ignore it — reject it, with an HTTP 400 and no completion. A request carrying a parameter the model refuses does not run at a different temperature; it does not run at all. So whether the field is sent is per-slot configuration while its value is not configurable anywhere: the value is zero, and what varies is a fact about a vendor's API.

This is what happened on one afternoon, to these three models. It is not a claim about these vendors in general, about other models, or about any other date — 30 calls is not a survey.

---

What the run produced

30 calls — five items, three slots, two disputes — produced 28 findings submitted on chain. The difference is 2 replies that were refused.

The 2 refusals, and why they cost nothing

Both were malformed JSON and both landed on item 4. Neither was wrapped in a code fence and neither was prefixed with prose — both were the agreed shape, started, and then broken. A refusal is a refusal, not a guess. Nothing retried with a looser parser, asked the model to try again, or inferred a finding from what the reply seemed to lean toward. Each affected item was still decided 2–0 by the two slots that did answer, and because two agreeing findings are needed to establish anything, a missing voice can only make establishing a deduction harder.

The refused text itself was not captured, and that is a gap this run exposed. The panel logged that a reply was malformed but not what it said — a report without its evidence. Raw-reply capture was added after the run rather than before it, so these two replies are lost for good. The next run will have them. Saying so is cheaper than implying they were kept.

Where the panel disagreed

Every other adjudicated item was unanimous among the slots that answered. The cracked pane is the item the evidence was written to leave genuinely contested, and the panel split on it — which is the case the design exists for, not a defect in it.

---

Where the two halves could disagree, and what pins them

The off-chain adjudicator builds the evidence tree by laying out rows; the contract folds a proof. Two different algorithms over one shape, in two languages. A single shared literal — the same five descriptions and the same expected root, in the Go tests and in the Solidity tests — holds them together. Without it the panel would build proofs the contract refuses, and the first symptom would be a reverted transaction on a live dispute.

A second guard covers the more dangerous direction. The deploy script's description literals and the published evidence bundle's descriptions are asserted equal, because nothing on chain could detect a mismatch: the contract commits to the description it was given, not to the one the model saw. A drift there would have the panel answering about a deduction the chain does not describe, and every hash would still check out.

What the fuzzing campaign under-samples

Stated because a verification claim without its limits is a stronger claim than the evidence supports.

Two of the harness's entry points open a dispute, file its evidence, adjudicate all five items and settle in a single call. That is what makes both showpiece states reliably reachable, and it is also why the disputes those drivers create never sit in the state where a claim is filed but not yet settled. Two other entry points need a dispute in exactly that phase, because they are the ones that attack it — offering one item's evidence against another, and trying to spend a slot's vote twice — so those attacks run less often than the rest of the harness.

That was measured, not assumed: a test walks independent pseudo-random sequences over the same entry points the fuzzer draws from, and its first run turned up a sequence that attacked the evidence binding zero times. Both attack paths are additionally driven deterministically, one test each, asserting the offers were refused and nothing was recorded. A deterministic assertion is the stronger check, so those properties do not rest on how often the campaign happens to reach the state; the campaign corroborates them rather than proving them. A driver that parks a dispute in the filed phase is open work.

How it is verified

The contract passes the Pigfox Solidity pipeline on every push: two linters, the direct-chain doctrine gate, EIP-55 address casing, a static property count, formatting, build, tests and invariants, 100% line, statement, branch and function coverage on src/ with no exclusions, Slither at fail-on: low, and property fuzzing under both Echidna and Medusa — each asserting it registered all seven declared properties, so a property that silently stops being picked up fails the job instead of reporting a smaller green run. The off-chain panel has its own gate at 100% coverage on every package, and its whole suite substitutes the model and chain seams, so it makes no vendor call and spends nothing.

Two stages were red for a while, and both were fixed in the shared pipeline rather than here — no contract, test or threshold was changed to make either pass. The size gate had measured the property-fuzzing harness against EIP-170, a limit that binds only deployed bytecode, while the harness is built in process and deployed nowhere. The coverage gate then could not finish at all: instrumented, it needed 33.8 GiB against a 16 GB runner, because the invariant suite costs 2,473 CPU-seconds to cover nothing the unit suite already reaches. Both fixes narrowed what is measured and left what runs untouched: the invariant campaign still runs in full, under both fuzzers, and coverage is still required at 100% on every line, statement, branch and function.

The full procedure, every deployed address, and all 35 transaction hashes from this run — each finding mapped to dispute, item and slot — are in the repository.