The healthcare prior authorization contract is the most complex domain contract in the Tenor suite. It models the full prior authorization lifecycle from physician submission through clinical review, peer review escalation, medical director override, denial with appeal rights, and appeals board adjudication. It uses 6 personas, 4 rule strata, 2 entities, SubFlowStep, HandoffStep, and Escalate handlers.

This is the "wow" contract -- the one that demonstrates Tenor can express genuinely complex, real-world business logic that would otherwise be buried in hundreds of if-else branches across dozens of microservices.

Business Domain

In the US healthcare system, many treatments require prior authorization from the patient's insurance payer before the treatment can proceed. The process involves:

1. The requesting physician submits an authorization request with diagnosis codes, treatment codes, and supporting medical records
2. The system triages by urgency (emergent cases get fast-tracked)
3. A clinical reviewer evaluates medical necessity against policy criteria
4. If criteria are not met, the case may escalate to a peer reviewer or medical director
5. Denial triggers appeal rights with a deadline
6. An appeals board reviews the denial and may overturn it based on merit or new evidence

Every step must be auditable, every decision must cite specific criteria, and authority must be clearly delineated between clinical reviewers, peer reviewers, medical directors, and appeals boards.

Why This Domain

Healthcare prior authorization is a natural showcase for Tenor because it involves:

• Deep flow nesting (SubFlowStep for the appeal sub-process)
• Authority escalation (Escalate handler from clinical reviewer to medical director)
• Authority handoff (HandoffStep from physician to appeals board)
• Four strata of rules building up from raw clinical checks to final authorization decisions
• Multi-entity effects (PriorAuth and AppealCase transition simultaneously)
• Mutually exclusive paths based on clinical criteria and urgency

Contract Structure

Entities

Entity	States	Initial	Transitions
PriorAuth	submitted, under_review, approved, denied, appealed, appeal_approved, appeal_denied	submitted	submitted->under_review, under_review->approved, under_review->denied, denied->appealed, appealed->appeal_approved, appealed->appeal_denied
AppealCase	filed, review, decided	filed	filed->review, review->decided

The PriorAuth entity has 7 states modeling the full lifecycle. The AppealCase entity is created only when a denial is appealed and tracks the appeal sub-process independently.

Personas

Persona	Authority
requesting_physician	Submits auth requests, files appeals
clinical_reviewer	Approves/denies auth, escalates to peer review
peer_reviewer	Reviews escalated cases
medical_director	Final approval/denial authority, can overturn on appeal
appeals_board	Reviews appeals, overturns or upholds denials
patient_advocate	Can file appeals on behalf of patients

Facts and Sources

Fact	Type	Source	Default
auth_status	Enum(7 values)	auth_service.current_status	--
medical_records	List(MedicalRecord, max: 50)	ehr_service.patient_records	--
policy_criteria	PolicyCriteria	policy_engine.criteria_evaluation	--
diagnosis_code	Text(max: 16)	clinical_service.icd10_code	--
treatment_code	Text(max: 16)	clinical_service.cpt_code	--
urgency_level	Enum: routine, urgent, emergent	clinical_service.urgency	--
clinical_criteria_met	Bool	review_service.criteria_met	false
appeal_deadline	Date	auth_service.appeal_deadline	--
denial_reason	Enum(4 values)	auth_service.denial_reason	--
peer_review_requested	Bool	review_service.peer_review_flag	false
appeal_filed	Bool	appeals_service.appeal_filed	false
appeal_merit_score	Int(0..100)	appeals_service.merit_score	--
new_evidence_submitted	Bool	appeals_service.new_evidence	false

Named Types

type PolicyCriteria {
  diagnosis_covered:           Bool
  treatment_in_formulary:      Bool
  provider_in_network:         Bool
  step_therapy_completed:      Bool
  prior_treatments_documented: Bool
}

type ReviewRecord {
  reviewer_id:   Text(max_length: 128)
  decision:      Text(max_length: 64)
  clinical_note: Text(max_length: 2048)
  review_date:   Date
}

type MedicalRecord {
  record_id:     Text(max_length: 64)
  record_type:   Text(max_length: 128)
  is_relevant:   Bool
  is_complete:   Bool
}

Verdict Chain

This contract uses 4 strata -- the deepest verdict chain of any domain contract.

Stratum 0 -- Clinical Criteria Checks

Direct checks against facts and medical records:

Rule	Condition	Verdict
all_records_complete	forall record in medical_records . record.is_complete = true	records_complete
all_records_relevant	forall record in medical_records . record.is_relevant = true	records_relevant
diagnosis_covered	policy_criteria.diagnosis_covered = true	diagnosis_is_covered
treatment_in_formulary	policy_criteria.treatment_in_formulary = true	treatment_is_formulary
provider_network_check	policy_criteria.provider_in_network = true	provider_in_network
step_therapy_check	policy_criteria.step_therapy_completed = true	step_therapy_done
clinical_criteria_check	clinical_criteria_met = true	clinical_criteria_passed
is_emergent	urgency_level = "emergent"	emergent_case
is_urgent	urgency_level = "urgent"	urgent_case

Stratum 1 -- Eligibility Determination

Composes stratum 0 verdicts into higher-level eligibility checks:

Rule	Dependencies	Verdict
documentation_sufficient	records_complete AND records_relevant	documentation_ok
policy_criteria_satisfied	diagnosis_is_covered AND treatment_is_formulary AND provider_in_network AND step_therapy_done	policy_satisfied
emergent_fast_track	emergent_case AND records_complete AND records_relevant	fast_track_eligible

Stratum 2 -- Authorization Decision

The final authorization verdicts:

Rule	Dependencies	Verdict
can_approve	documentation_ok AND policy_satisfied AND clinical_criteria_passed	authorization_approved
should_deny	documentation_ok AND NOT clinical_criteria_passed	authorization_denied
appeal_has_merit	appeal_merit_score >= 50	appeal_meritorious
appeal_with_new_evidence	new_evidence_submitted = true	new_evidence_available

Note the denial rule: documentation must be sufficient (otherwise the submission should be returned, not denied), but clinical criteria must be absent. This prevents denial when records are incomplete.

Stratum 3 -- Appeal Outcome

The final stratum composes appeal verdicts:

Rule	Dependencies	Verdict
can_overturn_denial	appeal_meritorious OR new_evidence_available	overturn_recommended

The disjunction means either a strong merit score OR new evidence is sufficient to recommend overturning -- they don't both have to be present.

Flow Orchestration

auth_review_flow (Primary Flow)

The primary flow models the full authorization lifecycle with urgency triage, clinical review, escalation, and appeal:

1. step_submit (OperationStep) -- Physician submits authorization
2. step_urgency_triage (BranchStep) -- Routes on fast_track_eligible
   • If true: step_fast_track_approve -- Medical director approves directly
   • If false: continue to clinical review
3. step_clinical_review (BranchStep) -- Routes on authorization_approved
   • If true: step_approve -- Clinical reviewer approves
   • If false: step_deny -- Clinical reviewer denies
4. step_deny on_failure: Escalate to medical director
5. step_director_review (BranchStep) -- Medical director re-evaluates
   • If true: step_director_approve -- Director approves
   • If false: step_director_deny -- Director denies
6. step_appeal_subflow (SubFlowStep) -- Invokes appeal_flow

appeal_flow (Sub-Flow)

Invoked as a SubFlowStep from the main auth_review_flow:

1. step_file_appeal (OperationStep) -- Physician files appeal
2. step_handoff_to_board (HandoffStep) -- Authority transfers from physician to appeals board
3. step_review_merit (BranchStep) -- Routes on overturn_recommended
   • If true: step_overturn -- Appeals board overturns denial
   • If false: step_uphold -- Appeals board upholds denial

Complete Contract Source

// Healthcare Prior Authorization Contract
// Domain: Healthcare payer — prior authorization lifecycle from submission
// through clinical review, peer review escalation, denial with appeal rights,
// and appeal adjudication.
//
// This is the "wow" showcase contract demonstrating Tenor's ability to express
// genuinely complex, real-world business logic. Exercises the widest set of
// spec features: deep flows with SubFlowStep, Escalate handlers, multi-stratum
// rules, 6 personas, Record types, bounded quantification, and handoff steps.
//
// The prior auth lifecycle:
//   1. Requesting physician submits authorization request
//   2. System routes by urgency (emergent/urgent/routine)
//   3. Clinical reviewer evaluates medical necessity
//   4. If criteria not met, escalation to peer reviewer
//   5. Medical director makes final authorization decision
//   6. Denial triggers appeal rights with deadline
//   7. Appeals board reviews and may overturn denial

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

type PolicyCriteria {
  diagnosis_covered:           Bool
  treatment_in_formulary:      Bool
  provider_in_network:         Bool
  step_therapy_completed:      Bool
  prior_treatments_documented: Bool
}

type ReviewRecord {
  reviewer_id:   Text(max_length: 128)
  decision:      Text(max_length: 64)
  clinical_note: Text(max_length: 2048)
  review_date:   Date
}

type MedicalRecord {
  record_id:     Text(max_length: 64)
  record_type:   Text(max_length: 128)
  is_relevant:   Bool
  is_complete:   Bool
}

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

persona requesting_physician
persona clinical_reviewer
persona peer_reviewer
persona medical_director
persona appeals_board
persona patient_advocate

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

fact auth_status {
  type:   Enum(values: ["submitted", "under_review", "approved", "denied", "appealed", "appeal_approved", "appeal_denied"])
  source: "auth_service.current_status"
}

fact medical_records {
  type:   List(element_type: MedicalRecord, max: 50)
  source: "ehr_service.patient_records"
}

fact policy_criteria {
  type:   PolicyCriteria
  source: "policy_engine.criteria_evaluation"
}

fact diagnosis_code {
  type:   Text(max_length: 16)
  source: "clinical_service.icd10_code"
}

fact treatment_code {
  type:   Text(max_length: 16)
  source: "clinical_service.cpt_code"
}

fact urgency_level {
  type:   Enum(values: ["routine", "urgent", "emergent"])
  source: "clinical_service.urgency"
}

fact clinical_criteria_met {
  type:    Bool
  source:  "review_service.criteria_met"
  default: false
}

fact appeal_deadline {
  type:   Date
  source: "auth_service.appeal_deadline"
}

fact denial_reason {
  type:   Enum(values: ["medical_necessity", "experimental_treatment", "out_of_network", "documentation_insufficient"])
  source: "auth_service.denial_reason"
}

fact peer_review_requested {
  type:    Bool
  source:  "review_service.peer_review_flag"
  default: false
}

fact appeal_filed {
  type:    Bool
  source:  "appeals_service.appeal_filed"
  default: false
}

fact appeal_merit_score {
  type:   Int(min: 0, max: 100)
  source: "appeals_service.merit_score"
}

fact new_evidence_submitted {
  type:    Bool
  source:  "appeals_service.new_evidence"
  default: false
}

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

entity PriorAuth {
  states:  [submitted, under_review, approved, denied, appealed, appeal_approved, appeal_denied]
  initial: submitted
  transitions: [
    (submitted, under_review),
    (under_review, approved),
    (under_review, denied),
    (denied, appealed),
    (appealed, appeal_approved),
    (appealed, appeal_denied)
  ]
}

entity AppealCase {
  states:  [filed, review, decided]
  initial: filed
  transitions: [
    (filed, review),
    (review, decided)
  ]
}

// ── Rules — Stratum 0 (clinical criteria checks) ────────────────────────────

rule all_records_complete {
  stratum: 0
  when:    ∀ record ∈ medical_records . record.is_complete = true
  produce: verdict records_complete { payload: Bool = true }
}

rule all_records_relevant {
  stratum: 0
  when:    ∀ record ∈ medical_records . record.is_relevant = true
  produce: verdict records_relevant { payload: Bool = true }
}

rule diagnosis_covered {
  stratum: 0
  when:    policy_criteria.diagnosis_covered = true
  produce: verdict diagnosis_is_covered { payload: Bool = true }
}

rule treatment_in_formulary {
  stratum: 0
  when:    policy_criteria.treatment_in_formulary = true
  produce: verdict treatment_is_formulary { payload: Bool = true }
}

rule provider_network_check {
  stratum: 0
  when:    policy_criteria.provider_in_network = true
  produce: verdict provider_in_network { payload: Bool = true }
}

rule step_therapy_check {
  stratum: 0
  when:    policy_criteria.step_therapy_completed = true
  produce: verdict step_therapy_done { payload: Bool = true }
}

rule clinical_criteria_check {
  stratum: 0
  when:    clinical_criteria_met = true
  produce: verdict clinical_criteria_passed { payload: Bool = true }
}

rule is_emergent {
  stratum: 0
  when:    urgency_level = "emergent"
  produce: verdict emergent_case { payload: Bool = true }
}

rule is_urgent {
  stratum: 0
  when:    urgency_level = "urgent"
  produce: verdict urgent_case { payload: Bool = true }
}

// ── Rules — Stratum 1 (eligibility determination) ───────────────────────────

rule documentation_sufficient {
  stratum: 1
  when:    verdict_present(records_complete)
         ∧ verdict_present(records_relevant)
  produce: verdict documentation_ok { payload: Bool = true }
}

rule policy_criteria_satisfied {
  stratum: 1
  when:    verdict_present(diagnosis_is_covered)
         ∧ verdict_present(treatment_is_formulary)
         ∧ verdict_present(provider_in_network)
         ∧ verdict_present(step_therapy_done)
  produce: verdict policy_satisfied { payload: Bool = true }
}

rule emergent_fast_track {
  stratum: 1
  when:    verdict_present(emergent_case)
         ∧ verdict_present(records_complete)
         ∧ verdict_present(records_relevant)
  produce: verdict fast_track_eligible { payload: Bool = true }
}

// ── Rules — Stratum 2 (final authorization decision) ────────────────────────

rule can_approve {
  stratum: 2
  when:    verdict_present(documentation_ok)
         ∧ verdict_present(policy_satisfied)
         ∧ verdict_present(clinical_criteria_passed)
  produce: verdict authorization_approved { payload: Bool = true }
}

rule should_deny {
  stratum: 2
  when:    verdict_present(documentation_ok)
         ∧ ¬verdict_present(clinical_criteria_passed)
  produce: verdict authorization_denied { payload: Bool = true }
}

rule appeal_has_merit {
  stratum: 2
  when:    appeal_merit_score >= 50
  produce: verdict appeal_meritorious { payload: Bool = true }
}

rule appeal_with_new_evidence {
  stratum: 2
  when:    new_evidence_submitted = true
  produce: verdict new_evidence_available { payload: Bool = true }
}

// ── Rules — Stratum 3 (appeal outcome) ──────────────────────────────────────

rule can_overturn_denial {
  stratum: 3
  when:    verdict_present(appeal_meritorious)
         ∨ verdict_present(new_evidence_available)
  produce: verdict overturn_recommended { payload: Bool = true }
}

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

operation submit_auth {
  allowed_personas: [requesting_physician]
  precondition:     verdict_present(documentation_ok)
  effects:          [(PriorAuth, submitted, under_review)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation approve_auth {
  allowed_personas: [clinical_reviewer, medical_director]
  precondition:     verdict_present(authorization_approved)
  effects:          [(PriorAuth, under_review, approved)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation deny_auth {
  allowed_personas: [clinical_reviewer, medical_director]
  precondition:     verdict_present(authorization_denied)
  effects:          [(PriorAuth, under_review, denied)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation file_appeal {
  allowed_personas: [requesting_physician, patient_advocate]
  precondition:     appeal_filed = true
  effects:          [(PriorAuth, denied, appealed), (AppealCase, filed, review)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation review_appeal {
  allowed_personas: [appeals_board]
  precondition:     verdict_present(appeal_meritorious) ∨ verdict_present(new_evidence_available)
  effects:          [(AppealCase, review, decided)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation overturn_denial {
  allowed_personas: [appeals_board, medical_director]
  precondition:     verdict_present(overturn_recommended)
  effects:          [(PriorAuth, appealed, appeal_approved)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation uphold_denial {
  allowed_personas: [appeals_board]
  precondition:     ¬verdict_present(overturn_recommended)
  effects:          [(PriorAuth, appealed, appeal_denied)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation escalate_to_peer {
  allowed_personas: [clinical_reviewer]
  precondition:     peer_review_requested = true
  effects:          [(PriorAuth, under_review, denied)]
  error_contract:   [precondition_failed, persona_rejected]
}

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

flow auth_review_flow {
  snapshot: at_initiation
  entry:    step_submit

  steps: {
    step_submit: OperationStep {
      op:      submit_auth
      persona: requesting_physician
      outcomes: {
        success: step_urgency_triage
      }
      on_failure: Terminate(outcome: submission_failed)
    }

    step_urgency_triage: BranchStep {
      condition: verdict_present(fast_track_eligible)
      persona:   clinical_reviewer
      if_true:   step_fast_track_approve
      if_false:  step_clinical_review
    }

    step_fast_track_approve: OperationStep {
      op:      approve_auth
      persona: medical_director
      outcomes: {
        success: Terminal(approved_fast_track)
      }
      on_failure: Terminate(outcome: fast_track_failed)
    }

    step_clinical_review: BranchStep {
      condition: verdict_present(authorization_approved)
      persona:   clinical_reviewer
      if_true:   step_approve
      if_false:  step_deny
    }

    step_approve: OperationStep {
      op:      approve_auth
      persona: clinical_reviewer
      outcomes: {
        success: Terminal(approved)
      }
      on_failure: Terminate(outcome: approval_processing_failed)
    }

    step_deny: OperationStep {
      op:      deny_auth
      persona: clinical_reviewer
      outcomes: {
        success: step_appeal_subflow
      }
      on_failure: Escalate(
        to: medical_director
        next: step_director_review
      )
    }

    step_director_review: BranchStep {
      condition: verdict_present(authorization_approved)
      persona:   medical_director
      if_true:   step_director_approve
      if_false:  step_director_deny
    }

    step_director_approve: OperationStep {
      op:      approve_auth
      persona: medical_director
      outcomes: {
        success: Terminal(approved_by_director)
      }
      on_failure: Terminate(outcome: director_approval_failed)
    }

    step_director_deny: OperationStep {
      op:      deny_auth
      persona: medical_director
      outcomes: {
        success: step_appeal_subflow
      }
      on_failure: Terminate(outcome: director_denial_failed)
    }

    step_appeal_subflow: SubFlowStep {
      flow:       appeal_flow
      persona:    requesting_physician
      on_success: Terminal(appeal_resolved)
      on_failure: Terminate(outcome: appeal_process_failed)
    }
  }
}

flow appeal_flow {
  snapshot: at_initiation
  entry:    step_file_appeal

  steps: {
    step_file_appeal: OperationStep {
      op:      file_appeal
      persona: requesting_physician
      outcomes: {
        success: step_handoff_to_board
      }
      on_failure: Terminate(outcome: appeal_filing_failed)
    }

    step_handoff_to_board: HandoffStep {
      from_persona: requesting_physician
      to_persona:   appeals_board
      next:         step_review_merit
    }

    step_review_merit: BranchStep {
      condition: verdict_present(overturn_recommended)
      persona:   appeals_board
      if_true:   step_overturn
      if_false:  step_uphold
    }

    step_overturn: OperationStep {
      op:      overturn_denial
      persona: appeals_board
      outcomes: {
        success: Terminal(appeal_granted)
      }
      on_failure: Terminate(outcome: overturn_failed)
    }

    step_uphold: OperationStep {
      op:      uphold_denial
      persona: appeals_board
      outcomes: {
        success: Terminal(appeal_denied)
      }
      on_failure: Terminate(outcome: uphold_failed)
    }
  }
}

Static Analysis Output

$ tenor check prior_auth.tenor

  Elaborating prior_auth.tenor ...

  ── Types ──────────────────────────────────────────────────────────
  PolicyCriteria                          5 fields    ok
  ReviewRecord                            4 fields    ok
  MedicalRecord                           4 fields    ok

  ── Facts ──────────────────────────────────────────────────────────
  auth_status              Enum(7)                     ok
  medical_records          List(MedicalRecord, 50)     ok
  policy_criteria          PolicyCriteria              ok
  diagnosis_code           Text(16)                    ok
  treatment_code           Text(16)                    ok
  urgency_level            Enum(3)                     ok
  clinical_criteria_met    Bool           default      ok
  appeal_deadline          Date                        ok
  denial_reason            Enum(4)                     ok
  peer_review_requested    Bool           default      ok
  appeal_filed             Bool           default      ok
  appeal_merit_score       Int(0..100)                 ok
  new_evidence_submitted   Bool           default      ok

  ── Entities ───────────────────────────────────────────────────────
  PriorAuth                7 states   6 transitions    ok
  AppealCase               3 states   2 transitions    ok

  ── Rules ──────────────────────────────────────────────────────────
  Stratum 0:
    all_records_complete       → records_complete          ok
    all_records_relevant       → records_relevant          ok
    diagnosis_covered          → diagnosis_is_covered      ok
    treatment_in_formulary     → treatment_is_formulary    ok
    provider_network_check     → provider_in_network       ok
    step_therapy_check         → step_therapy_done         ok
    clinical_criteria_check    → clinical_criteria_passed  ok
    is_emergent                → emergent_case             ok
    is_urgent                  → urgent_case               ok
  Stratum 1:
    documentation_sufficient   → documentation_ok          ok
    policy_criteria_satisfied  → policy_satisfied          ok
    emergent_fast_track        → fast_track_eligible       ok
  Stratum 2:
    can_approve                → authorization_approved    ok
    should_deny                → authorization_denied      ok
    appeal_has_merit           → appeal_meritorious        ok
    appeal_with_new_evidence   → new_evidence_available    ok
  Stratum 3:
    can_overturn_denial        → overturn_recommended      ok

  ── Operations ─────────────────────────────────────────────────────
  submit_auth           [requesting_physician]            ok
  approve_auth          [clinical_reviewer, med_director] ok
  deny_auth             [clinical_reviewer, med_director] ok
  file_appeal           [req_physician, patient_advocate] ok
  review_appeal         [appeals_board]                   ok
  overturn_denial       [appeals_board, med_director]     ok
  uphold_denial         [appeals_board]                   ok
  escalate_to_peer      [clinical_reviewer]               ok

  ── Flows ──────────────────────────────────────────────────────────
  auth_review_flow      11 steps  5 terminals             ok
  appeal_flow            5 steps  2 terminals             ok

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

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

Authority Topology

  requesting_physician ──┬── submit_auth ────────→ PriorAuth
                         └── file_appeal ────────→ PriorAuth, AppealCase

  patient_advocate ──────── file_appeal ─────────→ PriorAuth, AppealCase

  clinical_reviewer ─────┬── approve_auth ───────→ PriorAuth
                         ├── deny_auth ──────────→ PriorAuth
                         └── escalate_to_peer ───→ PriorAuth

  medical_director ──────┬── approve_auth ───────→ PriorAuth
                         ├── deny_auth ──────────→ PriorAuth
                         └── overturn_denial ────→ PriorAuth

  appeals_board ─────────┬── review_appeal ──────→ AppealCase
                         ├── overturn_denial ────→ PriorAuth
                         └── uphold_denial ──────→ PriorAuth

Authority flows in one direction: physicians submit and appeal, clinical reviewers evaluate (with escalation escape), the medical director has override authority, and the appeals board has final adjudication power.

Flow Path Enumeration

auth_review_flow

Path	Steps	Outcome
Emergent fast-track	step_submit -> step_urgency_triage[true] -> step_fast_track_approve	Terminal(approved_fast_track)
Routine approval	step_submit -> step_urgency_triage[false] -> step_clinical_review[true] -> step_approve	Terminal(approved)
Denial -> appeal -> overturn	step_submit -> ... -> step_deny -> step_appeal_subflow -> appeal_flow(overturn)	Terminal(appeal_resolved)
Denial -> appeal -> uphold	step_submit -> ... -> step_deny -> step_appeal_subflow -> appeal_flow(uphold)	Terminal(appeal_resolved)
Denial escalation -> director approve	step_submit -> ... -> step_deny[escalate] -> step_director_review[true] -> step_director_approve	Terminal(approved_by_director)
Denial escalation -> director deny -> appeal	step_submit -> ... -> step_deny[escalate] -> step_director_review[false] -> step_director_deny -> step_appeal_subflow	Terminal(appeal_resolved)
Submission failure	step_submit[fail]	Terminate(submission_failed)

appeal_flow

Path	Steps	Outcome
Appeal granted	step_file_appeal -> step_handoff_to_board -> step_review_merit[true] -> step_overturn	Terminal(appeal_granted)
Appeal denied	step_file_appeal -> step_handoff_to_board -> step_review_merit[false] -> step_uphold	Terminal(appeal_denied)
Filing failure	step_file_appeal[fail]	Terminate(appeal_filing_failed)

Sample Fact Sets

Approval Path (Routine, All Criteria Met)

{
  "auth_status": "submitted",
  "medical_records": [
    {"record_id": "MR-001", "record_type": "Lab Results", "is_relevant": true, "is_complete": true},
    {"record_id": "MR-002", "record_type": "Imaging", "is_relevant": true, "is_complete": true},
    {"record_id": "MR-003", "record_type": "Clinical Notes", "is_relevant": true, "is_complete": true}
  ],
  "policy_criteria": {
    "diagnosis_covered": true,
    "treatment_in_formulary": true,
    "provider_in_network": true,
    "step_therapy_completed": true,
    "prior_treatments_documented": true
  },
  "diagnosis_code": "M54.5",
  "treatment_code": "97140",
  "urgency_level": "routine",
  "clinical_criteria_met": true,
  "appeal_deadline": "2026-06-15",
  "denial_reason": "medical_necessity",
  "peer_review_requested": false,
  "appeal_filed": false,
  "appeal_merit_score": 0,
  "new_evidence_submitted": false
}

Denial Path (Clinical Criteria Not Met)

{
  "auth_status": "submitted",
  "medical_records": [
    {"record_id": "MR-001", "record_type": "Lab Results", "is_relevant": true, "is_complete": true},
    {"record_id": "MR-002", "record_type": "Imaging", "is_relevant": true, "is_complete": true}
  ],
  "policy_criteria": {
    "diagnosis_covered": true,
    "treatment_in_formulary": true,
    "provider_in_network": true,
    "step_therapy_completed": true,
    "prior_treatments_documented": true
  },
  "diagnosis_code": "Z96.1",
  "treatment_code": "27447",
  "urgency_level": "routine",
  "clinical_criteria_met": false,
  "appeal_deadline": "2026-07-15",
  "denial_reason": "medical_necessity",
  "peer_review_requested": false,
  "appeal_filed": false,
  "appeal_merit_score": 0,
  "new_evidence_submitted": false
}

Sample Evaluation Output

Approval Path

$ tenor eval prior_auth.tenor --facts prior_auth_approve.facts.json

  Evaluating with 13 facts ...

  ── Stratum 0 ──────────────────────────────────────────────────────
  ✓ all_records_complete       → records_complete          = true
    provenance: [medical_records]
  ✓ all_records_relevant       → records_relevant          = true
    provenance: [medical_records]
  ✓ diagnosis_covered          → diagnosis_is_covered      = true
    provenance: [policy_criteria]
  ✓ treatment_in_formulary     → treatment_is_formulary    = true
    provenance: [policy_criteria]
  ✓ provider_network_check     → provider_in_network       = true
    provenance: [policy_criteria]
  ✓ step_therapy_check         → step_therapy_done         = true
    provenance: [policy_criteria]
  ✓ clinical_criteria_check    → clinical_criteria_passed  = true
    provenance: [clinical_criteria_met]
  · is_emergent                — not satisfied (urgency ≠ "emergent")
  · is_urgent                  — not satisfied (urgency ≠ "urgent")

  ── Stratum 1 ──────────────────────────────────────────────────────
  ✓ documentation_sufficient   → documentation_ok          = true
    provenance: [records_complete, records_relevant]
  ✓ policy_criteria_satisfied  → policy_satisfied          = true
    provenance: [diagnosis_is_covered, treatment_is_formulary,
                 provider_in_network, step_therapy_done]
  · emergent_fast_track        — not satisfied (emergent_case absent)

  ── Stratum 2 ──────────────────────────────────────────────────────
  ✓ can_approve                → authorization_approved    = true
    provenance: [documentation_ok, policy_satisfied, clinical_criteria_passed]
  · should_deny                — not satisfied (clinical_criteria_passed present)
  · appeal_has_merit           — not satisfied (merit_score < 50)
  · appeal_with_new_evidence   — not satisfied (new_evidence = false)

  ── Stratum 3 ──────────────────────────────────────────────────────
  · can_overturn_denial        — not satisfied (no appeal verdicts)

  ── Flow: auth_review_flow ─────────────────────────────────────────
  step_submit            → success (submit_auth as requesting_physician)
  step_urgency_triage    → false   (fast_track_eligible absent)
  step_clinical_review   → true    (authorization_approved present)
  step_approve           → success (approve_auth as clinical_reviewer)
  Flow outcome: approved

  ── Entity States ──────────────────────────────────────────────────
  PriorAuth: submitted → under_review → approved

  10 verdicts produced, 2 entity transitions, flow outcome: approved

Formal Properties and Patterns

Deep stratification (4 strata): The verdict chain builds through 4 levels: raw clinical checks -> eligibility composites -> authorization decisions -> appeal outcomes. Each stratum sees a complete, stable set of inputs from all lower strata.

SubFlowStep for process composition: The appeal process is modeled as a separate flow invoked via SubFlowStep. This is not just syntactic sugar -- it means the appeal flow has its own snapshot semantics and can be independently verified for termination.

Escalate handler for authority escalation: When the clinical reviewer's denial operation fails (the clinical reviewer's denial is rejected), the Escalate handler transfers control to the medical director. This models the real-world pattern where a clinical reviewer's decision can be overridden.

HandoffStep for authority transfer: In the appeal flow, HandoffStep transfers authority from the requesting physician to the appeals board. This is a formal model of the real-world process where the physician files the appeal but the board adjudicates it.

Negated verdict preconditions: The uphold_denial operation requires NOT verdict_present(overturn_recommended). This is a safe pattern because the stratum 3 rule has already evaluated -- if overturn is not recommended, upholding the denial is the only valid action.

Multi-entity effects: The file_appeal operation transitions both PriorAuth (denied -> appealed) and AppealCase (filed -> review) in a single atomic operation, ensuring the two entities stay in sync.

Bounded quantification over medical records: Both all_records_complete and all_records_relevant use forall record in medical_records to ensure every submitted record meets the standard. A single incomplete or irrelevant record blocks the entire authorization.