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

## 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](/comparisons/contract-lifecycle/).
- Specification and checker projects:
  [github.com/Smart-Contract-Modelling-uOttawa/SymboleoPC](https://github.com/Smart-Contract-Modelling-uOttawa/SymboleoPC)
- Formal semantics paper (SoSyM):
  [site.uottawa.ca/~luigi/papers/22_SoSym.pdf](https://www.site.uottawa.ca/~luigi/papers/22_SoSym.pdf)