Tenor

Appearance

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 ​

bash
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:

hcl
persona admin
persona operator

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

Run the checker:

bash
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:

hcl
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.

bash
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.

hcl
source review_service {
  protocol:    http
  base_url:    "https://api.reviews.internal/v1"
  auth:        bearer_token
  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:

hcl
fact review_passed {
  type:    Bool
  source:  review_service
  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.

hcl
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.

bash
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:

hcl
operation approve_document {
  allowed_personas: [operator]
  precondition:     verdict_present(review_ok)
  effects:          [(Document, draft, 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."
  }
}

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 what happens when each failure mode occurs — these are mandatory.

Add a second operation for rejection (no precondition required — the admin can reject anytime):

hcl
operation reject_document {
  allowed_personas: [admin]
  precondition:     true
  effects:          [(Document, draft, rejected)]
  error_contract: {
    invalid_state: "Document is not in draft state."
    unauthorized:  "Only admin can reject documents."
  }
}
bash
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:

bash
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:

hcl
flow approval_flow {
  snapshot: at_initiation
  entry:    step_approve

  steps: {
    step_approve: OperationStep {
      op:      approve_document
      persona: operator
      outcomes: {
        approved: Terminal(success)
      }
      on_failure: Terminal(failure)
    }
  }
}

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.

bash
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:

hcl
persona admin
persona operator

source review_service {
  protocol:    http
  base_url:    "https://api.reviews.internal/v1"
  auth:        bearer_token
  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
  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_not_met: "Review verdict is not present. Cannot approve."
    invalid_state:        "Document is not in draft state."
    unauthorized:         "Only operator can approve documents."
  }
}

operation reject_document {
  allowed_personas: [admin]
  precondition:     true
  effects:          [(Document, draft, rejected)]
  error_contract: {
    invalid_state: "Document is not in draft state."
    unauthorized:  "Only admin can reject documents."
  }
}

flow approval_flow {
  snapshot: at_initiation
  entry:    step_approve

  steps: {
    step_approve: OperationStep {
      op:      approve_document
      persona: operator
      outcomes: {
        approved: Terminal(success)
      }
      on_failure: Terminal(failure)
    }
  }
}

Elaborate ​

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

bash
tenor elaborate approval.tenor --pretty
json
{
  "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.