This tutorial builds a working Tenor contract from an empty file to a complete behavioral specification. You will add constructs one at a time, running tenor check after each addition to watch the static analysis grow. By the end you will have a contract with personas, an entity, a source, facts, rules, operations, and a flow — and proof that it is correct.

Create the File

mkdir -p ~/tenor-tutorial && cd ~/tenor-tutorial
touch approval.tenor

Every Tenor contract lives in a single .tenor file. This one will model a document approval workflow: an admin submits documents for review, and an operator approves or rejects them based on verified criteria.

Step 1: Define Personas

Personas are named authority roles. They declare who can act within the contract. Start with two:

persona admin
persona operator

That is the entire declaration. Personas are intentionally simple — their power comes from how operations reference them.

Run the checker:

tenor check approval.tenor

$ tenor check approval.tenor

✓ Elaboration: 6 passes, 0 errors

  Static Analysis
  ─────────────────────────────────────────────────────
  S1  State Space       0 entities, 0 states total
  S2  Reachability      no entities to check
  S3  Admissibility     0 operations
  S4  Authority         2 personas, 0 authority entries
  S5  Verdicts          0 verdict types from 0 rules
  S6  Flow Paths        0 flows
  S7  Complexity        max predicate depth 0, max flow depth 0
  S8  Verdict Unique    no verdicts to check

  ✓ All 8 properties verified in 1ms

Two personas, zero authority entries. Nobody can do anything yet.

Step 2: Add an Entity

An entity is a finite state machine — a thing in your domain that moves through declared states. Add a document entity with three states:

persona admin
persona operator

entity Document {
  states:  [draft, approved, rejected]
  initial: draft
  transitions: [
    (draft, approved),
    (draft, rejected)
  ]
}

The Document starts in draft and can move to approved or rejected. No other transitions are possible — the elaborator enforces this structurally.

tenor check approval.tenor

$ tenor check approval.tenor

✓ Elaboration: 6 passes, 0 errors

  Static Analysis
  ─────────────────────────────────────────────────────
  S1  State Space       1 entity, 3 states total
  S2  Reachability      3/3 states reachable, 0 dead states
  S3  Admissibility     0 operations
  S4  Authority         2 personas, 0 authority entries
  S5  Verdicts          0 verdict types from 0 rules
  S6  Flow Paths        0 flows
  S7  Complexity        max predicate depth 0, max flow depth 0
  S8  Verdict Unique    no verdicts to check

  ✓ All 8 properties verified in 1ms

S1 now enumerates 3 states. S2 confirms all 3 are reachable from draft via the declared transitions. No dead states.

Step 3: Declare a Source

A source declares where external data comes from. It is infrastructure metadata — it has zero effect on evaluation but it tells humans and tooling where facts originate.

source review_service {
  protocol:    http
  base_url:    "https://api.reviews.internal/v1"
  description: "Internal document review service"
}

Add this above the entity. Sources do not affect static analysis output — tenor check will produce the same results. But the source is now available for facts to reference.

Step 4: Add a Fact

A fact is a typed value from an external source. The contract declares what data it needs; the runtime provides it. Add a fact that references the source you just declared:

fact review_passed {
  type:    Bool
  source:  review_service { path: "reviews/{document_id}.passed" }
  default: false
}

This declares that the contract needs a boolean called review_passed, that the review_service is its authoritative source, and that the default value is false (reviews start as not-passed).

The static analysis output does not change — facts are inputs, not analyzable structures. But the fact is now available for rules to reference.

Step 5: Add a Rule

A rule evaluates facts and produces verdicts. Verdicts are named, typed conclusions that operations can depend on as preconditions.

rule check_review {
  stratum: 0
  when:    review_passed = true
  produce: verdict review_ok {
    payload: Bool = true
  }
}

This rule sits at stratum 0, meaning it reads facts directly (not other verdicts). When review_passed is true, it produces a verdict called review_ok. Stratum 0 rules can only reference facts. Higher strata can reference verdicts from lower strata.

tenor check approval.tenor

$ tenor check approval.tenor

✓ Elaboration: 6 passes, 0 errors

  Static Analysis
  ─────────────────────────────────────────────────────
  S1  State Space       1 entity, 3 states total
  S2  Reachability      3/3 states reachable, 0 dead states
  S3  Admissibility     0 operations
  S4  Authority         2 personas, 0 authority entries
  S5  Verdicts          1 verdict type from 1 rule
  S6  Flow Paths        0 flows
  S7  Complexity        max predicate depth 1, max flow depth 0
  S8  Verdict Unique    all verdict types uniquely produced

  ✓ All 8 properties verified in 1ms

S5 now reports 1 verdict type from 1 rule. S7 shows predicate depth 1 (one level of fact evaluation). S8 confirms review_ok is produced by exactly one rule — no ambiguity.

Step 6: Add an Operation

An operation is the only way to change entity state. It binds a persona, a precondition, and effects together. Add an operation that lets the operator approve a document, but only when the review verdict is present:

operation approve_document {
  allowed_personas: [operator]
  precondition:     verdict_present(review_ok)
  effects:          [(Document, draft, approved)]
  error_contract:   [precondition_failed, persona_rejected]
}

This says: only the operator persona can approve, and only when review_ok is active. The effect transitions Document from draft to approved. The error contract declares the exhaustive set of failure modes as bare identifiers.

Add a second operation for rejection — the admin can reject when the review has not passed:

operation reject_document {
  allowed_personas: [admin]
  precondition:     review_passed = false
  effects:          [(Document, draft, rejected)]
  error_contract:   [invalid_state, unauthorized]
}

tenor check approval.tenor

$ tenor check approval.tenor

✓ Elaboration: 6 passes, 0 errors

  Static Analysis
  ─────────────────────────────────────────────────────
  S1  State Space       1 entity, 3 states total
  S2  Reachability      3/3 states reachable, 0 dead states
  S3  Admissibility     2 operations, all structurally satisfiable
  S4  Authority         2 personas, 2 authority entries
  S5  Verdicts          1 verdict type from 1 rule
  S6  Flow Paths        0 flows
  S7  Complexity        max predicate depth 1, max flow depth 0
  S8  Verdict Unique    all verdict types uniquely produced

  ✓ All 8 properties verified in 1ms

S3 now reports 2 operations, both structurally satisfiable. S4 shows 2 authority entries — the operator can approve, the admin can reject. The authority topology is provably bounded.

Check the authority detail:

tenor check approval.tenor --authority

$ tenor check approval.tenor --authority

  Authority Topology
  ─────────────────────────────────────────────────────────────
  Persona    Entity     State    Can invoke
  ─────────────────────────────────────────────────────────────
  admin      Document   draft    reject_document
  operator   Document   draft    approve_document
  ─────────────────────────────────────────────────────────────

  Q: Can the admin approve a document?
  A: No. approve_document allows [operator] only.
     admin has no path to approved from any state.

  Q: Can the operator reject a document?
  A: No. reject_document allows [admin] only.
     operator has no path to rejected from any state.

Each persona has exactly one capability. The admin cannot approve. The operator cannot reject. This is a structural proof, not a runtime check.

Step 7: Add a Flow

A flow orchestrates operations into a multi-step process with frozen-snapshot semantics. Add a flow that executes the approval:

flow approval_flow {
  snapshot: at_initiation
  entry:    step_approve

  steps: {
    step_approve: OperationStep {
      op:      approve_document
      persona: operator
      outcomes: {
        success: Terminal(success)
      }
      on_failure: Terminate(outcome: approval_failed)
    }
  }
}

The snapshot: at_initiation means the fact set and verdict set are captured when the flow starts and frozen for the duration. This prevents TOCTOU races — facts cannot change between evaluation and execution.

tenor check approval.tenor

$ tenor check approval.tenor

✓ Elaboration: 6 passes, 0 errors

  Static Analysis
  ─────────────────────────────────────────────────────
  S1  State Space       1 entity, 3 states total
  S2  Reachability      3/3 states reachable, 0 dead states
  S3  Admissibility     2 operations, all structurally satisfiable
  S4  Authority         2 personas, 2 authority entries
  S5  Verdicts          1 verdict type from 1 rule
  S6  Flow Paths        1 flow, 2 paths, all terminate
  S7  Complexity        max predicate depth 1, max flow depth 1
  S8  Verdict Unique    all verdict types uniquely produced

  ✓ All 8 properties verified in 2ms

S6 now reports 1 flow with 2 paths (success and failure), both terminating. S7 shows flow depth 1. Every path through the flow has been statically enumerated and verified.

The Complete Contract

Here is the full approval.tenor file — 42 lines:

persona admin
persona operator

source review_service {
  protocol:    http
  base_url:    "https://api.reviews.internal/v1"
  description: "Internal document review service"
}

entity Document {
  states:  [draft, approved, rejected]
  initial: draft
  transitions: [
    (draft, approved),
    (draft, rejected)
  ]
}

fact review_passed {
  type:    Bool
  source:  review_service { path: "reviews/{document_id}.passed" }
  default: false
}

rule check_review {
  stratum: 0
  when:    review_passed = true
  produce: verdict review_ok {
    payload: Bool = true
  }
}

operation approve_document {
  allowed_personas: [operator]
  precondition:     verdict_present(review_ok)
  effects:          [(Document, draft, approved)]
  error_contract:   [precondition_failed, persona_rejected]
}

operation reject_document {
  allowed_personas: [admin]
  precondition:     review_passed = false
  effects:          [(Document, draft, rejected)]
  error_contract:   [invalid_state, unauthorized]
}

flow approval_flow {
  snapshot: at_initiation
  entry:    step_approve

  steps: {
    step_approve: OperationStep {
      op:      approve_document
      persona: operator
      outcomes: {
        success: Terminal(success)
      }
      on_failure: Terminate(outcome: approval_failed)
    }
  }
}

Elaborate

The elaborator parses the .tenor file, validates every construct, and produces the interchange JSON — the universal representation that all downstream tooling consumes:

tenor elaborate approval.tenor --pretty

{
  "version": "1.0",
  "contract_id": "approval",
  "entities": [
    {
      "id": "Document",
      "states": ["draft", "approved", "rejected"],
      "initial": "draft",
      "transitions": [
        { "from": "draft", "to": "approved" },
        { "from": "draft", "to": "rejected" }
      ]
    }
  ],
  "personas": ["admin", "operator"],
  "sources": [
    {
      "id": "review_service",
      "protocol": "http",
      "fields": {
        "base_url": "https://api.reviews.internal/v1",
        "auth": "bearer_token",
        "description": "Internal document review service"
      }
    }
  ],
  "facts": [
    {
      "id": "review_passed",
      "type": { "kind": "Bool" },
      "source": { "ref": "review_service" },
      "default": false
    }
  ],
  "rules": [
    {
      "id": "check_review",
      "stratum": 0,
      "when": {
        "op": "eq",
        "left": { "ref": "review_passed" },
        "right": { "literal": true }
      },
      "produce": {
        "verdict_id": "review_ok",
        "payload": { "type": { "kind": "Bool" }, "value": true }
      }
    }
  ],
  "operations": [
    {
      "id": "approve_document",
      "allowed_personas": ["operator"],
      "precondition": { "op": "verdict_present", "verdict": "review_ok" },
      "effects": [
        { "entity": "Document", "from": "draft", "to": "approved" }
      ],
      "error_contract": {
        "precondition_not_met": "Review verdict is not present. Cannot approve.",
        "invalid_state": "Document is not in draft state.",
        "unauthorized": "Only operator can approve documents."
      }
    },
    {
      "id": "reject_document",
      "allowed_personas": ["admin"],
      "precondition": { "literal": true },
      "effects": [
        { "entity": "Document", "from": "draft", "to": "rejected" }
      ],
      "error_contract": {
        "invalid_state": "Document is not in draft state.",
        "unauthorized": "Only admin can reject documents."
      }
    }
  ],
  "flows": [
    {
      "id": "approval_flow",
      "snapshot": "at_initiation",
      "entry": "step_approve",
      "steps": {
        "step_approve": {
          "type": "OperationStep",
          "op": "approve_document",
          "persona": "operator",
          "outcomes": {
            "approved": { "type": "Terminal", "outcome": "success" }
          },
          "on_failure": { "type": "Terminal", "outcome": "failure" }
        }
      }
    }
  ]
}

The interchange JSON is the canonical machine-readable representation. The evaluator, platform, SDKs, and code generators all consume this format — not the .tenor source file.

What You Built

This contract declares:

• 2 personas with bounded authority — the operator can approve, the admin can reject, and neither can do the other's job
• 1 entity with 3 states and 2 transitions — every state is reachable, no dead states
• 1 external source with declared protocol and authentication
• 1 fact referencing that source with a typed default
• 1 rule at stratum 0 producing a verdict from the fact
• 1 operation gated by the verdict with a mandatory error contract
• 1 flow with frozen-snapshot semantics preventing TOCTOU races

All 8 static analysis properties pass. The authority topology is a proven fact. The flow paths are exhaustively enumerated. And you did not write a single test — the proofs are derived from the contract structure itself.

Next Steps

Now that you have a working contract, learn how to run the evaluator to compute verdicts and action spaces at runtime.