The claim

An OpenSearch cluster keeps its metadata in one cluster state that an elected node, the cluster-manager, publishes to the others. Every node runs the per-node consensus state machine CoordinationState, transcribed and specified in the OpenSearchCoordination mission, driven by the Coordinator over a network that loses, duplicates, delays and reorders messages, while nodes crash and restart. What the protocol is designed to guarantee is safety: in every execution, at most one node is cluster-manager in each term, each (term, version) names one cluster state, and committed cluster states never fork: of any two committed states, one builds on the other. Elastic's TLA+ model ZenWithTerms, which CoordinationState.java cites as its formal model, states these properties for that model and checks them with TLC on small instances; its "main invariant" is that committed publications are related by descent. OpenSearch's randomized test CoordinationStateTests.testSafety, built on CoordinationStateTestCluster, checks the first two properties on random executions of the Java class.

This mission proves these properties, for compatible bootstrap configurations and OpenSearch's default election strategy, for every number of nodes and every execution of a cluster model in which each node runs the transcribed Java code of OpenSearch revision b2a54ba5c0defba3d1d20423e911d4bf920bab19. The goal theorem is committed_linear: any two committed publications lie on one branch of the history.

The model

A cluster is the state of every node together with the set of messages sent so far. A step is one successful call of a CoordinationState method at one node, its output, if any, being added to the set: bootstrapping with a bootstrap configuration (setInitialState, under its asserted preconditions); handling a start-join request from any cluster-manager-eligible node for any term (elections, abdication, and the term bumps on receiving a message of a higher term), the join being sent to the requester; handling a join; publishing a new cluster state as an elected node (handleClientValue, under its asserted precondition); accepting a publication; handling a publish response, a resulting commit being sent; applying a commit; and restarting. A message, once sent, stays available: it may be handled any number of times, in any order, by any node it may be delivered to, or never. The steps cover every call the Coordinator makes; its own guards only reject more calls.

A cluster-manager-eligible node persists its current term and accepted state synchronously, and a restart keeps them except for the parts rebuilt at startup; a node that never joined a cluster may come back with another term-0 state, restored from the remote cluster-state store. A node that is not cluster-manager-eligible persists asynchronously or not at all, and may restart with any state. Nodes may bootstrap with different configurations, as ClusterBootstrapService allows when they have discovered different subsets of the nodes listed in cluster.initial_cluster_manager_nodes. Each publication records, as ghost data the real message does not carry, the term and version of the state its publisher had accepted: its parent. Descent along parents is the history in which the theorems are stated.

What is proved

The public statements about reachable clusters assume that the bootstrap configurations are compatible (any two have intersecting quorums of cluster-manager-eligible nodes) and that the election strategy is OpenSearch's default.

• Committed states never fork (committed_linear, the goal): any two committed publications are related by descent. A version is committed in at most one term, and committed versions increase with the term (committed_versions); every commit is of a publication (committed_published).
• Leader completeness (leader_completeness): every publication of a later term descends from every committed publication; a cluster-manager of a later term always builds on it.
• One cluster-manager per term (one_master_per_term: all publications of a term come from one node), one cluster state per term and version (one_state_per_version: same publisher, same state, same parent), election safety (election_safety: two nodes that hold a won election at the same moment, in the same current term, are the same node).
• The assertions of CoordinationState.invariant() never fail at a cluster-manager-eligible node (javaInvariant_reachable), although not every handler preserves them on its own: the per-node mission shows that handlePublishRequest can break them. Every eligible node's last committed configuration is empty, a bootstrap configuration, or the accepted configuration of a committed publication (lastCommitted_committed).
• Bootstrapping with partial views gives compatible configurations (bootstrap_compatible): the configurations ClusterBootstrapService builds meet the compatibility condition the safety statements assume, whatever subset of the required nodes each bootstrapping node has discovered, provided each requirement names the same node everywhere. The theorem is about the configurations alone; that the model's bootstrap configurations are of this form is not formalized.
• The common hypotheses can be met together with a commit (commit_reachable): a one-node cluster bootstraps, elects itself, publishes and commits. Only one committed key is exhibited: neither two distinct committed keys nor a publication of a later term than a committed key.

The proof is an inductive invariant of 30 facts about nodes, joins, publish responses, publications, commits and leaders (reachable_inv), preserved by each of the nine kinds of step (one theorem per step, under the same two hypotheses), together with 22 lemmas about a single cluster satisfying it: the publications form a forest; along a branch with no commit in between, a newly accepted configuration remains one of the two configurations in force (at most one reconfiguration in flight between commits); and election leader completeness, by strong induction on the term: an election in term t builds on every commit of an earlier term, because otherwise the first commit above the last committed ancestor of the election's base would have a responder among the election's voters, who accepted that commit before voting, which places it below the base after all. Two elections of one term therefore share a voter, and a voter joins one candidate per term.

Findings

The model transcribes the Java, not the TLA+ model, and differs from TLA+ where the code does. Java's handleCommit lacks the TLA+ guard that an elected node has accepted its own last publication: a cluster-manager can apply the commit of its accepted state while its next publication is in flight, and its committed configuration then changes in the middle of that publication. As a result the TLA+ invariant CommitHasQuorumVsPreviousCommittedConfiguration fails for the Java semantics (a 17-step execution: a publication is committed by responders that are not a quorum of its last committed configuration). Safety is unaffected: those responders are a quorum of the accepted configuration of the committed parent, and the invariant records exactly this weaker commit condition. A cluster-manager's last committed configuration can also move backwards. A plugin election strategy that can turn a won election into a lost one (OpenSearch ships only the default) can break "one state per term and version" when Java assertions are disabled (an 11-step execution), which is why the theorems assume the default strategy. The TLA+ invariant CommittedValuesDescendantsFromInitialValue fails harmlessly, because joins of term 0 compare metadata versions. In CoordinationStateTestCluster, the branch that makes a node that is not cluster-manager-eligible lose its persisted state on reboot no longer has any effect since the persisted-state registry was introduced.

Before the proof, two independently designed invariants were checked with explicit-state model checkers of the same message-passing model, with a single bootstrap configuration: about 29 million states by breadth-first search and 6 million random steps for the first, about 1.33 billion states for the second (including two complete runs of 25.4 and 201.1 million states), and inductiveness spot-checks over 39 and 149 million successor steps, without a counterexample.

What this rests on

The Java source at the pinned revision: CoordinationState.java through the per-node mission's transcription, whose definitions are imported, and, for the steps, Coordinator.java, ClusterBootstrapService.java and GatewayMetaState.java.

• Assumptions outside the model. A node's cluster-manager role never changes (a node restarted without the cluster-manager and data roles overwrites its persisted state with term 0, so changing the role and back can reset its term); persisted state is never rolled back; the offline opensearch-node tools are not used; each bootstrap requirement names the same node at every node; every node uses the default election strategy; a publication delivered through the remote cluster-state store reconstructs exactly the published state. The per-node abstractions apply (terms are natural numbers, versions integers without overflow).
• The Coordinator is not transcribed. That each of its calls into CoordinationState is a step of the model is argued from the code, not proved; its other duties (mode changes, the publication pipeline and its timeouts, fault detection, join validation, reconfiguration choices) are outside the theorems.
• Liveness is not proved here. Nothing says that an election eventually succeeds or that a publication is eventually committed; the pre-voting mission covers single rounds, progress when nothing disrupts an election or a publication is the subject of a separate mission over the same cluster model, and the randomized election timers of another.