What does REF formally specify, what invariants does TLC check, and what Rigorous Digital Engineering principles guide the verification architecture? A complete map of REF's three specification layers.
REF's TLA+ specifications are organized into three layers, each addressing a distinct correctness domain. Together they form the assume-guarantee chain that connects cryptographic primitives to economic incentives.
Four invariants checked by TLC across 152,658,351 states with non-vacuous Byzantine behavior. Configuration: 4 validators (v1–v4), 1 Byzantine (v4), 2 competing values, MaxHeight=1, MaxView=0. Zero violations. Zero states remaining on queue.
REFConsensus_v1.9.tla. Within the
EV-008 bounded state space, honest decision-history records at the same height
cannot disagree. This is a bounded model result, not an unbounded or
production-network no-fork theorem.
lockedView. It is not itself a
cross-view safety invariant, and EV-008 at MaxView=0 did not exercise
ViewChange.
prepareVotes set references a proposal with the same height, view,
and value. The v1.9 model has no Msgs state variable.
The canonical v1.9 source defines additional predicates including TypeOK,
NoConflictingDecisions, NoConflictingPrepareQCs, and
NoConflictingCommitsAtHeight. The EV-008 cfg selects exactly four
invariants: Agreement, LockedValueSafety,
UniqueHonestProposalPerRound, and
PrepareVotesReferenceProposals. Defined does not mean TLC-checked.
The v1.9 spec includes explicit Byzantine actions: ByzPropose (251,966
executions), ByzPrepare (1,901,481 executions), ByzCommit
(12,863,638 executions). The adversary was active across millions of state transitions
— this is not a vacuous pass on a system with no Byzantine behavior.
MaxView=0 in the EV-008 harness. LockedValueSafety was
selected and TLC-checked in the EV-008 harness at MaxView=0. The final action
coverage records ViewChange=0:0 and ReceiveQC=83394:9327900.
The run exercised ReceiveQC but no ViewChange transitions, so it
does not establish lock-displacement safety across later views (MaxView >= 1).
Seven invariants checked by TLC across 269 states (exhaustive for the tiny harness: 2 purchases, 3 nullifiers, 2 content values). Clean pass on February 11, 2026. Zero violations. Zero states remaining on queue.
tokens is a set of token records, not a map from purchases.
tokens and whose status is "valid".
TypeOK separately requires every token to reference a registered purchase.
nullifierSet belongs to a token that has at least one review.
In the model, SubmitReview adds the review and the token’s nullifier in the same state
transition; review records reference a token, not a nullifier directly.
nullifierSet, and is enforced by the IssueToken guard
n ∉ NullifiersInUse.
TokenLifecycle.tla defines exactly seven invariant operators in Inv, all listed above.
Single-use review behavior is enforced by the SubmitReview nullifier guard and
nullifierSet update. The model’s only token-status update is the RevokeToken
replacement from "valid" to "revoked". No additional lifecycle-status operator is
presented here as a source invariant.
Cryptographic controls establish specific modeled integrity properties under the stated assumptions; mechanism design addresses residual economic incentives such as merchant collusion.
Analytic: D(v) = C'(v) − R'(v). Since C'(v) = α·C₀·eαv·Nγ and R'(v) = k/(1+v), the condition D(0) > 0 reduces to α·C₀·Nγ > k.
Empirical: mc_results_quick.csv — 500 parameter draws,
all 500 satisfy honesty_dominates = True over tested ranges
(α ∈ [0.037, 0.205], C₀ ∈ [549, 39125], γ ∈ [1.77, 2.90], N ∈ [1041, 19969]).
The TLA+ specifications embody four principles from Rigorous Digital Engineering that structure the entire verification approach.
Each TLA+ spec traces to security requirements above (threat model, security properties) and implementation artifacts below (circuit signals, API schemas). The spec bridges "what must hold" and "what the code does."
Layers state what they assume and guarantee. Crypto guarantees (binding, soundness) feed consensus assumptions. EV-008's bounded checked consensus properties feed economic IC/IR conditions. Documented in THREAT_MODEL.md §6.
In the v1.9 consensus model, honest Propose and
Prepare are guarded by CanVoteFor(validator, val).
Commit additionally requires a prepare quorum and
lockedValue[validator] = val with
lockedView[validator] = view[validator]. A false guard disables that
transition in the modeled state space. The result excludes that transition only within the checked model and bounded configuration; it does not establish the absence of analogous violations in deployment.
Properties are verified within explicit finite bounds (4 validators, MaxView=0 for consensus; 2 purchases, 3 nullifiers for tokens). Limitations are documented, not hidden. Unbounded verification requires theorem provers (TLAPS), planned for Phase 2.
REF's three layers compose through explicit contracts. Each layer's guarantees become the next layer's assumptions.
Binding commitments (Poseidon), unforgeable signatures (Ed25519), sound proofs (Groth16 128-bit), domain-separated tags prevent cross-protocol replay.
Attestations are unforgeable (honest merchant ⇒ valid signature). Tokens are binding (witness cannot be forged). Nullifiers are collision-resistant.
Agreement, LockedValueSafety,
UniqueHonestProposalPerRound, and
PrepareVotesReferenceProposals, under the EV-008 finite bounds
including MaxView=0. These results do not establish liveness,
rotating-committee semantics, or cross-view safety.
Cross-layer use must import only claims established by the relevant artifacts.
EV-008 Agreement does not by itself prove token immutability,
network-wide nullifier uniqueness, or deployment participation rates.
Transparency requires distinguishing verified claims from planned work. Every entry traces to a specific artifact and TLC log.
Bounded model checking proves properties hold within the explored state space — not universally. The green items are verified by TLC logs. The cyan items hold by construction (action guards) but are not separate INVARIANT lines. The amber items are gaps where formal methods expertise would accelerate the work. The refinement from TLA+ to running Circom/Python code is human-maintained, not machine-checked (DEF-02).