docs← Back to article

Markdown for LLMs

Stipula

The source Markdown for this article. Copy it into your assistant or download it as a text file.

Download this articlePlain text ↗
# Stipula

**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.

## What Stipula is for

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.

## Where it meets Arxo

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.

## Key differences

- **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.

## A concrete scenario

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.

## Choosing and combining

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.

## Evidence and open questions

- 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.

## Sources and reproducible materials

- Shared scenario: [One contract, four systems](/comparisons/contract-lifecycle/).
- Language preprint: [arxiv.org/abs/2110.11069](https://arxiv.org/abs/2110.11069)
- Beginner's guide:
  [beginStipula.pdf](http://cs.unibo.it/~laneve/papers/beginStipula.pdf)
- Workbench: [github.com/stipula-language/stipula-workbench](https://github.com/stipula-language/stipula-workbench)