Correctness guarantees versus empirical evidence

Why it matters

"Does Raft guarantee that?" and "how do you know?" are different questions, and research discussions in systems, databases and networking switch between them constantly. Confusing a measured property with a guaranteed one leads to wrong designs: a system never observed to lose data under test is not a system that cannot lose data.

Core ideas

Three kinds of claims. A guarantee follows from an argument covering every execution a model allows: at most one leader per term, committed entries are never lost, transactions are serializable. A design argument explains why a mechanism should help without proving it. An empirical result reports what happened in particular runs: latency, throughput, availability under a workload. A claim-evidence table should label each.

Every guarantee has a model. Read the fine print: crash-stop or Byzantine failures, synchronous or asynchronous network, bounded clock error, storage that is durable once a write is acknowledged. Raft is a clean example. Section 5.6 of its paper requires that safety never depend on timing, while availability does: Raft can elect and keep a steady leader as long as broadcast time is much smaller than the election timeout, which in turn is much smaller than the mean time between failures. This mirrors a classic result: in an asynchronous system where even one process may crash, no deterministic consensus protocol can guarantee termination, so practical protocols keep safety always and make progress only when timing is good enough.

Safety, liveness and invariants. Safety says nothing bad happens, and a violation shows up in a finite trace. Liveness says something good eventually happens. Safety is usually proved through an invariant: a predicate that holds initially and is preserved by every allowed step, hence true in every reachable state. Finding the right inductive invariant is most of the work, and the same invariant is what tests and runtime assertions should check. Evaluations usually report liveness-like behaviour (election or recovery time) as measured distributions, not as guarantees.

How strong is the evidence? Roughly from weaker to stronger: informal argument, paper proof, model checking (exhaustive, but only for bounded configurations such as three servers and short logs), mechanized proof (checked by a machine, but only for the stated specification and assumptions). Raft's correctness section is instructive: a formal specification, a mechanically checked proof of one property that relies on invariants not themselves mechanically checked, and an informal proof of state machine safety. The seL4 project publishes the assumptions behind its kernel proofs, such as correct assembly code, hardware and boot; the guarantee is exactly as strong as that list.

Specification versus implementation. A proved algorithm does not make the code correct. Implementations add batching, snapshots, membership changes and optimizations, each of which can break an invariant. Testing, fuzzing, fault injection and checking recorded histories against a consistency model are evidence about the implementation: they can find violations but never prove their absence.

Assumptions can be empirical. Spanner's external consistency is guaranteed provided the uncertainty interval reported by TrueTime always contains true time. Keeping that bound small and correct is an engineering achievement supported by measurement. Name both layers when you discuss such systems: the conditional guarantee and the evidence that its condition holds.

Performance is rarely guaranteed. "Commit latency under 10 ms" in an evaluation means "observed under this workload and hardware". A worst-case bound needs analysis and assumptions; the largest observed value is only a sample statistic.

Common misconceptions

• "The tests pass, so the protocol is correct." Tests sample executions; rare interleavings and failure combinations may never occur.
• "The algorithm is proven, so the system is correct." The proof covers a model; the implementation and environment are separate claims.
• "Model checking proves correctness." It explores bounded configurations exhaustively; larger configurations remain an extrapolation unless proven.
• "Raft guarantees progress." It guarantees safety; progress needs its timing assumptions to hold.
• "The measured worst case is a bound." It is the largest value you happened to observe.

How to approach it

Classify every claim in Raft's safety, timing and evaluation sections, then do the same for Spanner's external-consistency argument and its clock-uncertainty measurements. In interviews, answer "is X guaranteed?" with the model, the property and the evidence type. Graduates should separate safety from liveness; senior candidates should also discuss the specification-implementation gap and how they would test invariants.