One contract, four systems

Status: the protocol is prepared and frozen, and the case bank is fixed with hashes. Expected outcomes below are predictions from the source texts, not results. The comparative run has not been performed for any of the four systems.

This page describes one contract lifecycle that four contract systems are asked to walk through: Symboleo, Accord / Cicero, Stipula, and Arxo. Each of the three neighbours already has its own prepared experiment on its own sample contract. This scenario puts them on one trace so that the same question gets four answers, side by side.

The scenario in plain words

A seller and a buyer agree on a sale of goods worth 1000 USD. The seller must deliver by a delivery deadline; the buyer must pay by a payment deadline. If payment is late, the seller may suspend delivery and the buyer may later resume it by paying within a window. If delivery fails, the buyer may terminate. A late-delivery penalty accrues at 10.5 percent of the price per 2-day period, capped at 55 percent of the price. The buyer may terminate for delay only when the delay is strictly more than 15 days. Force majeure releases the penalty only when both the contract clause and the request invoke it. A timeout k closes a window when nobody acts.

There is no statute behind this scenario. It is a union of three published sample contracts, chosen because no single one of them fits the other two:

• Symboleo’s meat-sale sample contributes delivery and payment obligations, a late-payment reparation, and the suspend, resume, and terminate powers — but has no money formula or cap.
• Accord’s Late Delivery and Penalty template (from the Cicero template library, Apache-2.0) contributes the penalty formula, the cap, the strict termination threshold, bilateral force majeure, and refusals — but has no suspension and no state machine.
• Stipula’s bike-rental example contributes agreement into an inactive state, calls allowed only in the right state, asset transfers, a timeout event, and an early end — but no penalty formula and no force majeure.

Every case in the bank names the case of the original sample it comes from, so each source bank stays checkable on its own terms.

The event trace

Step	Event	What is observed
E0	Agreement: parties, price, deadlines, rate, cap, threshold, k	positions created, initial state
E1	Offer by the seller	transition to the waiting state
E2	Delivery on time, late, or missing	delivery obligation fulfilled or violated
E3	Payment on time, late within the window, or missing	payment obligation fulfilled or violated; reparation created on breach
E4	Penalty accrual	amount = min(rate × fraction of period × price, cap); strict threshold for termination
E5	Suspension of delivery, then resumption after late payment	suspended, then active again
E6	Termination by choice, or successful completion	terminal projection
E7	Force majeure: both sides, one side, or none	release only when both flags are set
E8	Timeout k with no action	timeout event; the window closes
E9	Terminal projection	one whole-contract state, defined by the experiment

What each system is asked to produce

• Symboleo — per-obligation and per-power states over the trace (fulfilment, violation, suspension, successful or unsuccessful termination), produced through its model checker. Its explanation is the checker’s report or counterexample.
• Accord — the clause’s answer to each request: the penalty as an amount with a currency code, the termination flag, the outgoing payment event, or a refusal. Its explanation is the answer plus the event.
• Stipula — the state of the contract program after each call, the asset transfers, the timeout event, and the final distribution. Its explanation is the execution trace.
• Arxo — the status of each duty and power at each step, the penalty as exact money with a currency, the termination liberty, and refusals as invalidly exercised powers. Its explanation is the proof graph of each answer.

The whole-contract “terminal state” is not an Arxo concept: Arxo reports the status of each norm. The terminal projection used here is the experiment’s own rule, frozen after the first run and scored separately.

The case bank

Fourteen base cases and three edit cases. “Posed by” lists the systems for which the case is meaningful; the others do not observe that part of the lifecycle.

Case	Situation	Expected outcome (from the source texts)	Posed by	Comparability
S01	Delivery and payment both on time	both obligations fulfilled; success projection; penalty 0	all four	comparable
S02	No payment by the deadline	payment violated; reparation obligation created	all four	comparable
S03	Delivery suspended, then late payment within the window	suspended, then active again	Symboleo, Stipula, Arxo	comparable
S04	Delivery breached, buyer chooses to terminate	delivery violated; unsuccessful termination	Symboleo, Stipula, Arxo	comparable
S05	Delivery made after the deadline	still violated: the deadline wins over the late fact	Symboleo, Accord, Arxo	comparable
S06	Delivery fulfilled; the suspension power never used	the power expires or terminates unused	Symboleo, Arxo	comparable
S07	Both obligations breached	both violated; unsuccessful projection	Symboleo, Arxo	comparable
S08	Power with a deadline, exercised after it	expired, then terminated	Symboleo, Stipula, Arxo	comparable
S09	Delays of 1, 4, and 30 days; exactly 15 days	52.5, 210, and 550 (capped) USD; termination false at 15, true at 30	Accord, Arxo	comparable
S10	Force majeure on both sides, on one side, none	penalty 0 only when both are set	Accord, Arxo	comparable
S11	Refusals: unsupported duration unit, future delivery date; zero base; omitted optional field; event content	refusal for the two invalid calls; omitted field has no effect; event names amount and parties	Accord, Arxo	comparable
S12	The “buyer is not the seller” constraint is violated	open: the sources show no observable outcome	Symboleo, Arxo	not comparable
S13	Obligations meant to survive an unsuccessful end	open: the published semantics are unsettled	Symboleo, Arxo	not comparable
S14	Fractional period: delay of 3 days	template code gives 157.5; template text reads as 210	Accord, Arxo	not comparable
P1	Money changes from a bare number to an amount with currency	edition A answers 210.0; edition B answers 210 USD	Accord, Arxo	not comparable across editions
P2	An obligation gains a precondition; the threshold changes from a raw amount to a unit conversion	threshold of 2 weeks with a 4-day delay: edition A true, edition B false	Symboleo, Accord, Arxo	not comparable across editions
P3	Timeout k small versus large on the same contract	small k: the timeout wins; large k: the early end wins	Stipula, Arxo	not comparable across editions

Within one edition, the edit cases still score match or mismatch; only pairs that span two editions are set aside.

When answers count as the same

• Match — statuses and flags are equal as strings after the published mapping (for example, Arxo’s “violated” against Symboleo’s “Violation”). Money agrees within a relative tolerance of one in a million, plus a stated allowance for Accord’s wall-clock time: the studied template reads the current date, so a penalty can drift by the accrual over the run’s duration. The raw difference is always kept.
• Not comparable — the two sides answer different questions. Five grounds are fixed in advance: a violated constraint with no observable outcome in the sources (S12); obligations whose surviving semantics are open in the published papers (S13); split-in-half amounts in Stipula, whose exact semantics are not established (only the signs of the shares are compared); pairs that span two editions (P1–P3); and a template whose code and text disagree on fractional periods (S14).
• Mismatch — the same question, under the same edition, got different answers. The cause stays open until the source texts settle it.

Some properties compare only between some pairs. The penalty formula and force majeure compare only between Accord and Arxo; suspension and resumption compare only among Symboleo, Stipula, and Arxo. A refusal is an observable outcome on every side that has one — a thrown error, an invalidly exercised power, or a missing transition — and the error text itself is never compared. Explanations are compared as a qualitative pair (checker report, event, trace, proof graph), not byte for byte.

The Arxo side

The Arxo model for this scenario is already written as a small standalone package, independent of any law in the corpus. It passes the language’s static check with no diagnostics; its own scenarios are written but have not been executed. It follows the template code of Accord’s newer edition (continuous fraction of a period, cap as a minimum, strict threshold) and the texts of the Symboleo and Stipula samples.

Two short excerpts. The rate and the cap are named constants:

Arxo Law

const PENALTY_PCT: Decimal = 10.5 percent;
const CAP_PCT: Decimal = 55 percent;

The termination right is closed over admitted calls: where no rule establishes the right, its absence is stated explicitly rather than left unknown. That is how the exact-15-days case is meant to answer “false” rather than “not established”:

Arxo Law

closure TerminationDefault {
    predicate buyer_may_terminate;
    domain call_admitted;
    snapshot "urn:stand:shared-contract-lifecycle:cases:2026-09-30";
    complete_as_of @2026-09-30T00:00:00Z;
    derive_explicit_negative true;
}

Cases S12 and S13 have no Arxo rules on purpose: the sources give no observable outcome, so the model stays silent rather than guess. Force majeure flags and trace events enter as established facts of the case; nothing in this scenario calls for an evaluative judgment.

Out of scope

• Subcontracting, assignment, and substitution (Symboleo).
• Generating contract text from data (Accord).
• Liquidity and reachability analyses (Stipula).
• Second-order powers.
• Performance: timing, if recorded, is informative and never a criterion.
• Monitoring on a ledger.
• Exhaustive model checking over all paths — a Symboleo strength with no counterpart in a per-query answer, outside this comparison by design.

What a result will and will not say

When the run happens, the result will be a per-case table of the four answers and one outcome each. Agreement on these seventeen cases will not show that the four languages are equivalent, nor that the four models formalize the same contract. Each neighbour’s pins, licences, and source hashes are recorded in its own experiment; copies of samples whose licence is not stated are kept as hashes only.

Materials: experiments/comparisons/shared/contract-lifecycle/ in the project repository. See also the methodology.