REF — TLA+ Constants, Variables & Actions

01 — Constants

Fixed Parameters per Model-Checking Run

Constants define the boundaries of the state space TLC explores. They are fixed before each run — different values produce different verification scopes.

REFConsensus v1.9

Validators

SET of model values

The full set of validators in the network. Each is a distinct identity that can propose, vote, and decide.

{v1, v2, v3, v4}

Byzantine

SUBSET of Validators

Validators controlled by the adversary. Can propose conflicting values, vote arbitrarily, and equivocate.

{v4}

Values

SET of model values

Abstract proposals that validators agree on. Two values ensure the model tests conflicting proposals.

{val1, val2}

MaxHeight

Nat

Maximum blockchain height to explore. Bounds the state space to keep TLC tractable.

MaxView

Nat

Maximum view (round) per height. MaxView=0 means view changes are not exercised in this harness.

NIL

Model value

Sentinel value representing "no decision yet" or "no locked value." Used in per-validator state maps.

NIL

EV-008 TLC Configuration (actual values used in verification)

Validators{v1, v2, v3, v4}

Byzantine{v4}

Values{val1, val2}

MaxHeight1

MaxView0

States generated152,658,351

Distinct states17,588,825

Depth31

Time11m 06s

TokenLifecycle

Purchases

SET of model values

Finite set of purchase identifiers. Two purchases test cross-purchase isolation.

{p1, p2}

Nullifiers

SET of model values

Available nullifier identifiers. Three nullifiers (2 tokens + 1 spare) test uniqueness and collision attempts.

{n1, n2, n3}

Contents

SET of model values

Abstract review content values. Two distinct contents test review uniqueness per token.

{c1, c2}

EV-009 TLC Configuration (actual values used in verification)

Purchases{p1, p2}

Nullifiers{n1, n2, n3}

Contents{c1, c2}

CHECK_DEADLOCKFALSE (quiescence is correct behavior)

States generated269

Distinct states148

Depth7

Mechanism Design (Monte Carlo Parameters)

α (alpha)

Float — cost scaling exponent

Controls how fast attack costs grow per additional fake review. Higher α = steeper exponential cost curve.

[0.037 – 0.205]

C₀ (base cost)

Float — dollars

Baseline cost of a single attestation forgery. Includes bond escrow, validator fees, and platform integration costs.

[549 – 39,125]

γ (gamma)

Float — network exponent

How much the validator network amplifies attack difficulty. Network effects make fraud harder as N grows.

[1.77 – 2.90]

Integer — network size

Total validators in the network. Larger N strengthens security via the N^γ term in the cost function.

[1,041 – 19,969]

Float — reward curvature

Controls diminishing returns on fake reviews. R(v) = k·ln(1+v). The dominance condition requires α·C₀·N^γ > k.

[42,645 – 1,374,630]

02 — Variables

Mutable State TLC Explores

Variables define the state space. TLC exhaustively explores every reachable combination of variable values, checking invariants at each state.

REFConsensus v1.9 — 9 State Variables (Per-Validator)

Variable

Type

Purpose

height

[Validator → 0..MaxHeight]

Current blockchain height per validator

view

[Validator → 0..MaxView]

Current view (round) within the current height

decision

[Validator → Values ∪ {NIL}]

Finalized value per validator. Agreement invariant requires all non-NIL decisions to match.

lockedValue

[Validator → Values ∪ {NIL}]

Value this validator is locked on after seeing a prepare quorum. Prevents equivocation.

lockedView

[Validator → -1..MaxView]

The view at which lockedValue was set. -1 = not yet locked.

highestQC

[Validator → QCRecord]

Highest quorum certificate observed by this validator. Used in view changes.

prepareVotes

SUBSET VoteRecord

Set of PREPARE votes broadcast across the network. Accumulates until quorum.

commitVotes

SUBSET VoteRecord

Set of COMMIT votes. A quorum of matching commits triggers the Decide action.

decided

SUBSET DecisionRecord

Global set of decision records. Used for safety checking across all validators.

TokenLifecycle — 4 State Variables

Variable

Type

Purpose

purchases

SUBSET Purchases

Set of registered purchase identifiers. Grows monotonically.

tokens

[Purchases → TokenRecord ∪ {⊥}]

Maps each purchase to its token record (nullifier, content, status) or ⊥ if no token issued.

reviews

SUBSET ReviewRecord

Set of published review records, each bound to a token.

nullifier_set

SUBSET Nullifiers

Set of spent nullifiers. Append-only. Membership prevents double-spend.

03 — Actions

State Transitions — The Next Relation

Every action has a guard (precondition) and an effect (state mutation). TLC fires all enabled actions nondeterministically at each state, building the complete reachable state graph. Click any action to expand its guard and effect.

REFConsensus v1.9 — Honest Actions

Propose(v) Pre-Prepare

▾

Guard (precondition)

v ∈ Honest
v is leader for (height[v], view[v])
No existing proposal from v at this (h,v)

Effect (state change)

Create proposal record
Broadcast to all validators
Cast own PREPARE vote

TLC coverage: non-vacuous across all honest validators

Prepare(v) Prepare

▾

Guard

v ∈ Honest
Proposal exists for (height[v], view[v])
v has not yet voted PREPARE for this (h,v)

Effect

Add PREPARE vote to prepareVotes
Vote references existing proposal value

Lock(v) Lock

▾

Guard

v ∈ Honest
Quorum of matching PREPARE votes exists for value val
lockedView[v] < current view

Effect

lockedValue[v] ← val
lockedView[v] ← current view
highestQC[v] ← new QC record

Key safety mechanism: once locked, validator cannot vote for conflicting values

Commit(v) Commit

▾

Guard

v ∈ Honest
v is locked on a value
v has not yet COMMIT-voted at this (h,v)

Effect

Add COMMIT vote to commitVotes
Vote references lockedValue[v]

Decide(v) Decide

▾

Guard

v ∈ Honest
Quorum of matching COMMIT votes exists
decision[v] = NIL (not yet decided)

Effect

decision[v] ← committed value
Add to decided set
Advance height

Finality: once decided, the value is irrevocable for this height

REFConsensus v1.9 — Byzantine Actions

These actions model adversarial behavior. The Byzantine validator (v4) can equivocate, vote for conflicting values, and attempt to break safety. The invariants must hold despite these actions firing.

ByzPropose Byzantine

▾

Guard

Proposer ∈ Byzantine
Can propose ANY value (including conflicts)

Adversarial Effect

Propose conflicting values to different subsets
Stutter guard: proposal ∉ existing proposals

TLC executions: 251,966

ByzPrepare Byzantine

▾

Guard

Voter ∈ Byzantine
References an existing proposal
Vote ∉ prepareVotes (stutter prevention)

Adversarial Effect

Cast PREPARE vote for any existing proposal
Can vote for conflicting values at same (h,v)

TLC executions: 1,901,481

ByzCommit Byzantine

▾

Guard

Voter ∈ Byzantine
References an existing proposal
Vote ∉ commitVotes (stutter prevention)

Adversarial Effect

Cast COMMIT vote for any existing proposal
Can commit to conflicting values

TLC executions: 12,863,638

TokenLifecycle — Actions

CreatePurchase Lifecycle

▾

Guard

p ∈ Purchases
p ∉ purchases (not already registered)

Effect

purchases' = purchases ∪ {p}

IssueToken Lifecycle

▾

Guard

p ∈ purchases
tokens[p] = ⊥ (no token exists)
n ∈ Nullifiers \ used nullifiers

Effect

tokens'[p] = [nullifier ↦ n, status ↦ ISSUED]
Enforces AtMostOneTokenPerPurchase

SubmitReview Lifecycle

▾

Guard

tokens[p].status = ISSUED
tokens[p].nullifier ∉ nullifier_set
c ∈ Contents

Effect

reviews' = reviews ∪ {review record}
nullifier_set' = nullifier_set ∪ {nullifier}
tokens'[p].status = SPENT

Atomically: review published + nullifier spent + token consumed

RevokeToken Lifecycle

▾

Guard

tokens[p].status = ISSUED
No review exists for this token
(Refund scenario)

Effect

tokens'[p].status = REVOKED
Token can never be submitted

Handles ATK-10 (Refund Cycling) — token revoked on refund before review

04 — The Next-State Relation

How TLC Builds the State Graph

The Next relation is the disjunction of all actions. At every state, TLC fires every enabled action, exploring all possible interleavings.

REFConsensus_v1.9.tla

\* Next-state relation: disjunction of all actions Next == \/ ∃ v ∈ Honest: Propose(v) \/ ∃ v ∈ Honest: Prepare(v) \/ ∃ v ∈ Honest: Lock(v) \/ ∃ v ∈ Honest: Commit(v) \/ ∃ v ∈ Honest: Decide(v) \/ ByzPropose \* 251,966 executions \/ ByzPrepare \* 1,901,481 executions \/ ByzCommit \* 12,863,638 executions Spec == Init /\ [][Next]_vars

TokenLifecycle.tla

\* Next-state relation: token lifecycle transitions Next == \/ ∃ p ∈ Purchases: CreatePurchase(p) \/ ∃ p ∈ Purchases, n ∈ Nullifiers: IssueToken(p, n) \/ ∃ p ∈ Purchases, c ∈ Contents: SubmitReview(p, c) \/ ∃ p ∈ Purchases: RevokeToken(p) Spec == Init /\ [][Next]_vars

Design Note — Why No AdvanceView Action?

The EV-008 harness uses MaxView=0, meaning view-change transitions are not exercised. In the full v1.9 spec, AdvanceView and AdvanceHeight actions exist but are not in the critical path for the current safety proof. Extending to MaxView ≥ 1 to verify view-change lock propagation is the next verification milestone.

05 — Specification Evolution

From Simplified to Kiniry-Grade

The project-file Consensus.tla (84 lines) was the starting point. REFConsensus_v1.9.tla is the verified artifact. Key differences:

Aspect

Consensus.tla (original)

REFConsensus v1.9 (verified)

Variables

7 (epoch, view, Leader, Committee, Log, QC, Msgs)

9 per-validator (height, view, decision, lockedValue, lockedView, highestQC, prepareVotes, commitVotes, decided)

Actions

4 (Propose, PrepareQuorum, AdvanceView, NextCommittee)

8 (Propose, Prepare, Lock, Commit, Decide + ByzPropose, ByzPrepare, ByzCommit)

Byzantine model

None — all validators honest

Explicit Byzantine set with 3 adversarial actions

Locking

No lockedValue tracking

Per-validator lockedValue + lockedView

Phases

2 (Propose → PrepareQuorum)

4 (Propose → Prepare → Lock/Commit → Decide)

Invariants

2 (TypeOK, SafetyInvariant)

4 (Agreement, LockedValueSafety, UniqueHonestProposalPerRound, PrepareVotesReferenceProposals)

TLC result

Deadlock at 554K states (v1.8.1 sanity)

Clean pass: 152.7M states, 0 violations (EV-008)

Traceability

EV-008 artifact path: verification/evidence/EV-008_v1.9_final/ containing REFConsensus_v1.9.tla, REFConsensus_v1.9_bft_tiny.cfg, tlc_bft_tiny_COMPLETE.log, VERIFICATION_NOTES.md, and SHA256SUMS.txt.

EV-009 artifact path: token-lifecycle/ containing TokenLifecycle.tla, TokenLifecycle.cfg, and tlc_token_lifecycle.log.