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.
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. This configuration does not exercise
view-change safety properties. LockedValueSafety is checked structurally but
view changes that test lock propagation across rounds require MaxView ≥ 1. This is the
highest-priority extension for Phase 2 model checking.
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.
Two properties from the Q9 source document — NoDoubleSpend and
TokenStateMonotonicity — are not named INVARIANT lines in the TLC
configuration. NoDoubleSpend is structurally enforced by the state
machine: the SubmitReview action's guard requires nullifier ∉
nullifier_set, making double-spend impossible by construction.
TokenStateMonotonicity (ISSUED → REDEEMED → SPENT) is likewise enforced
by action guards on each transition. Both properties hold — they are enforced
structurally rather than checked as separate invariants.
Where cryptography makes fraud structurally impossible, mechanism design makes the residual attack surface — merchant collusion — economically irrational.
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. Consensus guarantees (agreement, finality) feed economic IC/IR conditions. Documented in THREAT_MODEL.md §6.
Preconditions guard all state transitions. Leader ∈ Committee before
Propose. nullifier ∉ nullifier_set before SubmitReview.
token.status = ISSUED before Redeem. Violations are structurally
impossible, not merely detected.
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 (no conflicting decisions). LockedValueSafety (no equivocation). UniqueHonestProposalPerRound. PrepareVotesReferenceProposals.
Finalized tokens cannot be forged or duplicated (consensus Agreement). Network-wide nullifier uniqueness maintained (GlobalNullifierUniqueness). N validators participate at measured rate.
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).