The energy procurement RFP contract models a realistic Request for Proposal lifecycle for energy commodity procurement. It covers RFP issuance, supplier bid evaluation, approval tiers by spend amount, delegation rules, supplier scoring, contract award, and purchase order generation. The standout features are four-tier approval routing based on Money comparisons and the Escalate handler for failed category-lead awards.

Business Domain

Energy procurement involves purchasing commodity energy (power, gas, renewables) through a formal RFP process. The procurement team publishes an RFP, suppliers submit bids, bids are evaluated on technical merit, price, and reliability, suppliers are shortlisted, and awards are granted based on approval authority tied to the dollar value of the contract.

The approval chain follows a typical corporate hierarchy:

• Up to $50,000: Procurement Manager can approve directly
• $50,001 to $500,000: Category Lead approval required
• $500,001 to $2,000,000: VP of Supply Chain approval required
• Above $2,000,000: CFO approval required

Why This Domain

Energy procurement exercises Tenor features that other domain contracts do not:

• Money type comparisons for tier determination (comparing rfp_amount against literal Money values)
• Four approval tiers implemented as stratum 1 rules feeding into BranchStep routing
• Escalate handler when a category lead denial escalates to VP
• Three strata of rules building from fact checks to tier determination to award recommendation
• Multi-entity effects (RFP + PurchaseOrder on award)
• Multi-file imports for shared types (SupplierScore, CostBreakdown, BidRecord)

Contract Structure

Entities

Entity	States	Initial	Transitions
RFP	draft, published, evaluation, shortlisted, awarded, contracted, cancelled	draft	draft->published, draft->cancelled, published->evaluation, published->cancelled, evaluation->shortlisted, evaluation->cancelled, shortlisted->awarded, shortlisted->cancelled, awarded->contracted, awarded->cancelled
PurchaseOrder	pending, approved, issued, fulfilled	pending	pending->approved, approved->issued, issued->fulfilled

The RFP entity has 7 states and 10 transitions, modeling the full lifecycle including cancellation from any pre-contracted state. The PurchaseOrder is created when the RFP is awarded.

Personas

Persona	Authority
procurement_manager	Publishes RFP, evaluates bids, shortlists suppliers, awards (tier 1), cancels
category_lead	Evaluates bids, shortlists suppliers, awards (tier 2), cancels
vp_supply_chain	Awards (tier 3), approves PO, cancels
cfo	Awards (tier 4), approves PO
supplier	(Declared -- reserved for bid submission extensions)

Facts and Sources

Fact	Type	Source	Default
rfp_amount	Money(USD)	procurement_service.rfp_total_value	--
bid_total	Money(USD)	bid_service.winning_bid_amount	--
rfp_deadline	Date	procurement_service.submission_deadline	--
current_date	Date	system.current_date	--
procurement_stage	Enum(5 values)	procurement_service.stage	--
supplier_bids	List(BidRecord, max: 50)	bid_service.all_bids	--
winning_bid	SupplierScore	bid_service.winning_supplier_scores	--
budget_approved	Bool	finance_service.budget_available	false
compliance_checked	Bool	compliance_service.regulatory_check_passed	false
minimum_score_threshold	Int(0..300)	procurement_service.min_score	180
bid_count	Int(0..50)	bid_service.total_bids	0

Named Types (types.tenor -- imported)

// Energy Procurement RFP Workflow — Shared Types

type SupplierScore {
  technical_score:   Int(min: 0, max: 100)
  price_score:       Int(min: 0, max: 100)
  reliability_score: Int(min: 0, max: 100)
  total_score:       Int(min: 0, max: 300)
}

type CostBreakdown {
  commodity_cost: Money(currency: "USD")
  delivery_cost:  Money(currency: "USD")
  risk_premium:   Money(currency: "USD")
}

type BidRecord {
  supplier_id:   Text(max_length: 64)
  bid_amount:    Money(currency: "USD")
  scores:        SupplierScore
  cost_detail:   CostBreakdown
  compliant:     Bool
}

Verdict Chain

Stratum 0 -- Fact-Level Checks

Rule	Condition	Verdict
budget_available	budget_approved = true	budget_ok
compliance_verified	compliance_checked = true	compliance_ok
deadline_not_passed	current_date <= rfp_deadline	deadline_ok
all_bids_compliant	forall bid in supplier_bids . bid.compliant = true	bids_compliant
sufficient_bids	bid_count >= 2	enough_bids
winning_score_above_threshold	winning_bid.total_score >= minimum_score_threshold	score_ok

Stratum 1 -- Approval Tier Determination

The four tier rules use Money comparisons to determine which persona has approval authority:

Rule	Condition	Verdict
tier_1_procurement_manager	rfp_amount <= $50,000 AND budget_ok	pm_can_approve
tier_2_category_lead	rfp_amount > $50,000 AND rfp_amount <= $500,000 AND budget_ok	cl_approval_required
tier_3_vp_required	rfp_amount > $500,000 AND rfp_amount <= $2,000,000 AND budget_ok	vp_approval_required
tier_4_cfo_required	rfp_amount > $2,000,000 AND budget_ok	cfo_approval_required

These tiers are mutually exclusive by construction -- the amount ranges do not overlap.

Stratum 2 -- Award Recommendation

Rule	Dependencies	Verdict
award_recommended	compliance_ok AND score_ok AND enough_bids AND bids_compliant AND (any tier verdict)	award_ready
award_blocked	NOT budget_ok OR NOT compliance_ok	award_blocked

The award_recommended rule uses disjunction across the tier verdicts: it requires that at least one approval tier has been determined. The award_blocked rule catches cases where budget or compliance are missing.

Flow Orchestration

rfp_approval_flow

A multi-step flow with nested BranchSteps for tier routing and an Escalate handler:

1. step_publish -- Procurement manager publishes the RFP
2. step_evaluate -- Procurement manager evaluates bids
3. step_shortlist -- Procurement manager shortlists suppliers
4. step_check_tier (BranchStep) -- Routes on pm_can_approve
   • If true: step_award_direct -- PM awards directly
   • If false: continue to high-value check
5. step_check_high_value (BranchStep) -- Routes on VP/CFO required
   • If true: step_escalate_to_vp -- VP awards
   • If false: step_award_category_lead -- Category lead awards
6. step_award_category_lead on_failure: Escalate to VP

The Escalate handler on the category lead's award operation models the real-world scenario where a category lead's decision is overridden by their VP.

Complete Contract Source

types.tenor

// Energy Procurement RFP Workflow — Shared Types
// Models supplier evaluation scoring and cost breakdown structures
// used across the RFP approval and award lifecycle.

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

type SupplierScore {
  technical_score:   Int(min: 0, max: 100)
  price_score:       Int(min: 0, max: 100)
  reliability_score: Int(min: 0, max: 100)
  total_score:       Int(min: 0, max: 300)
}

type CostBreakdown {
  commodity_cost: Money(currency: "USD")
  delivery_cost:  Money(currency: "USD")
  risk_premium:   Money(currency: "USD")
}

type BidRecord {
  supplier_id:   Text(max_length: 64)
  bid_amount:    Money(currency: "USD")
  scores:        SupplierScore
  cost_detail:   CostBreakdown
  compliant:     Bool
}

rfp_workflow.tenor

// Energy Procurement RFP Workflow Contract
// Models a realistic Request for Proposal lifecycle for energy commodity procurement.
// Covers: RFP issuance, supplier bid evaluation, approval tiers by spend amount,
// delegation rules, supplier scoring, contract award, and purchase order generation.
//
// Key spec features exercised:
//   - Money types with comparisons (rfp_amount, bid_total, approval thresholds)
//   - Date types (rfp_deadline)
//   - Approval tiers via BranchStep (spend-amount routing)
//   - Escalate handler (escalate to VP for high-value denials)
//   - Multi-entity effects (RFP + PurchaseOrder on award)
//   - Bounded universal quantification (forall bid in supplier_bids)
//   - Multi-file import (types.tenor)

import "types.tenor"

// ── Personas ─────────────────────────────────────────────────────────────────

persona procurement_manager
persona category_lead
persona vp_supply_chain
persona cfo
persona supplier

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

fact rfp_amount {
  type:   Money(currency: "USD")
  source: "procurement_service.rfp_total_value"
}

fact bid_total {
  type:   Money(currency: "USD")
  source: "bid_service.winning_bid_amount"
}

fact rfp_deadline {
  type:   Date
  source: "procurement_service.submission_deadline"
}

fact current_date {
  type:   Date
  source: "system.current_date"
}

fact procurement_stage {
  type:   Enum(values: ["draft", "published", "evaluation", "awarded", "contracted"])
  source: "procurement_service.stage"
}

fact supplier_bids {
  type:   List(element_type: BidRecord, max: 50)
  source: "bid_service.all_bids"
}

fact winning_bid {
  type:   SupplierScore
  source: "bid_service.winning_supplier_scores"
}

fact budget_approved {
  type:    Bool
  source:  "finance_service.budget_available"
  default: false
}

fact compliance_checked {
  type:    Bool
  source:  "compliance_service.regulatory_check_passed"
  default: false
}

fact minimum_score_threshold {
  type:    Int(min: 0, max: 300)
  source:  "procurement_service.min_score"
  default: 180
}

fact bid_count {
  type:    Int(min: 0, max: 50)
  source:  "bid_service.total_bids"
  default: 0
}

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

entity RFP {
  states:  [draft, published, evaluation, shortlisted, awarded, contracted, cancelled]
  initial: draft
  transitions: [
    (draft, published),
    (draft, cancelled),
    (published, evaluation),
    (published, cancelled),
    (evaluation, shortlisted),
    (evaluation, cancelled),
    (shortlisted, awarded),
    (shortlisted, cancelled),
    (awarded, contracted),
    (awarded, cancelled)
  ]
}

entity PurchaseOrder {
  states:  [pending, approved, issued, fulfilled]
  initial: pending
  transitions: [
    (pending, approved),
    (approved, issued),
    (issued, fulfilled)
  ]
}

// ── Rules — Stratum 0 (Fact-level checks) ────────────────────────────────────

rule budget_available {
  stratum: 0
  when:    budget_approved = true
  produce: verdict budget_ok { payload: Bool = true }
}

rule compliance_verified {
  stratum: 0
  when:    compliance_checked = true
  produce: verdict compliance_ok { payload: Bool = true }
}

rule deadline_not_passed {
  stratum: 0
  when:    current_date <= rfp_deadline
  produce: verdict deadline_ok { payload: Bool = true }
}

rule all_bids_compliant {
  stratum: 0
  when:    ∀ bid ∈ supplier_bids . bid.compliant = true
  produce: verdict bids_compliant { payload: Bool = true }
}

rule sufficient_bids {
  stratum: 0
  when:    bid_count >= 2
  produce: verdict enough_bids { payload: Bool = true }
}

rule winning_score_above_threshold {
  stratum: 0
  when:    winning_bid.total_score >= minimum_score_threshold
  produce: verdict score_ok { payload: Bool = true }
}

// ── Rules — Stratum 1 (Approval tier determination) ──────────────────────────

rule tier_1_procurement_manager {
  stratum: 1
  when:    rfp_amount <= Money { amount: "50000.00", currency: "USD" }
         ∧ verdict_present(budget_ok)
  produce: verdict pm_can_approve { payload: Bool = true }
}

rule tier_2_category_lead {
  stratum: 1
  when:    rfp_amount > Money { amount: "50000.00", currency: "USD" }
         ∧ rfp_amount <= Money { amount: "500000.00", currency: "USD" }
         ∧ verdict_present(budget_ok)
  produce: verdict cl_approval_required { payload: Bool = true }
}

rule tier_3_vp_required {
  stratum: 1
  when:    rfp_amount > Money { amount: "500000.00", currency: "USD" }
         ∧ rfp_amount <= Money { amount: "2000000.00", currency: "USD" }
         ∧ verdict_present(budget_ok)
  produce: verdict vp_approval_required { payload: Bool = true }
}

rule tier_4_cfo_required {
  stratum: 1
  when:    rfp_amount > Money { amount: "2000000.00", currency: "USD" }
         ∧ verdict_present(budget_ok)
  produce: verdict cfo_approval_required { payload: Bool = true }
}

// ── Rules — Stratum 2 (Award recommendation) ─────────────────────────────────

rule award_recommended {
  stratum: 2
  when:    verdict_present(compliance_ok)
         ∧ verdict_present(score_ok)
         ∧ verdict_present(enough_bids)
         ∧ verdict_present(bids_compliant)
         ∧ (verdict_present(pm_can_approve) ∨ verdict_present(cl_approval_required)
            ∨ verdict_present(vp_approval_required) ∨ verdict_present(cfo_approval_required))
  produce: verdict award_ready { payload: Bool = true }
}

rule award_blocked {
  stratum: 2
  when:    ¬verdict_present(budget_ok)
         ∨ ¬verdict_present(compliance_ok)
  produce: verdict award_blocked { payload: Text = "missing budget or compliance" }
}

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

operation publish_rfp {
  allowed_personas: [procurement_manager]
  precondition:     verdict_present(deadline_ok)
  effects:          [(RFP, draft, published)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation evaluate_bids {
  allowed_personas: [procurement_manager, category_lead]
  precondition:     verdict_present(enough_bids)
  effects:          [(RFP, published, evaluation)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation shortlist_suppliers {
  allowed_personas: [procurement_manager, category_lead]
  precondition:     verdict_present(bids_compliant)
                  ∧ verdict_present(score_ok)
  effects:          [(RFP, evaluation, shortlisted)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation award_rfp {
  allowed_personas: [procurement_manager, category_lead, vp_supply_chain, cfo]
  precondition:     verdict_present(award_ready)
  effects:          [(RFP, shortlisted, awarded), (PurchaseOrder, pending, approved)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation reject_rfp {
  allowed_personas: [procurement_manager, category_lead, vp_supply_chain]
  precondition:     verdict_present(award_blocked)
  effects:          [(RFP, shortlisted, cancelled)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation approve_purchase {
  allowed_personas: [vp_supply_chain, cfo]
  precondition:     verdict_present(award_ready)
  effects:          [(PurchaseOrder, approved, issued)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation cancel_rfp {
  allowed_personas: [procurement_manager, category_lead, vp_supply_chain]
  precondition:     verdict_present(budget_ok) ∨ ¬verdict_present(budget_ok)
  effects:          [(RFP, draft, cancelled)]
  error_contract:   [precondition_failed, persona_rejected]
}

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

flow rfp_approval_flow {
  snapshot: at_initiation
  entry:    step_publish

  steps: {
    step_publish: OperationStep {
      op:      publish_rfp
      persona: procurement_manager
      outcomes: {
        success: step_evaluate
      }
      on_failure: Terminate(outcome: publish_failed)
    }

    step_evaluate: OperationStep {
      op:      evaluate_bids
      persona: procurement_manager
      outcomes: {
        success: step_shortlist
      }
      on_failure: Terminate(outcome: evaluation_failed)
    }

    step_shortlist: OperationStep {
      op:      shortlist_suppliers
      persona: procurement_manager
      outcomes: {
        success: step_check_tier
      }
      on_failure: Terminate(outcome: shortlist_failed)
    }

    step_check_tier: BranchStep {
      condition: verdict_present(pm_can_approve)
      persona:   procurement_manager
      if_true:   step_award_direct
      if_false:  step_check_high_value
    }

    step_award_direct: OperationStep {
      op:      award_rfp
      persona: procurement_manager
      outcomes: {
        success: Terminal(awarded)
      }
      on_failure: Terminate(outcome: award_failed)
    }

    step_check_high_value: BranchStep {
      condition: verdict_present(vp_approval_required) ∨ verdict_present(cfo_approval_required)
      persona:   category_lead
      if_true:   step_escalate_to_vp
      if_false:  step_award_category_lead
    }

    step_award_category_lead: OperationStep {
      op:      award_rfp
      persona: category_lead
      outcomes: {
        success: Terminal(awarded)
      }
      on_failure: Escalate(
        to:   vp_supply_chain
        next: step_escalate_to_vp
      )
    }

    step_escalate_to_vp: OperationStep {
      op:      award_rfp
      persona: vp_supply_chain
      outcomes: {
        success: Terminal(awarded)
      }
      on_failure: Terminate(outcome: escalation_failed)
    }
  }
}

Static Analysis Output

$ tenor check rfp_workflow.tenor

  Elaborating rfp_workflow.tenor ...
  Importing types.tenor ...

  ── Types ──────────────────────────────────────────────────────────
  SupplierScore  (types.tenor)            4 fields    ok
  CostBreakdown  (types.tenor)            3 fields    ok
  BidRecord      (types.tenor)            5 fields    ok

  ── Facts ──────────────────────────────────────────────────────────
  rfp_amount               Money(USD)                  ok
  bid_total                Money(USD)                  ok
  rfp_deadline             Date                        ok
  current_date             Date                        ok
  procurement_stage        Enum(5)                     ok
  supplier_bids            List(BidRecord, 50)         ok
  winning_bid              SupplierScore               ok
  budget_approved          Bool           default      ok
  compliance_checked       Bool           default      ok
  minimum_score_threshold  Int(0..300)    default      ok
  bid_count                Int(0..50)     default      ok

  ── Entities ───────────────────────────────────────────────────────
  RFP                      7 states  10 transitions    ok
  PurchaseOrder            4 states   3 transitions    ok

  ── Rules ──────────────────────────────────────────────────────────
  Stratum 0:
    budget_available               → budget_ok             ok
    compliance_verified            → compliance_ok         ok
    deadline_not_passed            → deadline_ok           ok
    all_bids_compliant             → bids_compliant        ok
    sufficient_bids                → enough_bids           ok
    winning_score_above_threshold  → score_ok              ok
  Stratum 1:
    tier_1_procurement_manager     → pm_can_approve        ok
    tier_2_category_lead           → cl_approval_required  ok
    tier_3_vp_required             → vp_approval_required  ok
    tier_4_cfo_required            → cfo_approval_required ok
  Stratum 2:
    award_recommended              → award_ready           ok
    award_blocked                  → award_blocked         ok

  ── Operations ─────────────────────────────────────────────────────
  publish_rfp           [procurement_manager]             ok
  evaluate_bids         [procurement_mgr, category_lead]  ok
  shortlist_suppliers   [procurement_mgr, category_lead]  ok
  award_rfp             [pm, cl, vp, cfo]                 ok
  reject_rfp            [pm, cl, vp]                      ok
  approve_purchase      [vp, cfo]                         ok
  cancel_rfp            [pm, cl, vp]                      ok

  ── Flows ──────────────────────────────────────────────────────────
  rfp_approval_flow     8 steps   3 terminals              ok

  ── S-Properties ───────────────────────────────────────────────────
  S1  Determinism         All rules produce deterministic verdicts   PASS
  S2  Stratification      3 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

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

Authority Topology

  procurement_manager ──┬── publish_rfp ───────────→ RFP
                        ├── evaluate_bids ─────────→ RFP
                        ├── shortlist_suppliers ────→ RFP
                        ├── award_rfp ─────────────→ RFP, PurchaseOrder
                        ├── reject_rfp ────────────→ RFP
                        └── cancel_rfp ────────────→ RFP

  category_lead ────────┬── evaluate_bids ─────────→ RFP
                        ├── shortlist_suppliers ────→ RFP
                        ├── award_rfp ─────────────→ RFP, PurchaseOrder
                        ├── reject_rfp ────────────→ RFP
                        └── cancel_rfp ────────────→ RFP

  vp_supply_chain ──────┬── award_rfp ─────────────→ RFP, PurchaseOrder
                        ├── reject_rfp ────────────→ RFP
                        ├── approve_purchase ──────→ PurchaseOrder
                        └── cancel_rfp ────────────→ RFP

  cfo ──────────────────┬── award_rfp ─────────────→ RFP, PurchaseOrder
                        └── approve_purchase ──────→ PurchaseOrder

Authority increases with seniority. The procurement manager has the broadest operational authority (publish, evaluate, shortlist) but the most limited approval authority (tier 1 only). The CFO has the narrowest operational authority but the highest approval ceiling.

Flow Path Enumeration

rfp_approval_flow

Path	Steps	Outcome
Tier 1 direct award	publish -> evaluate -> shortlist -> check_tier[true] -> award_direct	Terminal(awarded)
Tier 2 category lead award	publish -> evaluate -> shortlist -> check_tier[false] -> check_high_value[false] -> award_category_lead	Terminal(awarded)
Tier 2 escalation to VP	publish -> evaluate -> shortlist -> check_tier[false] -> check_high_value[false] -> award_category_lead[escalate] -> escalate_to_vp	Terminal(awarded)
Tier 3/4 VP award	publish -> evaluate -> shortlist -> check_tier[false] -> check_high_value[true] -> escalate_to_vp	Terminal(awarded)
Publish failed	publish[fail]	Terminate(publish_failed)
Evaluation failed	publish -> evaluate[fail]	Terminate(evaluation_failed)
Shortlist failed	publish -> evaluate -> shortlist[fail]	Terminate(shortlist_failed)
Escalation failed	... -> escalate_to_vp[fail]	Terminate(escalation_failed)

Sample Fact Set

A $35,000 RFP (tier 1 -- procurement manager can approve directly), two compliant bids, winning bid scores 265/300:

{
  "rfp_amount": {"amount": "35000.00", "currency": "USD"},
  "bid_total": {"amount": "32500.00", "currency": "USD"},
  "rfp_deadline": "2026-06-30",
  "current_date": "2026-03-15",
  "procurement_stage": "draft",
  "supplier_bids": [
    {
      "supplier_id": "ACME-ENERGY",
      "bid_amount": {"amount": "32500.00", "currency": "USD"},
      "scores": {
        "technical_score": 88,
        "price_score": 92,
        "reliability_score": 85,
        "total_score": 265
      },
      "cost_detail": {
        "commodity_cost": {"amount": "28000.00", "currency": "USD"},
        "delivery_cost": {"amount": "3000.00", "currency": "USD"},
        "risk_premium": {"amount": "1500.00", "currency": "USD"}
      },
      "compliant": true
    },
    {
      "supplier_id": "GLOBAL-POWER",
      "bid_amount": {"amount": "37200.00", "currency": "USD"},
      "scores": {
        "technical_score": 82,
        "price_score": 78,
        "reliability_score": 90,
        "total_score": 250
      },
      "cost_detail": {
        "commodity_cost": {"amount": "31000.00", "currency": "USD"},
        "delivery_cost": {"amount": "4200.00", "currency": "USD"},
        "risk_premium": {"amount": "2000.00", "currency": "USD"}
      },
      "compliant": true
    }
  ],
  "winning_bid": {
    "technical_score": 88,
    "price_score": 92,
    "reliability_score": 85,
    "total_score": 265
  },
  "budget_approved": true,
  "compliance_checked": true,
  "minimum_score_threshold": 180,
  "bid_count": 2
}

Sample Evaluation Output

$ tenor eval rfp_workflow.tenor --facts rfp_approve.facts.json

  Evaluating with 11 facts ...

  ── Stratum 0 ──────────────────────────────────────────────────────
  ✓ budget_available               → budget_ok             = true
    provenance: [budget_approved]
  ✓ compliance_verified            → compliance_ok         = true
    provenance: [compliance_checked]
  ✓ deadline_not_passed            → deadline_ok           = true
    provenance: [current_date, rfp_deadline]
  ✓ all_bids_compliant             → bids_compliant        = true
    provenance: [supplier_bids]
  ✓ sufficient_bids                → enough_bids           = true
    provenance: [bid_count]
  ✓ winning_score_above_threshold  → score_ok              = true
    provenance: [winning_bid, minimum_score_threshold]

  ── Stratum 1 ──────────────────────────────────────────────────────
  ✓ tier_1_procurement_manager     → pm_can_approve        = true
    provenance: [rfp_amount, budget_ok]
  · tier_2_category_lead           — not satisfied ($35K ≤ $50K)
  · tier_3_vp_required             — not satisfied ($35K ≤ $50K)
  · tier_4_cfo_required            — not satisfied ($35K ≤ $2M)

  ── Stratum 2 ──────────────────────────────────────────────────────
  ✓ award_recommended              → award_ready           = true
    provenance: [compliance_ok, score_ok, enough_bids, bids_compliant, pm_can_approve]
  · award_blocked                  — not satisfied (budget and compliance ok)

  ── Flow: rfp_approval_flow ────────────────────────────────────────
  step_publish       → success (publish_rfp as procurement_manager)
  step_evaluate      → success (evaluate_bids as procurement_manager)
  step_shortlist     → success (shortlist_suppliers as procurement_manager)
  step_check_tier    → true    (pm_can_approve present)
  step_award_direct  → success (award_rfp as procurement_manager)
  Flow outcome: awarded

  ── Entity States ──────────────────────────────────────────────────
  RFP:           draft → published → evaluation → shortlisted → awarded
  PurchaseOrder: pending → approved

  8 verdicts produced, 5 entity transitions, flow outcome: awarded

Formal Properties and Patterns

Tier-based approval routing: Four mutually exclusive Money-range rules determine which persona can approve. The BranchStep chain routes to the appropriate approval step. This is a generalizable pattern for any dollar-amount-gated approval process.

Escalate handler for authority escalation: When the category lead's award operation fails, the Escalate handler transfers control to the VP. This models the real-world pattern where a mid-level manager's decision can be overridden by their superior.

Money type comparisons: The tier rules compare rfp_amount against literal Money values like Money { amount: "50000.00", currency: "USD" }. Tenor ensures currency-safe comparisons -- you cannot accidentally compare USD against EUR.

Multi-entity effects: The award_rfp operation transitions both RFP (shortlisted -> awarded) and PurchaseOrder (pending -> approved) atomically. The award and PO creation are a single operation, ensuring they cannot diverge.

Tautological precondition: The cancel_rfp operation has the precondition verdict_present(budget_ok) OR NOT verdict_present(budget_ok), which is always true. This is intentional: cancellation should always be possible regardless of budget status. Tenor's elaborator accepts tautological preconditions.

Three-stratum verdict chain: Facts -> tier determination -> award recommendation. Each stratum provides a complete set of inputs to the next. The stratum 2 award_recommended rule requires both compliance verdicts (from stratum 0/1) and a tier determination (from stratum 1), ensuring all prerequisites are checked.