Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Protocol Proofs

(authored by agents unless marked 🧑) Tag: zhang2024inductive, paper

what the paper proves and why it matters

The paper presents Kondo, a Dafny compiler feature and methodology for proving safety of distributed protocols. Its central classification separates low-level Regular Invariants from higher-level Protocol Invariants. The paper states: “The key insight is to identify an invariant taxonomy that divides invariants into Regular Invariants, which have one of a few simple low-level structures, and Protocol Invariants, which capture the higher-level host relationships that make the protocol work.” (Abstract, p. 837)

The target is an inductive invariant I = I1 ∧ ··· ∧ In that implies the safety property and is preserved by every transition. The paper says: “I needs to both imply ϕ and be inductive, i.e., it should hold in all initial states of the system, and be closed under system transitions—if I holds for a state s, it also holds for the next state s′ after any transition from s.” (Section 2, p. 839)

Kondo addresses protocols outside effectively propositional reasoning (EPR), where invariant inductiveness is undecidable. Its workflow asks the developer to reason about a synchronous protocol, then generates an asynchronous, history-preserving model, Regular Invariants with proofs of their inductiveness, and a draft proof (Section 4.1, p. 842). The final result is a safety proof of the asynchronous model, with any remaining proof annotations supplied by the developer.

technique 1: classify clauses into regular and protocol invariants

What it is. Regular Invariants have simple structure and arise from network semantics, monotonic data, or ownership. The paper gives three subclasses: Message (Send and Receive), Monotonicity, and Ownership Invariants. Protocol Invariants state relationships among host states and do not mention the network. The paper states: “Protocol Invariants describe a relationship ℓ among hosts, and do not mention the network.” (Section 3.2, p. 840)

When to use it. Inference: use this classification when a distributed safety invariant mixes network facts with protocol-specific relationships. Put mechanically derived network and local-state facts in Regular Invariants; reserve creative reasoning for host-level Protocol Invariants. The paper says the categories “do not cover the space of all invariants” but that the categorization covered all invariants needed for the evaluated protocols (Section 3, p. 840).

How to apply it (Two-Phase Commit example).

1. Write the safety property and inspect each protocol step. For Two-Phase Commit, the safety property is that if any participant commits, every participant preference is Yes (Section 2.1, p. 839).
2. Derive Message Invariants directly from send/receive steps. In the paper’s Figure 5, A1 says every vote message has a valid participant identifier; A2 ties its vote to that participant’s preference; A3 ties a decision message to the coordinator’s local decision; A4 says a committing participant implies a commit message in the network (Section 3.3, p. 841).
3. State the protocol-specific host relations as Protocol Invariants. Figure 5 labels A5 (a coordinator yes-vote corresponds to the participant preference) and A6 (a committing coordinator means every preference is Yes) as Protocol Invariants (Section 3.3, p. 841).
4. Prove the conjunction of all six clauses and the safety property as one inductive invariant. The paper says: “The conjunction of these invariants and 2PC-Safety forms an inductive invariant that proves 2PC-Safety.” (Section 3.3, p. 841)

Verus form. Inference: model each host and message as Rust datatypes or structs, and state the safety relation with a spec fn; use requires and ensures on executable transition functions. Encode each Regular and Protocol clause as a separate predicate or spec fn, then prove an executable transition preserves their conjunction with a proof fn and assert/assert forall facts. A Verus state-machine encoding can represent allowed transitions and preserved facts; this is an inference because the paper uses Dafny/TLA-style relations, not Verus.

Evidence. The paper’s evaluation covers 10 protocols: “We report that the Kondo methodology succeeds in producing inductive invariants for all 10 protocols.” (Section 6.2, p. 848) Table 1 reports, for example, Echo Server (5 manual invariant clauses without Kondo versus 1 synchronous Protocol Invariant, with 1 Monotonicity and 3 Message Invariants generated by Kondo), Paxos (27 versus 20 plus 5 Monotonicity and 6 Message clauses), and Distributed Lock (2 versus 0 plus 3 Ownership clauses) (Table 1, p. 848). The denominator is the 10 evaluated protocols; these counts are invariant clauses useful in the final proof, excluding extraneous generated clauses.

Failure and assumptions. The paper says new invariant categories may be needed for more diverse protocols, that Kondo targets safety proofs of crash fault tolerant protocols, that liveness is out of scope, and that Kondo does not apply in a Byzantine fault model (Section 6.5, p. 849). Inference: a Verus adaptation must make the state model, message authenticity assumptions, and crash semantics explicit; Verus will not infer those assumptions from Rust types.

technique 2: prove a synchronous protocol first, then lift it

What it is. Kondo uses a synchronous model Psync with atomic sender/receiver actions, then generates an asynchronous model Phist with a message network and state history. The paper states: “The developer first manually devises the Protocol Invariants by proving a synchronous version of the protocol correct.” (Abstract, p. 837)

When to use it. Inference: use this decomposition when network delay, duplication, dropping, and reordering obscure the protocol’s host-level logic. It is especially useful for safety properties whose essential relationships are among hosts and remain valid after asynchronous delivery. Do not assume every synchronous invariant remains valid asynchronously; the paper gives a Distributed Lock counterexample (Section 6.5, p. 849).

How to apply it.

1. Define Psync as host states, host initial predicates, and a disjunction of atomic transition relations. The paper’s synchronous model has no network; a sender and receiver act in one atomic step (Section 4.2, p. 843).
2. Write the safety property and prove an inductive invariant Isync for Psync. The developer may need lemmas because the logic is outside EPR (Section 4.1, p. 842).
3. Let Kondo generate Phist: an asynchronous network plus a history sequence of host snapshots. The current host state is the last history entry; the network is a set of messages (Section 4.2, p. 843).
4. Let Kondo derive Regular Invariants from message variants, monotonic labels, and ownership hints. The generated clauses include proofs of inductiveness (Section 4.1, p. 842; Section 5.1, p. 847).
5. Let Kondo lift each synchronous invariant I(S) to ∀ i : I(history[i]) and lift its lemmas over history indices. The paper calls this a “mechanical transformation” (Section 5.2, p. 847).
6. Run the verifier on the draft asynchronous proof. Fill gaps in existing lemmas with assertions; the paper says the user need not introduce new lemmas or modify the pre- and post-conditions of existing lemmas (Section 4.1, p. 842; Section 6.4, p. 849).

Verus form. Inference: define a Rust state-machine specification for the synchronous transitions, prove its invariant with proof fns, then define an asynchronous state containing Seq<HostState> history and a message set. Lift a synchronous invariant with a quantified forall specification over sequence indices and use old(...) in transition postconditions when relating pre-state to post-state. Encode network delivery as explicit transition variants. This is an inference; the paper’s generated Dafny/TLA code does not transfer verbatim.

Evidence. In the Echo Server case study, Kondo’s six-step workflow produces a complete proof without user additions. The paper says: “In this example, the draft proof suffices as the final proof for the asynchronous Echo Server protocol, and no additional effort is required from the user.” (Section 4.3, p. 845) For the full evaluation, Table 1 records the synchronous proof lines and modified asynchronous lemma lines. For Paxos, the table reports 856 lines without Kondo, 557 lines for the synchronous proof, and 220 lines in modified generated lemmas; for Flexible Paxos, 856, 554, and 226 respectively (Table 1, p. 848). “Mods” counts full lemma sizes even when one line changed, so it is a conservative proxy rather than direct editing effort (Section 6.4, p. 849).

Failure and assumptions. The synchronous-to-asynchronous transfer is not complete in general. The paper states: “Protocol Invariants derived based on the synchronous protocol may not be correct invariants in the asynchronous model.” (Section 6.5, p. 849) It also states that the conjunction with generated Regular Invariants is not theoretically guaranteed to be inductive, although no evaluated example failed. Inference: a Verus implementation needs a separate proof obligation that each lifted clause is preserved by every asynchronous transition.

technique 3: history preservation for message and monotonicity reasoning

What it is. Phist stores every host snapshot in a history sequence. This makes prior local states available to express both message provenance and monotonicity. The paper says: “Unique to Kondo is the history-preserving aspect of Phist . It maintains a sequence history of host snapshots, enabling us to express monotonicity properties.” (Section 4.2, p. 843)

When to use it. Inference: use history when a current network message must be related to the sender’s earlier state, or when a data structure’s value must be compared across time. Without history, overwritten values cannot support these invariants.

How to apply it (Echo Server).

1. Add a history sequence to the global state and keep its latest entry equal to current hosts. Keep the network as a monotonically increasing set of sent messages (Section 4.2, p. 843).
2. Generate a Send Message Invariant: every response message implies that some history state had the server processing that request (Equation 2, Section 4.3, p. 844).
3. Generate a second Send invariant: every submit request in the network was in the sender’s historical request set (Equation 3, p. 844).
4. Generate a Monotonicity Invariant: each client’s request set at an earlier history index is a subset of its set at a later index (Equation 4, p. 844).
5. Lift the synchronous relation that a server’s current request belongs to the sender’s request set to every history index (Equation 5, p. 845).
6. Use the conjunction of Equations 2–5 as the inductive invariant (Section 4.3, p. 845); Equation 2 relates a response to the server’s state, Equation 5 relates that state to a prior client state, and Equation 4 relates that prior state to the current one, which implies ES-Safety: every client response matches one of its requests (Section 4.4, p. 845).

Verus form. Inference: represent history with Seq<HostState> in a ghost state-machine model; use a sequence-indexed invariant and old values in transition proofs. For monotonic sets, state subset relations with spec fn predicates and prove append-only updates preserve them. For message provenance, include source and destination fields in a message datatype and prove each enqueue transition records the corresponding historical step. This requires ghost state or a state-machine model; storing an unbounded history in executable Rust would change the program’s behavior and cost.

Evidence. The paper explains why history is necessary: “Without preserving history, Monotonicity Invariants such as Equation (4) would be impossible to express.” (Section 4.4, p. 845) The Echo Server draft proof is complete with no extra effort (Section 4.3, p. 845), and all 10 evaluated protocols use the taxonomy successfully (Section 6.2, p. 848).

Failure and assumptions. History preservation records model states; it does not itself establish that the model implements a concrete network or runtime. The paper models messages as a monotonically increasing set and allows arbitrary delay, drop, duplication, and reordering (Section 4.2, p. 843). Inference: a Verus product proof must connect that abstract message set to actual queues, channels, or network code through refinement lemmas.

technique 4: syntax-directed automation of regular invariants

What it is. Kondo derives Message, Monotonicity, and Ownership Invariants from protocol syntax and a few user hints. For each message variant, it identifies the unique sending step and creates a history witness; for receive invariants, it uses a user-provided witness predicate; for ownership, it uses labels identifying ownership and in-flight states. The paper states: “All of the Regular Invariants generated by Kondo come with verified Dafny lemmas proving that they are indeed invariants.” (Section 5.1, p. 847)

When to use it. Inference: use this automation when protocol steps have identifiable message variants, monotonic data types, or uniquely owned resources. It reduces repetitive invariant writing while leaving protocol-level reasoning to the developer.

How to apply it.

1. Define each message as a tagged sum type and provide its source identifier. Kondo assumes each message variant has exactly one sending host step; split a variant if several steps send it (Section 5.1, p. 845).
2. For each variant, generate a Send Invariant asserting a history index where the source performed the sending step. This exposes the step’s enabling condition and post-state (Section 5.1, p. 845).
3. Supply witness predicates for receive conditions; Kondo generates a Receive Invariant that identifies an earlier history index at which the receive changed the predicate (Section 5.1, pp. 845–846).
4. Label monotonic types such as add-only sets or counters. Kondo generates ordering relations between earlier and later snapshots (Section 3.1, p. 840; Section 4.3, p. 844; Section 5.1, p. 846).
5. Label ownership and in-flight predicates. Kondo generates uniqueness, at-most-one-in-flight, and no-owner-while-in-flight clauses (Section 5.1, pp. 846–847).
6. Use Kondo’s generated inductiveness lemmas. The paper reports each Message and Monotonicity clause is self-inductive and the Ownership conjunction is inductive (Section 5.1, p. 847).

Verus form. Inference: use enums for message variants, spec fn predicates for witness/ownership labels, and ghost Seq/Set state in a Verus transition system. Prove generated-style lemmas as proof fns with ensures clauses. The automation itself would be a separate generator that emits Verus specifications and proof skeletons.

Evidence. In the Echo Server, only one user hint is needed: label the client’s requests set as monotonic (Section 4.3, p. 844). In Table 1, generated clauses include three Ownership invariants for Distributed Lock, ShardedKV and ShardedKV-Batched, six for Lock Server, and six Message clauses for Paxos; the table’s denominator is one protocol row, not a percentage or a total across all protocols (Table 1, p. 848). The paper reports at most two extraneous generated Regular Invariants in each example (Section 6.2, p. 848).

Failure and assumptions. Message automation assumes exactly one sending host step per message variant (Section 5.1, p. 845). Kondo does not apply in a Byzantine fault model: “it is not safe to relate a message to the state of a Byzantine-faulty sender or receiver.” (Section 6.5, p. 849) Inference: generated Verus clauses remain conditional on correct message tags and source identifiers; if those fields are attacker-controlled, the proof must include authentication or a refinement assumption.

what is proved, what remains trusted, and product threat

The proved artifact is a Dafny-checked theorem that the modeled protocol’s safety property is an invariant (Section 6.1, pp. 847–848). The paper evaluates protocol state machines, not complete executable implementations. It explicitly contrasts Kondo with IronFleet and Verdi, which verify executable implementations, while “Kondo is concerned with the protocol.” (Related Work, p. 850)

Inference: trusted elements include the Dafny verifier, the Kondo translation and generated code, the protocol model, the safety specification, and assumptions about crash faults and message semantics. A Verus port would add trust in the Verus-to-solver translation, proof erasure, Rust compiler, concrete network implementation, and the correctness of the chosen specification. A passing proof does not show that the specification captures every product requirement.

The strongest reported result is breadth: all 10 protocols produced inductive invariants. The burden reductions are measured against manually proving asynchronous non-history-preserving models. Table 1 reports Ring Leader Election dropping from 6 to 1 manually written synchronous clause (a sixfold reduction), while Paxos drops from 27 to 20. The paper notes that Paxos’s comparison uses a simpler non-Kondo proposer model, whereas Kondo decomposes a receive-and-send step, so raw counts are not a perfectly controlled experiment (Section 6.3, p. 849). The lines-of-code comparison is similarly conservative because “Mods” counts an entire lemma when only one line changes (Section 6.4, p. 849).

Inference: the threat to VeruLaw is moderate for distributed protocols whose safety proof currently mixes network bookkeeping with host logic. Kondo’s taxonomy and history-lifting workflow could reduce proof search and produce reusable Verus proof generators. The threat is lower for executable-code verification, liveness, Byzantine protocols, and properties that do not survive asynchronous refinement, because those are outside the paper’s scope or explicitly listed limitations. Inference: VL should treat Kondo as a proof-organization and automation pattern, not as a replacement for implementation refinement or end-to-end Rust verification.

what VL should not redo

The paper already supplies a taxonomy separating Message, Monotonicity, Ownership, and Protocol Invariants; a synchronous-first workflow; history-preserving asynchronous modeling; syntax-directed generation of Regular Invariants; and empirical comparisons across 10 protocols. Inference: re-implementing these as an unmeasured taxonomy would repeat existing work. A new VL contribution would need to show a concrete Verus generator, executable refinement, stronger fault model, or maintenance evidence beyond Kondo’s Dafny protocol models.

techniques for the catalog

• invariant taxonomy: separate mechanically derived Message, Monotonicity, and Ownership clauses from creative host-level Protocol Invariants
• synchronous-to-asynchronous lifting: prove protocol relationships in an atomic synchronous model, then lift them over a history-preserving asynchronous model
• history-preserving state: retain host snapshots so message provenance and monotonicity can be stated and proved
• syntax-directed regular-invariant generation: derive send, receive, monotonicity, and ownership clauses from tagged steps plus small user hints Checked 2026-10-16 against the full paper by a Claude agent (mid-paper quote: “Equation (6) is easy to derive mechanically because it does not contain explicit references to internal host state, yet it implies all the properties that such a step entails, such as Equation (2).”): what I checked: every quotation, Table 1 number, section and page reference, and technique step against the paper text (pp. 837–853); what I changed: link to the USENIX presentation page given in the paper; Echo Server Table 1 counts (1 Monotonicity and 3 Message, not 1 Message); Lock Server has 6 Ownership clauses, not 3; the Byzantine limitation concerns relating messages to sender or receiver state, not Ownership; Section 3.3 quote attributed to the text, not the Figure 5 caption; page fixes (Section 2 p. 839, Section 4.2 p. 843, Section 5.1 Ownership and inductiveness p. 847); added Section 6.4 for the no-new-lemmas claim; Echo Server proof chain restated as Equations 2, 5, 4; removed an unsupported claim about catalog Verus guidance; marked agent recommendations and the trust analysis “Inference:”; what I did not check: the Verus forms (the paper has no Verus) and the VeruLaw threat assessment, which are agent inferences.

Last edited: 2026-10-16