The concrete building blocks of REF's TLA+ specifications. What parameters are fixed, what state TLC explores, and what transitions define the protocol's behavior — sourced directly from the verified artifacts.
Constants define the boundaries of the state space TLC explores. They are fixed before each run — different values produce different verification scopes.
Next; Byzantine validators can execute the Byzantine action families. The canonical v1.9 model has no explicit network/message-delay layer.Variables define the state space. TLC exhaustively explores every reachable combination of variable values, checking invariants at each state.
[Validators -> 0..MaxHeight][Validators -> 0..MaxView][Validators -> Values \cup {NIL}]Agreement is instead quantified over honest records in decided at equal height; NoConflictingDecisions is the separate transient-state predicate and is not selected by the EV-008 cfg.[Validators -> Values \cup {NIL}]Lock. CanVoteFor permits the locked value unless a strictly higher highestQC governs the vote.[Validators -> -1..MaxView][Validators -> [view: -1..MaxView, value: Values \cup {NIL}]]CanVoteFor reads highestQC; Lock and ReceiveQC update it; ViewChange preserves it unchanged.SUBSET [validator: Validators, h: 0..MaxHeight, v: 0..MaxView, val: Values]HasPrepareQuorum.SUBSET [validator: Validators, h: 0..MaxHeight, v: 0..MaxView, val: Values]Decide when its other guards hold.SUBSET [validator: Validators, h: 0..MaxHeight, val: Values]Agreement compares records whose validators are in Honest and whose heights are equal.SUBSET [proposer: Validators, h: 0..MaxHeight, v: 0..MaxView, val: Values]TokensForPurchase(p) = {}.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.
v ∈ Honest
height[v] < MaxHeight
view[v] <= MaxView
decision[v] = NIL
∃ val ∈ Values
CanVoteFor(v, val)
Let HProps be the honest proposals at height[v]/view[v]: HProps = {} OR ∃ p ∈ HProps with p.val = val
No proposal already exists from v at height[v]/view[v]
proposals' = proposals ∪ {[proposer ↦ v, h ↦ height[v], v ↦ view[v], val ↦ val]}
UNCHANGED: height, view, lockedValue, lockedView, decision, prepareVotes, commitVotes, highestQC, decided
v ∈ Honest
height[v] < MaxHeight
view[v] <= MaxView
decision[v] = NIL
HonestHasNotVoted(v, prepareVotes)
∃ p ∈ proposals with p.h = height[v] and p.v = view[v]
CanVoteFor(v, p.val)
prepareVotes' adds [validator ↦ v, h ↦ p.h, v ↦ p.v, val ↦ p.val]
UNCHANGED: height, view, lockedValue, lockedView, decision, commitVotes, highestQC, decided, proposals
v ∈ Honest
height[v] < MaxHeight
view[v] <= MaxView
decision[v] = NIL
∃ val ∈ Values with HasPrepareQuorum(height[v], view[v], val)
view[v] > lockedView[v]
lockedValue[v] ← val
lockedView[v] ← view[v]
highestQC[v] ← [view ↦ view[v], value ↦ val]
UNCHANGED: height, view, decision, prepareVotes, commitVotes, decided, proposals
v ∈ Honest
height[v] < MaxHeight
view[v] <= MaxView
decision[v] = NIL
∃ val ∈ Values with HasPrepareQuorum(height[v], view[v], val)
lockedValue[v] = val
lockedView[v] = view[v]
HonestHasNotVoted(v, commitVotes)
commitVotes' adds [validator ↦ v, h ↦ height[v], v ↦ view[v], val ↦ val]
UNCHANGED: height, view, lockedValue, lockedView, decision, prepareVotes, highestQC, decided, proposals
v ∈ Honest
height[v] < MaxHeight
decision[v] = NIL
∃ val ∈ Values with HasCommitQuorum(height[v], view[v], val)
decision[v] ← val
decided' adds [validator ↦ v, h ↦ height[v], val ↦ val]
UNCHANGED: height, view, lockedValue, lockedView, prepareVotes, commitVotes, highestQC, proposals
v ∈ Honest
decision[v] ≠ NIL
height[v] < MaxHeight
height[v] ← height[v] + 1
view[v] ← 0; decision[v] ← NIL; lockedValue[v] ← NIL; lockedView[v] ← -1; highestQC[v] ← [view ↦ -1, value ↦ NIL]
UNCHANGED: prepareVotes, commitVotes, decided, proposals
v ∈ Honest
view[v] < MaxView
decision[v] = NIL
view[v] ← view[v] + 1
UNCHANGED: height, lockedValue, lockedView, decision, prepareVotes, commitVotes, highestQC, decided, proposals
v ∈ Honest
∃ other ∈ Validators
other ≠ v
height[other] = height[v]
highestQC[other].view > highestQC[v].view
highestQC[v] ← highestQC[other]
UNCHANGED: height, view, lockedValue, lockedView, decision, prepareVotes, commitVotes, decided, proposals
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.
validator ∈ Byzantine
∃ h ∈ 0..MaxHeight, vw ∈ 0..MaxView, val ∈ Values
Let prop = [proposer ↦ validator, h ↦ h, v ↦ vw, val ↦ val]
prop ∉ proposals
proposals' = proposals ∪ {prop}
UNCHANGED: height, view, lockedValue, lockedView, decision, prepareVotes, commitVotes, highestQC, decided
validator ∈ Byzantine
∃ p ∈ proposals
Let vote = [validator ↦ validator, h ↦ p.h, v ↦ p.v, val ↦ p.val]
vote ∉ prepareVotes
prepareVotes' = prepareVotes ∪ {vote}
UNCHANGED: height, view, lockedValue, lockedView, decision, commitVotes, highestQC, decided, proposals
validator ∈ Byzantine
∃ p ∈ proposals
Let vote = [validator ↦ validator, h ↦ p.h, v ↦ p.v, val ↦ p.val]
vote ∉ commitVotes
commitVotes' = commitVotes ∪ {vote}
UNCHANGED: height, view, lockedValue, lockedView, decision, prepareVotes, highestQC, decided, proposals
p ∈ Purchases
p ∉ purchases (not already registered)
purchases' = purchases ∪ {p}
UNCHANGED: tokens, reviews, nullifierSet
p ∈ purchases
TokensForPurchase(p) = {}
n ∈ Nullifiers
n ∉ NullifiersInUse
tokens' = tokens ∪ {[purchase ↦ p, status ↦ "valid", nullifier ↦ n]}
UNCHANGED: purchases, reviews, nullifierSet
t ∈ tokens
t.status = "valid"
c ∈ Contents
ReviewsForToken(t) = {}
t.nullifier ∉ nullifierSet
reviews' = reviews ∪ {[token ↦ t, content ↦ c]}
nullifierSet' = nullifierSet ∪ {t.nullifier}
UNCHANGED: purchases, tokens
t ∈ tokens
t.status = "valid"
ReviewsForToken(t) = {}
t.nullifier ∉ nullifierSet
tokens' = (tokens \ {t}) ∪ {[purchase ↦ t.purchase, status ↦ "revoked", nullifier ↦ t.nullifier]}
UNCHANGED: purchases, reviews, nullifierSet
The Next relation is the disjunction of all actions. At every state,
TLC fires every enabled action, exploring all possible interleavings.
The exact v1.9 action is ViewChange; there is no
AdvanceView action in v1.9. The EV-008 harness sets
MaxView=0, so the golden log records zero
ViewChange executions. ReceiveQC is present and was
exercised, but EV-008 still does not exercise distinct-view safety behavior.
This section uses only the bound canonical REFConsensus_v1.9.tla,
EV-008 cfg, and EV-008 golden log. It makes no predecessor-version or introduction/delta claim.
REFConsensus_v1.9.tla VARIABLES / varsREFConsensus_v1.9.tla Nextvalidator \in Honest; Byzantine actions are separately guarded by validator \in Byzantine.INVARIANTS in the bound cfg.INVARIANTS.ViewChange: 0 executions at MaxView=0. ReceiveQC: 83,394 final recorded executions.
Bound current evidence:
evidence/REFConsensus_v1.9.tla,
evidence/REFConsensus_v1.9_bft_tiny.cfg, and
evidence/tlc_bft_tiny_COMPLETE.log.
Historical predecessor comparisons are not verification evidence.