[Qian-Cheng-nju]

LeadersAreNodes is declared in BlockDag, but INSTANCE BlockDag does not assert it in Sailfish. The two TLC wrappers already check it explicitly; the standalone specification does not.

A one-node instance shows the gap:

N == {a}
F == {}
R == 1..3
GST == 0
Leader(r) == b
IsQuorum(Q) == a \in Q
IsBlocking(B) == a \in B

With a and b distinct, this satisfies Sailfish's other assumptions. Node a reaches round 3 with an empty log, violating Liveness because the designated round-1 leader b never had a vertex.

Assert the existing LeadersAreNodes definition after the instance. TLC then rejects this configuration before initialization. Changing the leader to a still reaches round 3 and commits <<a,1>>; TLCSailfish1 also passes with unchanged state counts.