Skip to content
docs
Arxo ↗

Stipula

For LLMs7 sections

In short: Stipula runs a contract as a program with states, gated calls, and assets that cannot be duplicated; Arxo models the positions the contract creates. On the same step trace they compare action by action — with amounts deliberately reduced to signs. This page is for readers who write executable agreements and want the mechanism-level seams.

Stipula treats legal contracts as executable programs: an agreement constructor, party functions gated by state, linear assets preserved across transfers, non-cancellable timeout events that make deadlines first-class instead of external cron jobs, escrow and external-data patterns out of the box — plus symbolic liquidity analysis (“no assets frozen forever”), a reachability visitor, and bisimulation reasoning for refactoring. Double-spend and silent destruction are ruled out by construction, not by discipline.

Contract-as-executable-program on the same step trace: who may act in which state, timeout and early-finish branches, and who holds what asset distribution — comparable step by step. Execution here means the workbench Java interpreter stepping calls and events, with its version pinned at run time; the analyzers parse but do not execute. One older agreement-syntax revision does not parse under the current grammar — a grammar-version refusal with a failing exit code, not a semantic divergence.

  • Impossible call versus invalid exercise. A call outside state or party has no transition — it cannot happen. Arxo marks the attempt as invalidly exercised with an issue and no effect. Same observable refusal, different mechanism, recorded as a pair.
  • Linearity has no Arxo counterpart. The bike in the studied rental is a non-duplicable asset; the Arxo side holds an ownership fact. A recorded semantic difference, explicitly never “fixed” into equality.
  • Amounts compare by sign, not sum. A split-half expression parses and type-checks as an asset, but its runtime value and rounding are unestablished from the closed interpreter — amounts are a non-comparable control, signs comparable. The page does not compare split sums, full stop.
  • Terminal states map to an experiment artifact. The end-and-fail states project onto an experience-written frozen position set — the experiment’s own device, never Arxo semantics. The journal paper behind the language is paywalled, so its theses stay stated, not confirmed.

Twelve rental cases — agreement to the inactive state, offer and pay transitions, wrong-party and wrong-state refusals, an unguarded payment transition, early split finish versus timeout to the end state, asset linearity, an explanation pair — plus four edits: agreement-syntax revisions, a timeout-parameter race, and an authority-and-dispute variant. The interpreter side and the Arxo scenario side compare powers exercised, duty windows, and holdings per step.

Choose Stipula when the contract is a program to be stepped: gated calls, linear value flow, first-class timeouts, and analyses over the code. Look to Arxo when the positions need named grounds, dated editions, and replayable derivations across sources. Combined, the program can execute the agreement while Arxo holds the normative positions it creates — with the step trace as the shared record and amounts honestly signed.

  • Sources checked: September 2026 (fourteen sources re-opened with matching bytes, hashes, and sizes; the beginner’s guide read whole).
  • Studied profile: the workbench main line plus two agreement revisions of the studied contract; interpreter version pinned at run time.
  • Basis: confirmed by documentation plus a prepared protocol; comparative run not performed. One variant without the engine is a recorded-expectation check, still not-checked for unrun steps.
  • Open: split-sum semantics, guard-meaning discipline across revisions, paywalled-paper theses, and the run itself.

Documentation for Arxo. Writings — blog.arxo.io.

Anonymous visit counts on stats.arxo.io, no cookies.