Tenor's static analysis obligations define eight properties (S1 through S8) that a conforming analyzer must derive from a contract alone, without executing it. These are not optional lint checks --- they are structural guarantees that follow from Tenor's design constraints (C1 through C7). The tenor check command computes all eight properties and reports the results.
The core claim: every execution path is statically enumerable, every authority boundary is derivable, and every verdict is traceable to its source facts --- all from the contract text, before any code runs.
S1 --- Complete State Space
For each Entity, the complete set of states S(e) is enumerable.
What it proves
S1 guarantees that you can list every possible state for every entity in the contract. There are no hidden states, no dynamically created states, no states that emerge at runtime. The state set is exactly what the contract declares.
This is the foundation for all other properties. If you cannot enumerate states, you cannot reason about transitions, authority, or reachability.
Example output
$ tenor check escrow.tenor
S1 Complete state space
Escrow: {awaiting_funding, funded, released, refunded, disputed}
Payment: {pending, authorized, captured, voided}Every entity in the contract appears with its full declared state set. If a state is listed here, it exists. If it is not listed, it does not exist --- no runtime behavior can introduce a state not in this set.
S2 --- Reachable States
For each Entity, the set of states reachable from the initial state via the declared transition relation is derivable.
What it proves
S2 goes beyond S1 by analyzing the transition graph. Starting from each entity's declared initial state, the analyzer walks all declared transitions to determine which states are actually reachable. States that are declared but unreachable from the initial state are dead states --- they exist in the contract but no sequence of operations can ever reach them.
Dead state detection catches common authoring errors: a state was declared but the transition into it was forgotten, or a refactoring removed a transition path without removing the state.
Example output
$ tenor check escrow.tenor
S2 Reachable states
Escrow: {awaiting_funding, funded, released, refunded, disputed} (5/5 reachable)
Payment: {pending, authorized, captured} (3/4 reachable)
WARNING: dead state detected: {voided}
'voided' is not reachable from initial state 'pending'
via the declared transition relationA dead state warning does not make the contract invalid --- it compiles and evaluates correctly. But it indicates a likely authoring error. Either the state should be removed, or a missing transition should be added.
S3a --- Structural Admissibility
For each Entity state and each persona, the set of Operations whose preconditions are structurally satisfiable --- given only type-level information, without enumerating domain values --- and whose effects include a transition from that state is derivable.
What it proves
S3a answers: "In state X, which operations could possibly execute, based on types alone?" This is a type-level analysis. It checks whether an operation's precondition can ever be true by examining the types of the facts it references, without considering specific values.
For example, if a precondition compares a fact of type Enum(["pending", "confirmed"]) with the literal "approved", S3a detects that this is structurally unsatisfiable --- "approved" is not in the enum's variant set, so the comparison can never be true regardless of the fact's runtime value.
S3a is always computationally feasible. It runs in O(|expression tree|) per precondition. This is the analysis that tenor check always performs.
Example output
$ tenor check escrow.tenor
S3a Structural admissibility per state
Escrow.awaiting_funding:
buyer -> [fund_escrow]
seller -> []
arbiter -> []
Escrow.funded:
buyer -> [request_refund]
seller -> [release_escrow]
arbiter -> [release_escrow, force_refund]
Escrow.disputed:
buyer -> []
seller -> []
arbiter -> [resolve_dispute]
Escrow.released:
(terminal — no operations)
Escrow.refunded:
(terminal — no operations)This is the authority topology in action: for every entity state, you see exactly which personas can invoke which operations. Empty brackets mean the persona has no available actions in that state.
S3b --- Domain Satisfiability (Qualified)
A stronger version of S3a: for each Entity state and each persona, determine whether there exists a concrete FactSet and VerdictSet assignment under which the precondition evaluates to true.
What it proves
S3b goes beyond S3a by attempting to find actual fact values that make a precondition true. Where S3a asks "is this structurally possible?", S3b asks "does a concrete satisfying assignment exist?"
S3b is qualified: it is not always computationally feasible. The analysis requires model enumeration over the product of fact domain sizes. For facts with small domains (small Enum sets, narrow Int ranges, short List bounds), enumeration is fast. For facts with large domains (wide Int ranges, large Decimal precision, long Text), the enumeration space is astronomically large.
S3b is decidable in principle for all valid Tenor contracts (the language is non-Turing-complete), but the enumeration cost may be prohibitive in practice. Static analysis tools implementing S3b should document their domain size thresholds and fall back to S3a when enumeration is infeasible.
Example output
$ tenor check escrow.tenor --s3b
S3b Domain satisfiability per state
Escrow.funded, seller, release_escrow:
SATISFIABLE: inspection_passed = true, amount > 0
Escrow.funded, buyer, request_refund:
SATISFIABLE: days_since_funding > 30
Escrow.awaiting_funding, buyer, fund_escrow:
SATISFIABLE: amount >= min_escrow_amount
NOTE: fact 'amount' has range Int(0, 1000000) — enumeration feasible
Payment.pending, buyer, authorize_payment:
SKIPPED: fact 'payment_details' has type Text(max_length: 500)
— domain too large for enumeration, falling back to S3aS4 --- Authority Topology
For any declared Persona P and Entity state S, the set of Operations P can invoke in S is derivable. Whether a persona can cause a transition from S to S' is answerable.
What it proves
S4 is the complete authority map of the contract. For every persona, in every possible entity state, you know exactly what they can do. This is derived purely from the contract --- no runtime identity resolution, no external RBAC system, no ambient authority.
S4 enables security auditing without reading implementation code: "Can the buyer release funds directly?" is answerable from the contract alone. "Can any persona cause a transition from funded to released without the arbiter?" is answerable. The complete set of declared personas is statically known, enabling exhaustive enumeration of the authority relation.
Example output
$ tenor check escrow.tenor
S4 Authority topology
buyer:
can invoke: fund_escrow, request_refund
can cause: awaiting_funding -> funded
funded -> refunded (via request_refund, when conditions met)
seller:
can invoke: release_escrow
can cause: funded -> released
arbiter:
can invoke: release_escrow, force_refund, resolve_dispute
can cause: funded -> released
funded -> refunded
disputed -> released
disputed -> refundedThe authority topology is exhaustive. If a persona-state-operation triple is not listed, the persona provably cannot perform that operation in that state. There is no mechanism in the language to bypass this --- authority is structural, not configurable at runtime.
S5 --- Verdict and Outcome Space
The complete set of possible verdict types producible by a contract's rules is enumerable. The complete set of possible outcomes for each Operation is enumerable.
What it proves
S5 guarantees that you can list every verdict the contract can ever produce (across all rules at all strata) and every outcome each operation can ever return. There are no hidden verdicts, no dynamically generated outcomes.
For any operation O, the analyzer reports: "O can produce outcomes {o1, ..., on}" without executing the operation. This powers the exhaustive outcome handling requirement in flows (every outcome of every referenced operation must have a routing target).
Example output
$ tenor check escrow.tenor
S5 Verdict and outcome space
Verdicts:
EscrowEligibility (stratum 0) — produced by: check_eligibility
ComplianceStatus (stratum 0) — produced by: check_compliance
ReleaseApproval (stratum 1) — produced by: approve_release
Operation outcomes:
fund_escrow: {funded, rejected}
release_escrow: {released, held}
request_refund: {refunded, denied}
force_refund: {refunded}
resolve_dispute: {released, refunded}S6 --- Flow Path Enumeration
For each Flow, the complete set of possible execution paths, all personas at each step, all Operation outcomes at each OperationStep, all entity states reachable via the Flow, and all terminal outcomes are derivable.
What it proves
S6 enumerates every possible execution path through every flow. Since flows are finite DAGs (no loops, no unbounded recursion), and every OperationStep has a finite set of outcomes with exhaustive routing, the total number of paths is bounded and enumerable.
This means you can ask: "What are all the ways this flow can end?" and get a complete answer. For compliance and audit, S6 proves that every path has been considered --- there are no surprise execution sequences.
Example output
$ tenor check escrow.tenor
S6 Flow path enumeration
escrow_flow:
Path 1: start -> fund -> release -> [terminal: completed]
personas: buyer(fund), seller(release)
entity states: Escrow: awaiting_funding -> funded -> released
Path 2: start -> fund -> refund -> [terminal: refunded]
personas: buyer(fund), buyer(request_refund)
entity states: Escrow: awaiting_funding -> funded -> refunded
Path 3: start -> fund -> dispute -> resolve(released) -> [terminal: completed]
personas: buyer(fund), buyer(dispute), arbiter(resolve)
entity states: Escrow: awaiting_funding -> funded -> disputed -> released
Path 4: start -> fund -> dispute -> resolve(refunded) -> [terminal: refunded]
personas: buyer(fund), buyer(dispute), arbiter(resolve)
entity states: Escrow: awaiting_funding -> funded -> disputed -> refunded
Path 5: start -> fund(rejected) -> [terminal: funding_failed]
personas: buyer(fund)
entity states: Escrow: awaiting_funding (unchanged)
Total: 5 paths, 3 terminal outcomesS7 --- Evaluation Complexity Bounds
For each PredicateExpression, the evaluation complexity bound is statically derivable. For each Flow, the maximum execution depth is statically derivable.
What it proves
S7 guarantees that you can know, before execution, the worst-case computational cost of evaluating any predicate and the maximum depth of any flow. This follows from Tenor's non-Turing-completeness: no loops, no unbounded recursion, no aggregation.
For predicates, complexity depends on the expression tree depth and any bounded quantification (forall, exists) over List facts. The bound is O(product of List max bounds) for quantified expressions, O(expression tree depth) for quantifier-free expressions.
For flows, the maximum depth is the longest path in the flow DAG, including sub-flow expansion. Since flows are finite DAGs with no cycles, this is always bounded.
Example output
$ tenor check escrow.tenor
S7 Evaluation complexity bounds
Predicates:
check_eligibility.when: O(1) — no quantifiers, 3 comparisons
check_compliance.when: O(n) — forall over compliance_items (max: 20)
approve_release.when: O(1) — verdict_present + 1 comparison
Flows:
escrow_flow: max depth 4 (fund -> dispute -> resolve -> end)
review_flow: max depth 2 (check -> decide -> end)S8 --- Verdict Uniqueness
For each VerdictType name, at most one Rule in the contract may declare a
produceclause for that VerdictType. If two or more Rules produce the same VerdictType name, the contract is statically rejected.
What it proves
S8 guarantees that every verdict has a single, unambiguous source rule. There is no runtime conflict resolution, no priority-based override, no non-deterministic verdict production. If you see verdict ComplianceStatus in an evaluation result, it came from exactly one rule --- always the same rule.
This is enforced during Pass 5 as a structural check. It does not require predicate satisfiability analysis or reachability reasoning --- it is a simple uniqueness constraint on (verdict_type_name, rule_id) pairs.
Example output
When S8 holds (the normal case), tenor check simply confirms it:
$ tenor check escrow.tenor
S8 Verdict uniqueness
All verdict types have unique producers. (5 verdicts, 5 rules)When S8 is violated, the elaborator rejects the contract at Pass 5:
$ tenor check broken.tenor
error[pass 5]: duplicate VerdictType 'ComplianceStatus'
Rule 'check_basic_compliance' at stratum 0 produces 'ComplianceStatus'
Rule 'check_enhanced_compliance' at stratum 0 also produces 'ComplianceStatus'
help: Use distinct VerdictType names for each rule.
If both rules contribute to the same logical verdict,
use a higher-stratum aggregation rule that consumes both.Design rationale
Contracts that require conditional production of the same logical verdict from different rules should use distinct VerdictType names for each condition and, if needed, a higher-stratum aggregation rule. This preserves explicit provenance (you always know which rule produced which verdict) and avoids the need for a runtime resolution strategy.
Running Static Analysis
# Full analysis (S1-S8)
tenor check contract.tenor
# JSON output (machine-readable)
tenor check contract.tenor --format json
# Verbose mode (includes S3b where feasible)
tenor check contract.tenor --verbose
# Check a multi-file contract
tenor check contracts/main.tenorAll S1-S8 properties are computed from the interchange bundle produced by the elaborator. The analyzer (tenor-analyze crate) consumes the same TenorInterchange format as the evaluator and SDKs. This means the analysis results are guaranteed to match what the evaluator will execute --- there is no representation gap between analysis and execution.