The trade finance letter of credit contract models an international documentary credit lifecycle under UCP 600 rules. Five distinct personas represent the parties in an LC transaction: applicant, beneficiary, issuing bank, advising bank, and confirming bank. The contract uses HandoffStep to model the document flow between parties, bounded quantification for document compliance verification, and Money/Date types for amount and deadline checks.

Business Domain

A Letter of Credit (LC) is a payment guarantee used in international trade. The issuing bank (on behalf of the importer/applicant) guarantees payment to the beneficiary (exporter) upon presentation of compliant documents. The process:

1. The issuing bank opens the LC for a specified amount and expiry date
2. The beneficiary ships goods and assembles required documents (bill of lading, commercial invoice, packing list, certificate of origin, insurance certificate)
3. The beneficiary presents documents to the advising bank
4. The advising bank examines documents and forwards to the issuing bank
5. The issuing bank checks compliance: are all documents present and valid? Is the draft amount within the LC amount? Is the presentation within the expiry date?
6. If compliant, the issuing bank accepts and pays. If discrepant, the discrepancy is raised.

This follows the Uniform Customs and Practice for Documentary Credits (UCP 600), the international standard governing LC transactions.

Why This Domain

Trade finance exercises Tenor features focused on multi-party orchestration and document compliance:

• Five personas representing distinct legal parties in an international transaction
• HandoffStep chains modeling the physical flow of documents between parties
• Money type for LC amount and draft amount comparison
• Date type for expiry date compliance
• Bounded quantification over document requirements (all present, all valid)
• Two entities with parallel state machines (LetterOfCredit and Document)
• Multi-entity effects where presentation and examination affect both entities simultaneously

Contract Structure

Entities

Entity	States	Initial	Transitions
LetterOfCredit	issued, amended, presented, examined, discrepant, accepted, paid, expired	issued	issued->amended, issued->presented, issued->expired, amended->presented, amended->expired, presented->examined, examined->accepted, examined->discrepant, discrepant->examined, accepted->paid, accepted->expired
Document	pending, submitted, examined, accepted, rejected	pending	pending->submitted, submitted->examined, examined->accepted, examined->rejected, rejected->submitted

The LetterOfCredit entity has 8 states and 11 transitions, including the discrepant->examined transition that allows re-examination after discrepancy resolution. The Document entity tracks the document package through its own lifecycle, with rejected->submitted allowing re-presentation.

Personas

Persona	Authority
applicant	Importer who requests the LC (declared, reserved for amendments)
beneficiary	Exporter who presents documents
issuing_bank	Opens the LC, accepts presentation, pays beneficiary, raises discrepancies
advising_bank	Examines documents on behalf of issuing bank, raises discrepancies
confirming_bank	Adds confirmation to the LC (declared, reserved for confirmation extensions)

Facts and Sources

Fact	Type	Source	Default
lc_amount	Money(USD)	lc_service.face_value	--
draft_amount	Money(USD)	presentation_service.draft_amount	--
expiry_date	Date	lc_service.expiry_date	--
presentation_date	Date	presentation_service.presentation_date	--
required_documents	List(DocumentRequirement, max: 20)	lc_service.required_documents	--
invoice_submitted	Bool	presentation_service.invoice_submitted	false
transport_doc_submitted	Bool	presentation_service.transport_doc_submitted	false
documents_received	Bool	presentation_service.documents_received	false
discrepancy_type	Enum(5 values)	examination_service.discrepancy_type	"none"

Named Types

type DocumentRequirement {
  doc_name:  Text(max_length: 64)
  required:  Bool
  present:   Bool
  valid:     Bool
}

Verdict Chain

Stratum 0 -- Individual Compliance Checks

Rule	Condition	Verdict
all_documents_present	forall doc in required_documents . doc.present = true	documents_complete
all_documents_valid	forall doc in required_documents . doc.valid = true	documents_validated
amount_within_lc	draft_amount <= lc_amount	amount_valid
presentation_before_expiry	presentation_date <= expiry_date	within_deadline
invoice_present	invoice_submitted = true	invoice_verified
transport_document_present	transport_doc_submitted = true	transport_doc_verified

The six stratum 0 rules cover the core UCP 600 compliance checks: document completeness, document validity, amount compliance, deadline compliance, and key document presence.

Stratum 1 -- Composite Compliance Determination

Rule	Dependencies	Verdict
documents_fully_compliant	documents_complete AND documents_validated AND amount_valid AND within_deadline AND invoice_verified AND transport_doc_verified	presentation_compliant
discrepancy_detected	NOT documents_complete OR NOT amount_valid OR NOT within_deadline	has_discrepancy

Full compliance requires ALL six conditions. Discrepancy triggers on any of three critical failures (missing documents, wrong amount, late presentation). Note the asymmetry: document validity and individual document presence (invoice, transport) are required for full compliance but do not independently trigger discrepancy -- they are necessary-but-not-sufficient for compliance, and their absence results in non-compliance rather than a formal discrepancy.

Flow Orchestration

lc_presentation_flow

The flow uses two HandoffSteps to model the physical document flow between parties:

1. step_present (OperationStep) -- Beneficiary presents documents (transitions both LC and Document entities)
2. step_handoff_advising (HandoffStep) -- Authority transfers from beneficiary to advising bank
3. step_examine (OperationStep) -- Advising bank examines documents
4. step_handoff_issuing (HandoffStep) -- Authority transfers from advising bank to issuing bank
5. step_check_compliance (BranchStep) -- Routes on presentation_compliant
   • If true: step_accept -> step_pay -- Issuing bank accepts and pays
   • If false: step_raise_discrepancy -- Advising bank raises discrepancy

The two HandoffSteps model the real-world document flow: beneficiary -> advising bank -> issuing bank. Each handoff is a formal authority transfer tracked in the provenance chain.

Complete Contract Source

// Trade Finance: Letter of Credit Contract
// Models an international documentary credit lifecycle under UCP 600 rules.
// Exercises: multi-party personas (5), Money types/comparisons, Date types,
// document entity state machine, bounded quantification, HandoffStep,
// BranchStep for compliance routing.
//
// Domain: International trade -- issuing bank opens LC for importer (applicant),
// beneficiary (exporter) presents documents through advising bank, documents
// are examined for compliance, accepted or rejected, and payment is made.

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

type DocumentRequirement {
  doc_name:  Text(max_length: 64)
  required:  Bool
  present:   Bool
  valid:     Bool
}

// ── Personas ─────────────────────────────────────────────────────────────────
// Five distinct parties in a letter of credit transaction:

persona applicant
persona beneficiary
persona issuing_bank
persona advising_bank
persona confirming_bank

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

fact lc_amount {
  type:   Money(currency: "USD")
  source: "lc_service.face_value"
}

fact draft_amount {
  type:   Money(currency: "USD")
  source: "presentation_service.draft_amount"
}

fact expiry_date {
  type:   Date
  source: "lc_service.expiry_date"
}

fact presentation_date {
  type:   Date
  source: "presentation_service.presentation_date"
}

fact required_documents {
  type:   List(element_type: DocumentRequirement, max: 20)
  source: "lc_service.required_documents"
}

fact invoice_submitted {
  type:    Bool
  source:  "presentation_service.invoice_submitted"
  default: false
}

fact transport_doc_submitted {
  type:    Bool
  source:  "presentation_service.transport_doc_submitted"
  default: false
}

fact documents_received {
  type:    Bool
  source:  "presentation_service.documents_received"
  default: false
}

fact discrepancy_type {
  type:   Enum(values: ["none", "late_presentation", "incorrect_amount", "missing_document", "data_mismatch"])
  source: "examination_service.discrepancy_type"
  default: "none"
}

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

entity LetterOfCredit {
  states:  [issued, amended, presented, examined, discrepant, accepted, paid, expired]
  initial: issued
  transitions: [
    (issued, amended),
    (issued, presented),
    (issued, expired),
    (amended, presented),
    (amended, expired),
    (presented, examined),
    (examined, accepted),
    (examined, discrepant),
    (discrepant, examined),
    (accepted, paid),
    (accepted, expired)
  ]
}

entity Document {
  states:  [pending, submitted, examined, accepted, rejected]
  initial: pending
  transitions: [
    (pending, submitted),
    (submitted, examined),
    (examined, accepted),
    (examined, rejected),
    (rejected, submitted)
  ]
}

// ── Rules -- Stratum 0 ──────────────────────────────────────────────────────
// Individual compliance checks on presentation documents.

rule all_documents_present {
  stratum: 0
  when:    ∀ doc ∈ required_documents . doc.present = true
  produce: verdict documents_complete { payload: Bool = true }
}

rule all_documents_valid {
  stratum: 0
  when:    ∀ doc ∈ required_documents . doc.valid = true
  produce: verdict documents_validated { payload: Bool = true }
}

rule amount_within_lc {
  stratum: 0
  when:    draft_amount <= lc_amount
  produce: verdict amount_valid { payload: Bool = true }
}

rule presentation_before_expiry {
  stratum: 0
  when:    presentation_date <= expiry_date
  produce: verdict within_deadline { payload: Bool = true }
}

rule invoice_present {
  stratum: 0
  when:    invoice_submitted = true
  produce: verdict invoice_verified { payload: Bool = true }
}

rule transport_document_present {
  stratum: 0
  when:    transport_doc_submitted = true
  produce: verdict transport_doc_verified { payload: Bool = true }
}

// ── Rules -- Stratum 1 ──────────────────────────────────────────────────────
// Composite compliance determination using stratum-0 verdicts.

rule documents_fully_compliant {
  stratum: 1
  when:    verdict_present(documents_complete)
         ∧ verdict_present(documents_validated)
         ∧ verdict_present(amount_valid)
         ∧ verdict_present(within_deadline)
         ∧ verdict_present(invoice_verified)
         ∧ verdict_present(transport_doc_verified)
  produce: verdict presentation_compliant { payload: Bool = true }
}

rule discrepancy_detected {
  stratum: 1
  when:    ¬verdict_present(documents_complete)
         ∨ ¬verdict_present(amount_valid)
         ∨ ¬verdict_present(within_deadline)
  produce: verdict has_discrepancy { payload: Bool = true }
}

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

operation present_documents {
  allowed_personas: [beneficiary]
  precondition:     documents_received = true
  effects:          [(LetterOfCredit, issued, presented), (Document, pending, submitted)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation examine_documents {
  allowed_personas: [advising_bank]
  precondition:     documents_received = true
  effects:          [(LetterOfCredit, presented, examined), (Document, submitted, examined)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation accept_presentation {
  allowed_personas: [issuing_bank]
  precondition:     verdict_present(presentation_compliant)
  effects:          [(LetterOfCredit, examined, accepted), (Document, examined, accepted)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation pay_beneficiary {
  allowed_personas: [issuing_bank]
  precondition:     verdict_present(presentation_compliant)
  effects:          [(LetterOfCredit, accepted, paid)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation raise_discrepancy {
  allowed_personas: [advising_bank, issuing_bank]
  precondition:     verdict_present(has_discrepancy)
  effects:          [(LetterOfCredit, examined, discrepant), (Document, examined, rejected)]
  error_contract:   [precondition_failed, persona_rejected]
}

// ── Flows ────────────────────────────────────────────────────────────────────
// Main LC presentation and examination workflow.
// Beneficiary presents documents -> advising bank examines -> if compliant,
// issuing bank accepts and pays; if discrepant, discrepancy is raised.

flow lc_presentation_flow {
  snapshot: at_initiation
  entry:    step_present

  steps: {
    step_present: OperationStep {
      op:      present_documents
      persona: beneficiary
      outcomes: {
        success: step_handoff_advising
      }
      on_failure: Terminate(outcome: failure)
    }

    step_handoff_advising: HandoffStep {
      from_persona: beneficiary
      to_persona:   advising_bank
      next:         step_examine
    }

    step_examine: OperationStep {
      op:      examine_documents
      persona: advising_bank
      outcomes: {
        success: step_handoff_issuing
      }
      on_failure: Terminate(outcome: failure)
    }

    step_handoff_issuing: HandoffStep {
      from_persona: advising_bank
      to_persona:   issuing_bank
      next:         step_check_compliance
    }

    step_check_compliance: BranchStep {
      condition: verdict_present(presentation_compliant)
      persona:   issuing_bank
      if_true:   step_accept
      if_false:  step_raise_discrepancy
    }

    step_accept: OperationStep {
      op:      accept_presentation
      persona: issuing_bank
      outcomes: {
        success: step_pay
      }
      on_failure: Terminate(outcome: failure)
    }

    step_pay: OperationStep {
      op:      pay_beneficiary
      persona: issuing_bank
      outcomes: {
        success: Terminal(success)
      }
      on_failure: Terminate(outcome: failure)
    }

    step_raise_discrepancy: OperationStep {
      op:      raise_discrepancy
      persona: advising_bank
      outcomes: {
        success: Terminal(discrepant)
      }
      on_failure: Terminate(outcome: failure)
    }
  }
}

Static Analysis Output

$ tenor check letter_of_credit.tenor

  Elaborating letter_of_credit.tenor ...

  ── Types ──────────────────────────────────────────────────────────
  DocumentRequirement                     4 fields    ok

  ── Facts ──────────────────────────────────────────────────────────
  lc_amount                Money(USD)                  ok
  draft_amount             Money(USD)                  ok
  expiry_date              Date                        ok
  presentation_date        Date                        ok
  required_documents       List(DocReq, 20)            ok
  invoice_submitted        Bool           default      ok
  transport_doc_submitted  Bool           default      ok
  documents_received       Bool           default      ok
  discrepancy_type         Enum(5)        default      ok

  ── Entities ───────────────────────────────────────────────────────
  LetterOfCredit           8 states  11 transitions    ok
  Document                 5 states   5 transitions    ok

  ── Rules ──────────────────────────────────────────────────────────
  Stratum 0:
    all_documents_present        → documents_complete       ok
    all_documents_valid          → documents_validated      ok
    amount_within_lc             → amount_valid             ok
    presentation_before_expiry   → within_deadline          ok
    invoice_present              → invoice_verified         ok
    transport_document_present   → transport_doc_verified   ok
  Stratum 1:
    documents_fully_compliant    → presentation_compliant   ok
    discrepancy_detected         → has_discrepancy          ok

  ── Operations ─────────────────────────────────────────────────────
  present_documents     [beneficiary]                    ok
  examine_documents     [advising_bank]                  ok
  accept_presentation   [issuing_bank]                   ok
  pay_beneficiary       [issuing_bank]                   ok
  raise_discrepancy     [advising_bank, issuing_bank]    ok

  ── Flows ──────────────────────────────────────────────────────────
  lc_presentation_flow  8 steps   2 terminals            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        No compensate handlers (N/A)               PASS

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

Authority Topology

  beneficiary ────────── present_documents ──────→ LetterOfCredit, Document

  advising_bank ────────┬ examine_documents ─────→ LetterOfCredit, Document
                        └ raise_discrepancy ─────→ LetterOfCredit, Document

  issuing_bank ─────────┬ accept_presentation ───→ LetterOfCredit, Document
                        ├ pay_beneficiary ───────→ LetterOfCredit
                        └ raise_discrepancy ─────→ LetterOfCredit, Document

Authority flows along the document chain: beneficiary presents, advising bank examines, issuing bank accepts and pays. Both the advising bank and issuing bank can raise discrepancies, reflecting the UCP 600 requirement that either party can identify non-compliance.

Flow Path Enumeration

lc_presentation_flow

Path	Steps	Outcome
Compliant presentation	step_present -> handoff_advising -> step_examine -> handoff_issuing -> check_compliance[true] -> step_accept -> step_pay	Terminal(success)
Discrepant presentation	step_present -> handoff_advising -> step_examine -> handoff_issuing -> check_compliance[false] -> step_raise_discrepancy	Terminal(discrepant)
Presentation failure	step_present[fail]	Terminate(failure)
Examination failure	step_present -> handoff_advising -> step_examine[fail]	Terminate(failure)
Acceptance failure	... -> step_accept[fail]	Terminate(failure)
Payment failure	... -> step_accept -> step_pay[fail]	Terminate(failure)
Discrepancy raise failure	... -> step_raise_discrepancy[fail]	Terminate(failure)

Sample Fact Sets

Compliant Presentation

All 5 required documents present and valid, draft amount within LC amount, presentation before expiry:

{
  "lc_amount": {"amount": "250000.00", "currency": "USD"},
  "draft_amount": {"amount": "245000.00", "currency": "USD"},
  "expiry_date": "2025-06-30",
  "presentation_date": "2025-06-15",
  "required_documents": [
    {"doc_name": "Bill of Lading", "required": true, "present": true, "valid": true},
    {"doc_name": "Commercial Invoice", "required": true, "present": true, "valid": true},
    {"doc_name": "Packing List", "required": true, "present": true, "valid": true},
    {"doc_name": "Certificate of Origin", "required": true, "present": true, "valid": true},
    {"doc_name": "Insurance Certificate", "required": true, "present": true, "valid": true}
  ],
  "invoice_submitted": true,
  "transport_doc_submitted": true,
  "documents_received": true,
  "discrepancy_type": "none"
}

Discrepant Presentation

Draft amount exceeds LC amount, packing list missing, discrepancy_type is missing_document:

{
  "lc_amount": {"amount": "250000.00", "currency": "USD"},
  "draft_amount": {"amount": "275000.00", "currency": "USD"},
  "expiry_date": "2025-06-30",
  "presentation_date": "2025-06-15",
  "required_documents": [
    {"doc_name": "Bill of Lading", "required": true, "present": true, "valid": true},
    {"doc_name": "Commercial Invoice", "required": true, "present": true, "valid": true},
    {"doc_name": "Packing List", "required": true, "present": false, "valid": false},
    {"doc_name": "Certificate of Origin", "required": true, "present": true, "valid": true},
    {"doc_name": "Insurance Certificate", "required": true, "present": true, "valid": true}
  ],
  "invoice_submitted": true,
  "transport_doc_submitted": true,
  "documents_received": true,
  "discrepancy_type": "missing_document"
}

Sample Evaluation Output

Compliant Presentation

$ tenor eval letter_of_credit.tenor --facts lc_present.facts.json

  Evaluating with 9 facts ...

  ── Stratum 0 ──────────────────────────────────────────────────────
  ✓ all_documents_present        → documents_complete       = true
    provenance: [required_documents]
  ✓ all_documents_valid          → documents_validated      = true
    provenance: [required_documents]
  ✓ amount_within_lc             → amount_valid             = true
    provenance: [draft_amount, lc_amount]
  ✓ presentation_before_expiry   → within_deadline          = true
    provenance: [presentation_date, expiry_date]
  ✓ invoice_present              → invoice_verified         = true
    provenance: [invoice_submitted]
  ✓ transport_document_present   → transport_doc_verified   = true
    provenance: [transport_doc_submitted]

  ── Stratum 1 ──────────────────────────────────────────────────────
  ✓ documents_fully_compliant    → presentation_compliant   = true
    provenance: [documents_complete, documents_validated, amount_valid,
                 within_deadline, invoice_verified, transport_doc_verified]
  · discrepancy_detected         — not satisfied (all checks pass)

  ── Flow: lc_presentation_flow ─────────────────────────────────────
  step_present          → success (present_documents as beneficiary)
  step_handoff_advising → handoff (beneficiary → advising_bank)
  step_examine          → success (examine_documents as advising_bank)
  step_handoff_issuing  → handoff (advising_bank → issuing_bank)
  step_check_compliance → true    (presentation_compliant present)
  step_accept           → success (accept_presentation as issuing_bank)
  step_pay              → success (pay_beneficiary as issuing_bank)
  Flow outcome: success

  ── Entity States ──────────────────────────────────────────────────
  LetterOfCredit: issued → presented → examined → accepted → paid
  Document:       pending → submitted → examined → accepted

  7 verdicts produced, 8 entity transitions, flow outcome: success

Discrepant Presentation

$ tenor eval letter_of_credit.tenor --facts lc_discrepancy.facts.json

  Evaluating with 9 facts ...

  ── Stratum 0 ──────────────────────────────────────────────────────
  · all_documents_present        — not satisfied (Packing List missing)
  · all_documents_valid          — not satisfied (Packing List invalid)
  · amount_within_lc             — not satisfied ($275K > $250K)
  ✓ presentation_before_expiry   → within_deadline          = true
    provenance: [presentation_date, expiry_date]
  ✓ invoice_present              → invoice_verified         = true
    provenance: [invoice_submitted]
  ✓ transport_document_present   → transport_doc_verified   = true
    provenance: [transport_doc_submitted]

  ── Stratum 1 ──────────────────────────────────────────────────────
  · documents_fully_compliant    — not satisfied (3 checks failed)
  ✓ discrepancy_detected         → has_discrepancy          = true
    provenance: [documents_complete absent, amount_valid absent]

  ── Flow: lc_presentation_flow ─────────────────────────────────────
  step_present          → success (present_documents as beneficiary)
  step_handoff_advising → handoff (beneficiary → advising_bank)
  step_examine          → success (examine_documents as advising_bank)
  step_handoff_issuing  → handoff (advising_bank → issuing_bank)
  step_check_compliance → false   (presentation_compliant absent)
  step_raise_discrepancy → success (raise_discrepancy as advising_bank)
  Flow outcome: discrepant

  ── Entity States ──────────────────────────────────────────────────
  LetterOfCredit: issued → presented → examined → discrepant
  Document:       pending → submitted → examined → rejected

  4 verdicts produced, 8 entity transitions, flow outcome: discrepant

Formal Properties and Patterns

HandoffStep chains for multi-party orchestration: The two HandoffSteps (beneficiary -> advising bank -> issuing bank) model the physical flow of documents between parties. Each handoff is recorded in the provenance chain, creating an auditable trail of authority transfers. This is critical for UCP 600 compliance, where the chain of custody matters.

Parallel entity state machines: LetterOfCredit and Document progress through their states in lockstep: when documents are presented, both entities transition; when documents are examined, both transition; when documents are accepted or rejected, both transition. Multi-entity effects enforce this coordination.

Re-presentation via rejected->submitted: The Document entity allows rejected->submitted, modeling the UCP 600 provision where a beneficiary can correct and re-present documents after a discrepancy is found. Similarly, discrepant->examined on LetterOfCredit allows re-examination.

Bounded quantification over documents: Both all_documents_present and all_documents_valid use forall doc in required_documents to check every document in the presentation. A single missing or invalid document blocks compliance. This matches the UCP 600 standard where partial compliance is treated as non-compliance.

Money and Date comparisons: The amount_within_lc rule uses draft_amount <= lc_amount for currency-safe Money comparison. The presentation_before_expiry rule uses presentation_date <= expiry_date for Date comparison. Tenor's type system ensures these comparisons are semantically valid.

Asymmetric compliance/discrepancy rules: Full compliance requires six verdicts (strict conjunction). Discrepancy triggers on three critical failures (disjunction). This means some failures (invalid documents, missing invoice without missing all documents) result in non-compliance without a formal discrepancy -- they are compliance failures that prevent acceptance but do not generate a discrepancy notice. This models real-world LC practice where not all non-compliance rises to the level of a formal discrepancy.

Default values for safety: documents_received, invoice_submitted, and transport_doc_submitted all default to false. This ensures that if the presentation service is unavailable, the system defaults to "not received" rather than accidentally processing an incomplete presentation.