Symboleo

In short: Symboleo proves things about all paths of a contract; Arxo derives the answer to one question with its grounds. This page is for readers who specify contract lifecycles and want to know where per-norm statuses overlap — and where exhaustive search has no counterpart.

Key differencesChoosing and combiningEvidence & limitations

What Symboleo is for

Symboleo is a specification language for legal-contract lifecycles: obligations and powers over an event-based temporal account, with statecharts, environment attributes, subcontracting and assignment, and surviving obligations. Its strengths are first-class deadlines as temporal predicates with a published axiom set, exhaustive model checking of small models with temporal-logic properties, and a conformance checker that replays traces — backed by an active multi-year publication series.

Where it meets Arxo

The shared ground is the lifecycle of individual norms — created, active, fulfilled, violated, suspended, terminated, expired — over the same timestamped event trace, compared status by status. Arxo has no single observable “contract state”: a terminal whole-contract projection used in the experiment is explicitly the experiment’s own frozen artifact, scored non-comparable if it diverges — never Arxo semantics.

Key differences

• Exhaustive search has no Arxo counterpart. The model checker ranges over all paths with liveness and safety properties; a proof graph answers one query. Out of scope for the comparison, not a defect on either side.
• Powers act only through their declared functions. Suspend, resume, discharge, terminate, trigger — and second-order powers are commented out of the grammar, hence unsupported. Capability boundaries come from the grammar, stated openly.
• The toolchain needs finishing by hand. Specification output requires documented manual completion before the checker runs; the monitoring path needs a ledger; one code generator carries a confirmed eager-termination defect — a generator defect, explicitly not semantics.
• Some semantics are open by the papers’ own admission. Surviving obligations carry a bug marker in the sample; those cases stay non-comparable with the marker cited.

A concrete scenario

The prepared experiment walks a goods-sale contract through fourteen cases — delivery and payment, late-payment reparation, suspend and resume powers, termination, deadline boundaries, preconditions, constraints, surviving obligations, whole-contract suspension — plus three edits across the two studied grammar editions. Statuses compare by exact string equality after a published mapping table.

Choosing and combining

Choose Symboleo when the question ranges over paths: exhaustive safety and liveness properties of a small contract model, with powers as first-class citizens. Look to Arxo when the question is one case with its grounds, dated editions, and source-anchored review. Combined, Symboleo can verify the lifecycle design while Arxo decides and explains individual cases against the pinned text.

Evidence and open questions

• Sources checked: September 2026 (both grammars read whole, both domain texts, the axiom set, hashes matching).
• Studied profile: the classic and the newer grammar editions at pins, with the headless checker release; the external checker version is fixed only at run time.
• Basis: confirmed by documentation plus a prepared protocol; comparative run not performed. Expected states are predictions, not results.
• Open: surviving-obligation semantics, cross-edition pairs recorded as non-comparable, and any size-ratio figures, which are historical and foreign-version — not findings.

Sources and reproducible materials

• Shared scenario: One contract, four systems.
• Specification and checker projects: github.com/Smart-Contract-Modelling-uOttawa/SymboleoPC
• Formal semantics paper (SoSyM): site.uottawa.ca/~luigi/papers/22_SoSym.pdf