Safety vs Liveness

Origin: composes, foundational distributed-systems theory from the 1980s, not something Solidus originated. Solidus status: testnet, safety is formally checked; liveness has been engineered against and bug-fixed, but not field-tested.

Safety and liveness are the two things any consensus protocol has to promise, and they pull in different directions. Safety means "nothing bad ever happens", informally, the network never finalizes two conflicting blocks at the same height, no matter how badly things go wrong. Liveness means "something good eventually happens", the network keeps making progress and doesn't just freeze forever, even when some participants misbehave or the network is slow. A protocol that never finalizes anything is perfectly safe (it can't contradict itself) but useless. A protocol that finalizes whatever it's told, instantly, is perfectly live but unsafe. Real consensus protocols have to hold both at once, and the interesting engineering is in exactly how.

Where it comes from

The Byzantine Generals framing (a group of generals who must agree on a plan even though some might be traitors) was formalized by Leslie Lamport, Robert Shostak, and Marshall Pease in 1982. A harder result followed in 1985: Michael Fischer, Nancy Lynch, and Michael Paterson proved that under fully asynchronous networking (no bound on message delay at all), no deterministic protocol can guarantee both safety and liveness if even one node might fail, the "FLP impossibility result." This is why every practical BFT protocol, including HotStuff, assumes partial synchrony, messages eventually arrive within some (possibly unknown) bound, rather than claiming to have solved an impossible problem. Solidus didn't originate any of this; its consensus engine composes the standard HotStuff approach to the tradeoff.

How Solidus's engine holds each half

Safety comes from the locked_qc rule described under Fork Choice: a validator will not vote for a proposal that conflicts with a block it has already locked in, full stop, regardless of network conditions. Liveness comes from the pacemaker: if a round's leader fails to produce a valid proposal within a timeout, validators broadcast timeout votes, and once enough accumulate (see View Change), the round advances to a new leader with a longer timeout, so the network doesn't wait forever on one stuck or malicious proposer.

Getting the liveness half right in practice is genuinely fiddly, and Solidus's own development history has a concrete example worth naming rather than hiding: when the network goes idle (no pending transactions, so no reason to keep producing empty blocks), the pacemaker's countdown needs to be handled carefully on the transition back to active. An early version could leave a stale, long-expired deadline in place, which fired a burst of timeout votes racing against a genuinely fresh proposal and could kill a legitimate transaction block. That was found and fixed. It's mentioned here as evidence of what liveness engineering against a real adversary actually looks like, not as a claim that no such issue could recur.

What's been checked, and what hasn't

Formally, safety is well-covered: an exhaustive TLA+ model check of the exact commit rule, including Byzantine and equivocating replicas, explored 963,033 states and found zero violations. Liveness is on weaker footing: the pacemaker's timeout values were tuned and tested against in-process channels within a small, team-run four-node committee, not against real network latency, jitter, or partition between genuinely independent operators. Solidus's own engineering notes describe this gap plainly rather than papering over it.

Check it yourself

The TLA+ specification and TLC model-checker results in the public solidusnetwork/protocol repository are independently re-runnable safety evidence. There is no equivalent public liveness benchmark against real, adversarial network conditions today, none exists to point to.

Related terms: Fork Choice · View Change · Quorum Certificate · HotStuff · BFT · Finality