The escrow release contract is the canonical integration test from Appendix D of the Tenor specification. It exercises every construct type in a single file: named types, facts with defaults, two entities with interleaved state machines, stratified rules, bounded universal quantification, seven operations with persona restrictions, and two flows featuring BranchStep, HandoffStep, and Compensate handlers.

Business Domain

This contract models a standard escrow release process for an e-commerce or marketplace transaction. An escrow account holds funds on behalf of a buyer and seller. When delivery is confirmed and all line items are validated, the escrow agent can release funds -- either automatically (within a compliance threshold) or through a compliance officer (for larger amounts). If delivery fails and the buyer requests a refund, the escrow agent processes the refund. Either party can flag a dispute at any time after delivery status is known.

Why This Domain

Escrow transactions are a natural fit for Tenor because they involve:

• Multiple parties with distinct authority (buyer, seller, escrow agent, compliance officer)
• Conditional routing based on financial thresholds
• Compensation logic when operations fail mid-flow
• Authority handoff between personas
• State machines that must be kept consistent across multiple entities

Contract Structure

Entities

Entity	States	Initial	Transitions
EscrowAccount	held, released, refunded, disputed	held	held->released, held->refunded, held->disputed, disputed->released, disputed->refunded
DeliveryRecord	pending, confirmed, failed	pending	pending->confirmed, pending->failed, confirmed->pending

The EscrowAccount models the lifecycle of funds. The DeliveryRecord tracks the physical delivery state. Note the confirmed->pending transition on DeliveryRecord -- this enables the compensation pattern where a delivery confirmation is reverted if the release operation fails.

Personas

Persona	Authority
buyer	Can flag disputes
seller	Can confirm delivery, flag disputes
escrow_agent	Can release/refund escrow, record failures, revert confirmations
compliance_officer	Can release escrow for high-value transactions

Facts and Sources

Fact	Type	Source	Default
escrow_amount	Money(USD)	escrow_service.current_balance	--
delivery_status	Enum: pending, confirmed, failed	delivery_service.status	--
line_items	List(LineItemRecord, max: 100)	order_service.line_items	--
compliance_threshold	Money(USD)	compliance_service.release_threshold	$10,000.00
buyer_requested_refund	Bool	buyer_portal.refund_requested	false

Named Types

type LineItemRecord {
  id:          Text(max_length: 64)
  description: Text(max_length: 256)
  amount:      Money(currency: "USD")
  valid:       Bool
}

Verdict Chain

Stratum 0 -- Fact-Level Checks

Rules at stratum 0 evaluate directly against facts:

Rule	Condition	Verdict
all_line_items_valid	forall item in line_items . item.valid = true	line_items_validated
delivery_confirmed	delivery_status = "confirmed"	delivery_confirmed
delivery_failed	delivery_status = "failed"	delivery_failed
amount_within_threshold	escrow_amount <= compliance_threshold	within_threshold
refund_requested	buyer_requested_refund = true	refund_requested

Stratum 1 -- Composite Decisions

Rules at stratum 1 compose stratum 0 verdicts:

Rule	Dependencies	Verdict
can_release_without_compliance	line_items_validated AND delivery_confirmed AND within_threshold	release_approved (payload: "auto")
requires_compliance_review	line_items_validated AND delivery_confirmed AND NOT within_threshold	compliance_review_required
can_refund	delivery_failed AND refund_requested	refund_approved

This creates a clear decision tree: small releases are auto-approved, large releases need compliance review, and refunds require both delivery failure and buyer request.

Flow Orchestration

standard_release Flow

The primary flow demonstrates BranchStep, HandoffStep, and Compensate:

1. step_confirm (OperationStep) -- Seller confirms delivery
2. step_check_threshold (BranchStep) -- Routes based on within_threshold verdict
   • If true: step_auto_release -- Escrow agent releases funds
   • If false: step_handoff_compliance -- HandoffStep transfers authority to compliance officer
3. step_compliance_release (OperationStep) -- Compliance officer releases funds

Both release steps include Compensate handlers that revert the delivery confirmation if the release operation fails, ensuring transactional consistency.

refund_flow Flow

A minimal single-step flow where the escrow agent processes a refund:

1. step_refund (OperationStep) -- Escrow agent refunds the escrow

Complete Contract Source

// Integration test: Escrow Release Contract (Appendix D)
// Exercises: all construct types, bounded quantification, compensation, HandoffStep,
// BranchStep, multi-persona authority, multi-entity effects, stratum 0 and 1 rules
// Expected: elaborates without error, produces integration_escrow.expected.json

// ── Named Types ──────────────────────────────────────────────────────────────

type LineItemRecord {
  id:          Text(max_length: 64)
  description: Text(max_length: 256)
  amount:      Money(currency: "USD")
  valid:       Bool
}

// ── Facts ─────────────────────────────────────────────────────────────────────

fact escrow_amount {
  type:   Money(currency: "USD")
  source: "escrow_service.current_balance"
}

fact delivery_status {
  type:   Enum(values: ["pending", "confirmed", "failed"])
  source: "delivery_service.status"
}

fact line_items {
  type:   List(element_type: LineItemRecord, max: 100)
  source: "order_service.line_items"
}

fact compliance_threshold {
  type:    Money(currency: "USD")
  source:  "compliance_service.release_threshold"
  default: Money { amount: "10000.00", currency: "USD" }
}

fact buyer_requested_refund {
  type:    Bool
  source:  "buyer_portal.refund_requested"
  default: false
}

// ── Entities ──────────────────────────────────────────────────────────────────

entity EscrowAccount {
  states:  [held, released, refunded, disputed]
  initial: held
  transitions: [
    (held, released),
    (held, refunded),
    (held, disputed),
    (disputed, released),
    (disputed, refunded)
  ]
}

entity DeliveryRecord {
  states:  [pending, confirmed, failed]
  initial: pending
  transitions: [
    (pending, confirmed),
    (pending, failed),
    (confirmed, pending)
  ]
}

// ── Rules — Stratum 0 ────────────────────────────────────────────────────────

rule all_line_items_valid {
  stratum: 0
  when:    ∀ item ∈ line_items . item.valid = true
  produce: verdict line_items_validated { payload: Bool = true }
}

rule delivery_confirmed {
  stratum: 0
  when:    delivery_status = "confirmed"
  produce: verdict delivery_confirmed { payload: Bool = true }
}

rule delivery_failed {
  stratum: 0
  when:    delivery_status = "failed"
  produce: verdict delivery_failed { payload: Bool = true }
}

rule amount_within_threshold {
  stratum: 0
  when:    escrow_amount <= compliance_threshold
  produce: verdict within_threshold { payload: Bool = true }
}

rule refund_requested {
  stratum: 0
  when:    buyer_requested_refund = true
  produce: verdict refund_requested { payload: Bool = true }
}

// ── Rules — Stratum 1 ────────────────────────────────────────────────────────

rule can_release_without_compliance {
  stratum: 1
  when:    verdict_present(line_items_validated)
         ∧ verdict_present(delivery_confirmed)
         ∧ verdict_present(within_threshold)
  produce: verdict release_approved { payload: Text = "auto" }
}

rule requires_compliance_review {
  stratum: 1
  when:    verdict_present(line_items_validated)
         ∧ verdict_present(delivery_confirmed)
         ∧ ¬verdict_present(within_threshold)
  produce: verdict compliance_review_required { payload: Bool = true }
}

rule can_refund {
  stratum: 1
  when:    verdict_present(delivery_failed)
         ∧ verdict_present(refund_requested)
  produce: verdict refund_approved { payload: Bool = true }
}

// ── Operations ────────────────────────────────────────────────────────────────

operation release_escrow {
  allowed_personas: [escrow_agent]
  precondition:     verdict_present(release_approved)
  effects:          [(EscrowAccount, held, released)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation release_escrow_with_compliance {
  allowed_personas: [compliance_officer]
  precondition:     verdict_present(compliance_review_required)
  effects:          [(EscrowAccount, held, released)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation refund_escrow {
  allowed_personas: [escrow_agent]
  precondition:     verdict_present(refund_approved)
  effects:          [(EscrowAccount, held, refunded)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation flag_dispute {
  allowed_personas: [buyer, seller]
  precondition:     verdict_present(delivery_confirmed)
                  ∨ verdict_present(delivery_failed)
  effects:          [(EscrowAccount, held, disputed)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation confirm_delivery {
  allowed_personas: [seller]
  precondition:     ∀ item ∈ line_items . item.valid = true
  effects:          [(DeliveryRecord, pending, confirmed)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation record_delivery_failure {
  allowed_personas: [escrow_agent]
  precondition:     verdict_present(delivery_failed)
  effects:          [(DeliveryRecord, pending, failed)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation revert_delivery_confirmation {
  allowed_personas: [escrow_agent]
  precondition:     verdict_present(delivery_confirmed)
  effects:          [(DeliveryRecord, confirmed, pending)]
  error_contract:   [precondition_failed, persona_rejected]
}

// ── Flows ─────────────────────────────────────────────────────────────────────

flow standard_release {
  snapshot: at_initiation
  entry:    step_confirm

  steps: {
    step_confirm: OperationStep {
      op:      confirm_delivery
      persona: seller
      outcomes: {
        success: step_check_threshold
      }
      on_failure: Terminate(outcome: failure)
    }

    step_check_threshold: BranchStep {
      condition: verdict_present(within_threshold)
      persona:   escrow_agent
      if_true:   step_auto_release
      if_false:  step_handoff_compliance
    }

    step_auto_release: OperationStep {
      op:      release_escrow
      persona: escrow_agent
      outcomes: {
        success: Terminal(success)
      }
      on_failure: Compensate(
        steps: [{
          op:         revert_delivery_confirmation
          persona:    escrow_agent
          on_failure: Terminal(failure)
        }]
        then: Terminal(failure)
      )
    }

    step_handoff_compliance: HandoffStep {
      from_persona: escrow_agent
      to_persona:   compliance_officer
      next:         step_compliance_release
    }

    step_compliance_release: OperationStep {
      op:      release_escrow_with_compliance
      persona: compliance_officer
      outcomes: {
        success: Terminal(success)
      }
      on_failure: Compensate(
        steps: [{
          op:         revert_delivery_confirmation
          persona:    escrow_agent
          on_failure: Terminal(failure)
        }]
        then: Terminal(failure)
      )
    }
  }
}

flow refund_flow {
  snapshot: at_initiation
  entry:    step_refund

  steps: {
    step_refund: OperationStep {
      op:      refund_escrow
      persona: escrow_agent
      outcomes: {
        success: Terminal(success)
      }
      on_failure: Terminate(outcome: failure)
    }
  }
}

Static Analysis Output

$ tenor check integration_escrow.tenor

  Elaborating integration_escrow.tenor ...

  ── Types ──────────────────────────────────────────────────────────
  LineItemRecord                          4 fields    ok

  ── Facts ──────────────────────────────────────────────────────────
  escrow_amount            Money(USD)                 ok
  delivery_status          Enum(3)                    ok
  line_items               List(LineItemRecord, 100)  ok
  compliance_threshold     Money(USD)     default     ok
  buyer_requested_refund   Bool           default     ok

  ── Entities ───────────────────────────────────────────────────────
  EscrowAccount            4 states   5 transitions   ok
  DeliveryRecord           3 states   3 transitions   ok

  ── Rules ──────────────────────────────────────────────────────────
  Stratum 0:
    all_line_items_valid          → line_items_validated        ok
    delivery_confirmed            → delivery_confirmed          ok
    delivery_failed               → delivery_failed             ok
    amount_within_threshold       → within_threshold            ok
    refund_requested              → refund_requested            ok
  Stratum 1:
    can_release_without_compliance → release_approved           ok
    requires_compliance_review     → compliance_review_required ok
    can_refund                     → refund_approved            ok

  ── Operations ─────────────────────────────────────────────────────
  release_escrow                  [escrow_agent]               ok
  release_escrow_with_compliance  [compliance_officer]         ok
  refund_escrow                   [escrow_agent]               ok
  flag_dispute                    [buyer, seller]              ok
  confirm_delivery                [seller]                     ok
  record_delivery_failure         [escrow_agent]               ok
  revert_delivery_confirmation    [escrow_agent]               ok

  ── Flows ──────────────────────────────────────────────────────────
  standard_release          5 steps   2 terminals              ok
  refund_flow               1 step    1 terminal               ok

  ── S-Properties ───────────────────────────────────────────────────
  S1  Determinism         All rules produce deterministic verdicts   PASS
  S2  Stratification      2 strata, no circular dependencies        PASS
  S3  Totality            All verdict references resolve             PASS
  S4  Reachability        All entity states reachable                PASS
  S5  Authority           All operations have authorized personas    PASS
  S6  Termination         All flow paths reach terminal states       PASS
  S7  Compensation        All compensate handlers are well-formed    PASS

  ✓ integration_escrow.tenor — 7/7 S-properties satisfied

Authority Topology

  seller ──────────────┐
                       ├── confirm_delivery ──→ DeliveryRecord
                       ├── flag_dispute ──────→ EscrowAccount
  buyer ───────────────┘

  escrow_agent ────────┬── release_escrow ────────────→ EscrowAccount
                       ├── refund_escrow ─────────────→ EscrowAccount
                       ├── record_delivery_failure ───→ DeliveryRecord
                       └── revert_delivery_confirmation → DeliveryRecord

  compliance_officer ──┬── release_escrow_with_compliance → EscrowAccount

The authority topology shows clear separation of concerns:

• Seller controls delivery confirmation and can flag disputes
• Buyer can only flag disputes (no unilateral power over funds)
• Escrow agent manages all escrow operations and delivery failure recording
• Compliance officer has authority only for high-value releases (via HandoffStep)

Flow Path Enumeration

standard_release

Path	Steps	Outcome
Auto-release (happy path)	step_confirm -> step_check_threshold[true] -> step_auto_release	Terminal(success)
Compliance release	step_confirm -> step_check_threshold[false] -> step_handoff_compliance -> step_compliance_release	Terminal(success)
Auto-release with compensation	step_confirm -> step_check_threshold[true] -> step_auto_release[fail] -> compensate(revert_delivery_confirmation)	Terminal(failure)
Compliance release with compensation	step_confirm -> step_check_threshold[false] -> step_handoff_compliance -> step_compliance_release[fail] -> compensate(revert_delivery_confirmation)	Terminal(failure)
Confirm delivery failure	step_confirm[fail]	Terminate(failure)

refund_flow

Path	Steps	Outcome
Refund success	step_refund	Terminal(success)
Refund failure	step_refund[fail]	Terminate(failure)

Sample Fact Set

The following fact set exercises the auto-release happy path (escrow amount within threshold, delivery confirmed, all line items valid):

{
  "escrow_amount": {"amount": "8500.00", "currency": "USD"},
  "delivery_status": "confirmed",
  "compliance_threshold": {"amount": "10000.00", "currency": "USD"},
  "buyer_requested_refund": false,
  "line_items": [
    {"id": "L1", "description": "Widget A", "amount": {"amount": "5000.00", "currency": "USD"}, "valid": true},
    {"id": "L2", "description": "Widget B", "amount": {"amount": "3500.00", "currency": "USD"}, "valid": true}
  ]
}

Sample Evaluation Output

$ tenor eval integration_escrow.tenor --facts escrow_release.facts.json

  Evaluating with 5 facts ...

  ── Stratum 0 ──────────────────────────────────────────────────────
  ✓ all_line_items_valid         → line_items_validated    = true
    provenance: [line_items]
  ✓ delivery_confirmed           → delivery_confirmed      = true
    provenance: [delivery_status]
  ✓ amount_within_threshold      → within_threshold        = true
    provenance: [escrow_amount, compliance_threshold]
  · delivery_failed              — not satisfied (delivery_status ≠ "failed")
  · refund_requested             — not satisfied (buyer_requested_refund = false)

  ── Stratum 1 ──────────────────────────────────────────────────────
  ✓ can_release_without_compliance → release_approved       = "auto"
    provenance: [line_items_validated, delivery_confirmed, within_threshold]
  · requires_compliance_review    — not satisfied (within_threshold present)
  · can_refund                    — not satisfied (delivery_failed absent)

  ── Flow: standard_release ─────────────────────────────────────────
  step_confirm          → success (confirm_delivery as seller)
  step_check_threshold  → true   (within_threshold present)
  step_auto_release     → success (release_escrow as escrow_agent)
  Flow outcome: success

  ── Entity States ──────────────────────────────────────────────────
  EscrowAccount:  held → released
  DeliveryRecord: pending → confirmed

  4 verdicts produced, 2 entity transitions, flow outcome: success

Formal Properties and Patterns

This contract demonstrates the following formal properties and design patterns:

Stratified verdict composition: Stratum 0 rules evaluate raw facts. Stratum 1 rules compose stratum 0 verdicts into authorization decisions. This separation ensures rules at each stratum see a stable, complete set of inputs.

Threshold-based routing: The within_threshold verdict drives the BranchStep in the flow, routing to either auto-release or compliance handoff. This pattern is reusable for any dollar-amount tier logic.

Compensation for transactional consistency: Both release operations include Compensate handlers that revert the delivery confirmation. If a release fails after delivery was confirmed, the system doesn't leave the delivery in a confirmed state with no corresponding release -- the compensation handler reverts it.

Authority handoff: The HandoffStep from escrow_agent to compliance_officer models a real organizational boundary. The escrow agent cannot approve high-value releases; authority must be explicitly transferred.

Bounded universal quantification: The all_line_items_valid rule uses forall item in line_items . item.valid = true to ensure every line item in the order has been validated before release.

Mutually exclusive verdicts: The delivery_confirmed and delivery_failed verdicts cannot both be present (the delivery status fact is a single enum value). The stratum 1 rules that depend on them are therefore mutually exclusive by construction.