Verification Playground

The broker catalog's own description of this model, reproduced from its verification document.

The data-path model (data_path_model) composes the production HWM core (ReplicaState), whose high watermark stands still while the ISR is under min.insync.replicas as Kafka's Partition.maybeIncrementLeaderHW does, the leader's ISR expansion kernel (isr_candidate_selected), the leader-epoch truncation lookup (epoch_and_offset_for_entries), the controller failover decision (failover_one), the KIP-966 recovery election (select_leader), the KIP-966 ELR maintenance rule (next_partition_elr), fetch visibility (compute_visibility_window), and, on the diskless path, the WAL-durable HWM and the controller's offset reservation (reserve_offsets over the image's PartitionOffsetAdvance counter). It checks three brokers, one partition, and at most three leader epochs. data_clean (strategy None, unclean disabled, log length 4) reaches exactly 762,237 unique states and requires committed_durable and no_loss_when_clean. data_unclean (Balanced recovery, unclean enabled, log length 4) reaches exactly 1,471,603 and requires committed_durable while witnessing unclean_loss. data_elr (min.insync.replicas 2, log length 3) reaches exactly 898,023; the real ELR set is handed to failover_one, so a partition whose live ISR empties elects a surviving ELR member cleanly, and each election is applied by the rule that chose it: an ISR election truncates nothing and is checked by committed_durable, an ELR member must hold, and an ELR election must keep, every record that reached the HWM (elr_holds_every_committed_record, elr_election_keeps_every_committed_record), and only an election reported as losing data sets lost. Anti-vacuity witnesses require a high watermark held back by min ISR while every ISR member holds a later record (hwm_held_by_min_isr), an ELR to be published, an ELR election to happen, and one to pass over a strictly longer surviving log. data_diskless reaches exactly 450 and requires that a WAL-acknowledged record is never lost, that the HWM is released by WAL sync alone, and that reserved offset ranges are gap-free and unique. All four are pinned by PINNED_UNIQUE_STATES_* in data_path_model/runner.rs, below the depth-70, 60,000,000-generated, and 8,000,000-unique guards. Record payloads, transactions, remote storage, multiple partitions, and the last-known-ELR half of KIP-966 remain outside the model.

The broker catalog's own description of this model, reproduced from its verification document.

The producer-state model (producer_state_model) drives the host's retained-batch bookkeeping (ProducerEntry::retained_batches and earlier_after_append) and check_retained around the proved producer_decision, for one producer ID over one- and two-record batches. It compares every answer with an independent classification by Kafka's rules over a ghost window of the five batches Kafka retains (NUM_BATCHES_TO_RETAIN), and the decision_matches_kafka property turns any disagreement into a counterexample. Witnesses require a duplicate of the last, of an older, and of the oldest of five retained batches, an out-of-order refusal of a retry below a full window, and an epoch bump. The basic config (epochs 0 and 1, sequences through 6) and the wide config (epochs through 3, sequences through 9) reach exactly 731 and 4,233 unique states, pinned by PINNED_UNIQUE_STATES_BASIC and PINNED_UNIQUE_STATES_WIDE, below the depth-40 and 2,000,000-state truncation guards. The broker serializes one producer's requests, so the model enumerates submit sequences rather than concurrent requests; offsets, snapshots, and transactions remain outside the model.

The broker catalog's own description of this model, reproduced from its verification document.

The replica-state model (replica_state_model) holds the production ReplicaState and drives its install_isr, update_follower_leo, and recompute_hw_for_leader_append for one partition with three replicas, a fixed leader, and log ends through 3. It explores every interleaving of leader append, follower fetch, and ISR installation. A follower's reported log end never regresses, and an ISR expansion admits only a follower whose log end reached the high watermark, the high-watermark half of Kafka's Partition.isFollowerInSync. ISR changes are explicit actions rather than timed decisions, so the lag rule is not checked here. Properties require the high watermark to stay nonnegative and inside the leader's log, every ISR member to hold every committed record (no_data_loss), follower log ends clamped to the leader's, and the leader in the ISR; a transition check requires a nondecreasing high watermark. Witnesses cover an advanced high watermark, one that reaches the leader's log end, one held below it by a lagging member, and an ISR shrink. The isr_safety config and the isr_overshoot config, whose followers may report a log end past the leader's to exercise the clamp, each reach exactly 174 unique states, pinned by PINNED_UNIQUE_STATES_SAFETY and PINNED_UNIQUE_STATES_OVERSHOOT, below the depth-80 and 200,000-state truncation guards. Wall-clock lag, the controller's AlterPartition path, and I/O remain outside the model.

The broker catalog's own description of this model, reproduced from its verification document.

The fetch-session model (fetch_session_model) drives the production KIP-227 forget-then-merge composition apply_incremental over sequences of incremental fetches, starting from a fully resolved session. Topic references carry a name only (Fetch v12 and below), an ID only (v13 and above), or both, over two names and two IDs, so the search covers a rename (same ID, new name) and a conflicting ID on one partition. The no_shadow property requires that no two cached keys name one logical partition, that is, the same partition and a shared identity half; no_orphan_default requires every cached entry to carry a requested max_bytes, and a transition check requires the cache to reflect each subscribed partition with the requested max_bytes. Witnesses cover a rename, an emptied session, ID-only and name-only keys, and two keys on one partition. The basic config (four references) and the wide config (seven references) reach exactly 18 and 148 unique states, pinned by PINNED_UNIQUE_STATES_BASIC and PINNED_UNIQUE_STATES_WIDE, below the depth-30 and 500,000-unique-state guards. The production merge resolves a request that matches two cached keys in HashMap iteration order; the checked properties hold for every resolution. Session epochs, eviction, and the wire codec remain outside the model.

The broker catalog's own description of this model, reproduced from its verification document.

The Fetch visibility model (fetch_visibility_model) drives the production compute_visibility_window over advancing partition watermarks, kept in Kafka's order 0 <= log_start <= lso <= hw <= log_end with KFC-1's log_start <= deliverable <= hw. Each advance action raises one watermark by one, and retention carries the delivery watermark along with the log start. A Fetch probe runs every consumer and follower fetch shape at every offset up to one past the log end. Each probe checks the clamp contract: a consumer never reads at or past the high watermark or the delivery watermark, a read-committed consumer stops at min(lso, hw), and a follower reads to the log end. Each probe also checks that every fetcher is told the partition's high watermark and min(lso, hw), as Kafka's Partition.readRecords reports them, and each advance checks that neither reported watermark regresses (KIP-227). Witnesses cover an LSO clamp, a delivery-watermark clamp, a delivery watermark above the LSO, a follower read past the high watermark, and an out-of-range fetch after retention. Log ends through 4 and 7 reach exactly 182 and 1,254 unique states, pinned by PINNED_UNIQUE_STATES_BASIC and PINNED_UNIQUE_STATES_WIDE, below the depth-40 and 200,000-state truncation guards. Record reads, remote tiers, and the fetch-session cache remain outside the model.

The broker catalog's own description of this model, reproduced from its verification document.

The failover model (leader_failover_model) drives the production failover_one over one three-replica partition with brokers dying, reviving, and rejoining the ISR (the leader-side isr_maintenance_selected and controller-side isr_admission kernels), and recomputes the published eligible-leader set after every change with the production next_partition_elr. The assignment is [1, 3, 2], so ISR order and assignment order differ. Each decision is checked in the transition against Kafka's one-broker rule for a fenced broker (handleBrokerFenced): a shrink removes exactly the dead broker and keeps the leader, and a clean election emits exactly that target ISR. It is also checked against the rung ladder of Kafka's PartitionChangeBuilder.electAnyLeader: a clean election takes the first valid replica in assignment order from the target ISR, or with no live ISR member from the first acceptable ELR member in assignment order as a singleton ISR; offset-aware recovery only with no live ISR and no electable ELR member; the KIP-841 election only when additionally the strategy is None and the toggle is on, electing the first acceptable replica; Unavailable only when no rung was open; and no witness ever leads. Properties require the ISR within the replicas, the leader inside its ISR (leader_in_isr), a non-witness leader, and ELR disjoint from ISR. At min.insync.replicas 1, failover_safe, failover_unclean, and failover_recover each reach exactly 525 unique states and the three witness variants 210. At min.insync.replicas 2, failover_elr_unclean reaches 1,470, failover_elr_recover 1,246, and failover_witness_elr_unclean 532, each witnessing a published ELR and an election taken from it. The winner-selection half (offset_recovery) runs select_leader over every response fan-out for each of the 16 published-ELR and witness combinations, 6,859 unique states each. All counts are pinned in leader_failover_model/runner.rs, below the depth-80 and 200,000-state guards. Logs, and so the completeness of an elected replica, are outside this model; data_path_model checks that.

The broker catalog's own description of this model, reproduced from its verification document.

The reassignment model (reassignment_model) drives the production KIP-455 completion step reassign_one, and through it the proved reassignment_action, for one partition with leader epochs through 10. It explores every interleaving of an adding replica joining the ISR, broker death and revival, and completion ticks. A transition check requires every decision to come only after every adding replica is in the ISR; a handoff to move leadership to an alive, in-ISR target replica that is not being removed, keep the replica sets, and bump the leader epoch by exactly one; and a completion to install exactly the target replica set, which still contains the leader. Properties require the ISR, the leader, and the adding and removing sets inside the replica set, and the leader inside the ISR; witnesses cover a completion, a handoff, and a wait. reassign_basic (replicas 1 to 3, add 3, remove 2, leader 1), reassign_leader_handoff (the same change with the removed replica 2 as leader), and reassign_wide (five replicas, add two, remove two, leader removed) reach exactly 21, 42, and 310 unique states, pinned by PINNED_UNIQUE_STATES_BASIC, PINNED_UNIQUE_STATES_LEADER_HANDOFF, and PINNED_UNIQUE_STATES_WIDE, below the depth-80 and 200,000-state guards. Catch-up is an explicit action rather than a replicated log; the AlterPartitionReassignments planner and controller submission remain outside the model.

The broker catalog's own description of this model, reproduced from its verification document.

The stretch-cluster model (stretch_cluster_model) checks KFC-2's witness claim over three sites with one broker each, replication.factor 3, min.insync.replicas 2, a witness replica in the third site, leader epochs through 6, and at most two sites down or isolated at once. It builds the replica list with the production stretch_replicas, takes every failover decision with failover_one and every KIP-460 preferred election with select_new_leader_for_partition, and takes its durability arithmetic from the proved krabka_verified::stretch kernels; ISR rejoin after a site heals and the two acks=all gates of the Produce handler are modeled. Properties require that a witness never leads, that an acks=all produce commits whenever at most one site is impaired and the controller has converged, that every leader change carries a strictly greater epoch, that a site set without a voter majority never commits, and that a preferred election keeps the leader in the preferred site whenever that site holds an alive, in-sync, non-witness replica. Five witnesses include a failover that keeps the witness in the ISR. The run reaches exactly 1,596 unique states, pinned by PINNED_UNIQUE_STATES_THREE_SITES, below the depth-60 and 200,000-state guards. Two #[should_panic] RED configs must fail: the pre-witness controller (legacy_elect, 5,724 states) breaks leader_never_witness, and min.insync.replicas 1 (2,660 states) breaks minority_never_commits. The controller may decide in every state, including states without a metadata quorum, which over-approximates the reachable set; KRaft itself, logs, and I/O remain outside the model.

The broker catalog's own description of this model, reproduced from its verification document.

The diskless crash model (diskless_crash_model) composes the diskless WAL design's crash-window recovery rules with the distributed WAL quorum rule and stateless appenders. Three production kernels decide the steps that carry its properties: consensus::majority_watermark computes the quorum-durable frontier from the live WAL members; offset_allocator::wal_reservation_frontier folds the pending reservation chain and offset_allocator::reserve_offsets places the next reservation, as the controller's V1PartitionOffsetAdvance submit path does, and either kernel refusing fails the run; and diskless::diskless_trim_decision places every trim, as the flusher does. It checks offsets through two, two appenders, three WAL members with at most one lost, sequencer epochs through two, and every reachable ordering of reservation, fsync, crash-before-fsync, crash-mid-fsync, object PUT, index commit, trim, member loss, and sequencer handoff. The run reaches exactly 6,341 unique states at depth 15, pinned by PINNED_UNIQUE_STATES in the model file, below its depth-24 and 100,000-state truncation guards. The safety properties require the quorum-acknowledged and producer-acknowledged frontiers to survive a minority WAL loss, a sequencer handoff never to lower the quorum-durable frontier, every trim to stay at or below both the committed index frontier and the quorum-durable frontier, and the reservations to be gap-free and unique. Reachability witnesses cover a crash between reservation and fsync, a PUT before its index commit, a torn fsync, a trim at the index frontier, a minority WAL loss with acknowledged unflushed records, two appenders interleaving, and a handoff that lowers only the advertised watermark. WAL members, fsync, PUT, and index commit are counters, not logs or objects; every reservation stays pending (the image frontier is 0); the trim runs with no safety lag against the durable frontier as the high watermark. The idempotent-producer dedup rebuild is not modeled; diskless::recovery's unit tests rebuild the dedup state from a real recovered log instead.

The broker catalog's own description of this model, reproduced from its verification document.

The client-server failover model (client_server_failover_model) composes a producer client's failover routing and retry bookkeeping with the production idempotent-producer check check_pure. It checks three brokers, one producer identity with one batch, logs of at most one batch, a high watermark through 1, at most four send attempts and four metadata refreshes, and every interleaving of send, retry, replication, high-watermark advance, acknowledgement, leader death, clean election, and metadata refresh. Election is modeled: only a live follower that holds the committed prefix can become leader. Eleven always properties require that an acknowledged batch is committed and stays durable, that no log holds the batch twice, that a reroute never skips a sequence, that a NOT_LEADER_OR_FOLLOWER before append keeps the sequence, that an appended but unacknowledged batch is never reported acknowledged, that a timeout with an unknown result records the acceptance, that every leader holds the committed prefix, and that the attempt and refresh caps hold. Ten witnesses cover each response kind, a duplicate answered after an unknown result, retries across a failover, and an acknowledgement that survives a clean failover. The run reaches exactly 38,131 unique states, pinned by PINNED_UNIQUE_STATES in its runner, below the depth-36 and 120,000-state guards. The wire client, transactions, and unclean election remain outside the model.

The broker catalog's own description of this model, reproduced from its verification document.

The quorum WAL model (model.rs) drives the in-process three-replica harness -- the #[cfg(test)] WalShardEngine::new, the local-replica branch of replicate_and_sync, and OpenMode::Recover -- over real Log instances: record-batch append, replica sync with byte verification of each replica's whole retained log, acknowledgement and watermark advancement, and byte-agreement recovery, truncation, and repair. It does not drive the production diskless path, where remote voters fetch the leader's tail and report fsynced offsets (record_follower_ack, serve_fetch); unit tests cover that path. It checks three voters, at most two one-record batches, leader epochs 0 through 2, and every ordering of up to eight enabled operations. The run reaches exactly 2,996 unique states at depth 9, pinned by PINNED_UNIQUE_STATES in the model file, below its depth-10 and 20,000-state truncation guards. The safety properties keep the watermark inside the leader log, preserve every previously committed prefix across transitions, and require a byte-identical quorum at the committed frontier. Every acknowledgement is checked against its rule: it succeeds exactly when at least two live voters hold no record that disagrees with the leader's log. Every recovery must succeed; an OpenMode::Recover error fails the run instead of pruning the transition. Reachability witnesses cover successful acknowledgements, a failed acknowledgement with a live minority, a failed acknowledgement with a live but divergent majority, leader changes, divergent replicas, and a completed recovery. KRaft epoch monotonicity and leader completeness are modeled preconditions: Elect(v) is enabled only when the current leader is down and v is live and holds the whole acknowledged prefix, which KIP-595's vote rule and quorum intersection guarantee in production. Appends come only from the current leader; a deposed leader's append is fenced by the registry's epoch check outside the engine and is not enumerated. Successful filesystem calls are atomic operation boundaries; allocation, fsync, and crash atomicity below those calls remain I/O assumptions.

The broker catalog's own description of this model, reproduced from its verification document.

The classic group model (classic_state_model) wraps the production ClassicGroup and drives its add_member, remove_member, complete_rebalance, install_assignments, and expire_dead_members, plus the JoinGroup handler's KIP-345 fence pre-check current_member_id_for_instance. It explores every interleaving of dynamic, static, and fenced joins, heartbeats, leaves, rebalance completion, sync, and session-timeout expiry over a logical clock, and checks that a member, static or dynamic, expires exactly when it is past its session timeout. Properties require a coherent static-member index, one live owner for each group.instance.id, only current members in the members joined this round, and an empty member set exactly in the Empty state; witnesses cover a stable group, a pinned static instance, two members, and a generation bump. The basic config (two members, one instance ID, clock through 4) and the wide config (three members, two instance IDs, clock through 5) reach exactly 3,853 and 482,874 unique states, pinned by PINNED_UNIQUE_STATES_BASIC and PINNED_UNIQUE_STATES_WIDE, below the depth-80, 8,000,000-generated, and 600,000-unique guards. A proptest companion drives the same operations over random schedules. Wire decoding, the offsets log, and the actor mailbox remain outside the model.

The broker catalog's own description of this model, reproduced from its verification document.

The consumer-group composition model (consumer_group_composition_model) reuses the reconciliation model's driving of step_heartbeat and composes it with the production OffsetCommit fence GroupState::validate_offset_commit, including the KIP-1251 per-partition assignment-epoch check. Every commit cross-checks the fence against an independent oracle of the expected epoch comparison, partition assignment epoch and error code, so a divergence fails the run. Properties require that no two members own one partition and that no member is advertised a partition another member still owns; witnesses cover an accepted commit, a member-epoch bump that fences a commit from before a rebalance, a partition held from an epoch older than the member epoch, and a handoff. The basic config (two members, two partitions, epochs through 7) and the wide config (three members, two partitions, epochs through 6) reach exactly 6,328 and 29,647 unique states, pinned by PINNED_UNIQUE_STATES_BASIC and PINNED_UNIQUE_STATES_WIDE, below the depth-80 and 2,000,000-state guards. Plain consumer groups deliver at least once, so no-duplicate and no-gap delivery are deliberately not checked; __consumer_offsets persistence and the classic protocol are out of scope.

The broker catalog's own description of this model, reproduced from its verification document.

The KIP-848 reconciliation model (reconciler_model) drives the production step_heartbeat, and through it GroupState::reconcile_member and the default uniform assignor, over join, leave, and heartbeat actions and a faithful client. The client adds and revokes partitions strictly by the assignment the coordinator returned in that member's last heartbeat, revokes before it adds, and makes no cross-member check, as a real consumer does, so exclusivity must come from the coordinator's withholding alone. Properties require that no two members own one partition at the same time and that no member is advertised a partition another member still owns; witnesses cover a handoff and convergence. The basic config (two members, two partitions, epochs through 9) and the wide config (three members, two partitions, epochs through 7) reach exactly 552 and 3,813 unique states, pinned by PINNED_UNIQUE_STATES_BASIC and PINNED_UNIQUE_STATES_WIDE, below the depth-60 and 200,000-state guards. Offset commits, the offsets log, and the wire protocol remain outside the model.

The broker catalog's own description of this model, reproduced from its verification document.

The coordinator replay model drives the production replay_mutation and replay_epoch_is_admissible decisions used by the consumer, share, and streams adapters. It checks one group, two members, every group, member, assignment, topology, partition-metadata, and share-state record class, epochs -1, 0, 1, and i32::MAX, exact retries, mismatched value kinds, and every reachable log ordering. The run reaches exactly 6,376 unique states and converges at depth 14, pinned by PINNED_UNIQUE_STATES in the model file, below its depth-40 and two-million-state truncation guards. Properties require key/value kind agreement, parent-before-child application, nonnegative monotonic epochs, assignment ownership by a present member, and whole-group tombstone dominance until a later group-metadata write. Reachability witnesses cover a group created by a child record, an ignored tombstone for an absent group, a load that fails on an out-of-order tombstone, malformed type binding, stale-epoch suppression, i32::MAX, and member assignment replay. The bootstrap adapter decodes a value before publishing its group-type lock; malformed values return an error without state. As in Kafka's GroupMetadataManager.replay, a child record creates its missing group, a tombstone for a group the log does not hold is ignored, and an out-of-order tombstone fails the load. A member tombstone also removes its target and current assignments. A target-metadata tombstone removes its targets. The outer replay walk supplies record order and bounded cursors through replay_batch_cursor_decision. Key parsing, schema decoding, transaction-marker interpretation, log reads, compaction, cache allocation, actor seeding, and process-crash atomicity remain host or I/O assumptions.

The broker catalog's own description of this model, reproduced from its verification document.

The streams-group reconciliation model drives the production StreamsGroupState membership, timeout, target-installation, and cooperative active-task transitions; the production streams assignor; the port of Kafka's CurrentAssignmentBuilder through StreamsGroupState::reconcile_member; the shared member-epoch fence; and the production snapshot/apply replay adapters. It exhaustively checks two member IDs, one subtopology with one or two tasks, three logical timeout ticks, topology epochs through two, group epochs through six (five bumps from the initial epoch 1), and one crash/replay in every reachable ordering. The run reaches exactly 37,960 unique states, pinned by PINNED_UNIQUE_STATES in the model file, below its depth-64 and one-million-state truncation guards. A task pending revocation counts as still owned, so the properties require exclusive current and target active-task ownership, topology-valid assignments, nonnegative fenced epochs, coherent group phases, and exact durable replay projection. Reachability witnesses cover unknown-member, stale, and forward heartbeat rejection; timeout; topology growth; replay; withheld ownership; release; and two-member membership. Request decoding, actor mailbox delivery, offsets-log append durability, cache publication, wall-clock scheduling, metadata-source snapshots, and internal-topic I/O remain outside the model. Adapter tests cover malformed reports, epoch exhaustion, retry, stale and forward epochs, and failed log appends. A failed append returns COORDINATOR_LOAD_IN_PROGRESS, publishes no partial batch, and leaves recovery to durable replay after the actor restarts.

The broker catalog's own description of this model, reproduced from its verification document.

The EndTxn decision model (decision_model) runs one transactional id through every interleaving of an EndTxn split at its marker window (Phase 1, then Phase 3 after the lock is released for the fan-out), InitProducerId naming no identity, AddPartitionsToTxn, and the completion task. It drives decide_phase1_transition, prepare_completion_identities_with_fresh, completion_producer_identity, decide_end_txn_completion, the Prepare* gate of pending_completion_response (completion_for), the verified next_producer_identity bump, prepare_server_abort_identities_with_fresh for the fence of an Ongoing transaction (the function the InitProducerId handler and the reaper prepare that abort with), and the completion task's completion_for, completion_decision and apply_completion. The PrepareAbort state of that fence and the handler's state table are modeled, and the KIP-360 identity classification and keepPreparedTxn recovery are not exercised. The fence runs at TV_2 and below it. Up to producer epoch 3 and 6 the search visits exactly 231 and 7,744 unique states at depth 11 and 20 at either version, pinned by PINNED_UNIQUE_STATES_BASIC and PINNED_UNIQUE_STATES_WIDE. always properties require that an EndTxn whose Phase 3 finds the entry no longer at its prepared identity, state and generation never writes Complete*; that each generation finalizes at most once, so never both committed and aborted; that InitProducerId never moves a Prepare* transaction (Kafka's CONCURRENT_TRANSACTIONS); that the fence raises the epoch once and records the last epoch and the transaction version Kafka records at the cluster's version; that Phase 3 rejects only an entry that moved; and that the epoch never regresses. Witnesses show a commit, an abort, and a producer overtaken inside the marker window -- reached only through legal transitions: the completion task finishes the prepared transaction and a later InitProducerId or transaction moves the entry on. A table test pins InitProducerId's outcome from every state.

The broker catalog's own description of this model, reproduced from its verification document.

The exactly-once read composition (eos_composition_model) runs two transactional producers and an advancing high watermark over one partition. It drives the EndTxn cores on their Proceed path and the production compute_visibility_window; the LSO rule and the abort filter of visible() are modeled. Properties are checked against oracles derived by producer and control marker, never by the generation tags the model's own lso() and filter read: window_is_min_lso_hw requires the real window to equal min(first unstable offset, hw), committed_prefix_complete requires every committed record below that window to be visible, nothing_visible_above_hw bounds the visible set by the HWM, and no_visible_aborted excludes every offset in an aborted range as Kafka's aborted-transaction index derives it from the Abort markers. only_committed_visible requires every visible record to be committed; ghost flags fail no_transition_violation if the HWM or LSO regresses or an End does not Proceed. The two configurations (one and two generations per producer, logs of 5 and 7 batches) visit exactly 1,228 and 58,524 unique states at depth 13 and 19, pinned by PINNED_UNIQUE_STATES_BASIC and PINNED_UNIQUE_STATES_WIDE. Witnesses show a visible commit, a filtered abort, a commit held back behind an older open transaction, and the HWM clamp active.

The broker catalog's own description of this model, reproduced from its verification document.

The KIP-939 timeout model (two_pc_model) runs one transactional id through InitProducerId with and without enable2Pc and with requested timeouts 1, 60000, 900000 (= transaction.max.timeout.ms), 900001 and 0, AddPartitionsToTxn, EndTxn, completion, the idle reaper, and a monotonic clock over 0, 1, 2, 60000, 60001, 900000, 900001, i32::MAX, i32::MAX + 1, i64::MAX, so a transaction opened at 0 meets every timeout's start + timeout and start + timeout + 1. It drives resolve_txn_timeout, should_abort_idle_txn, decide_phase1_transition, prepare_completion_identities_with_fresh, prepare_server_abort_identities_with_fresh (the abort of the reaper and the InitProducerId fence), completion_for, completion_decision, apply_completion, completion_producer_identity and the verified next_producer_identity; the PrepareAbort state of apply_prepare_abort and of the fence, and the start_ms stamp, are modeled, and each Prepare* completes atomically. The cluster's transaction version is TV_2 or below it. Up to producer epoch 3 and 5 the search visits exactly 21,876 and 80,914 unique states at depth 20 and 22 at either version, pinned by PINNED_UNIQUE_STATES_BASIC and PINNED_UNIQUE_STATES_WIDE. A property requires that the abort of an Ongoing transaction raises the epoch once and records the last epoch and transaction version Kafka records at the cluster's version. The headline two_pc_never_reaped keys on the request's enable2Pc flag, not the persisted timeout, so a wrong encoding fails it. reaper_never_early and reaper_never_misses compare every sweep with Kafka's timedOutTransactions rule restated from the request (Ongoing, not 2PC, start + requested < now in exact arithmetic). Generations finalize in strictly increasing order, and the epoch never regresses. Witnesses show a classic reap, a reap exactly one millisecond past the timeout, a sweep that spares a transaction exactly at its timeout, a 2PC transaction open past start + i32::MAX, and a commit.

The broker catalog's own description of this model, reproduced from its verification document.

The share-group membership model (share_group_model) drives the production ShareGroupState join, leave, and timeout transitions; the production assignment reconciler and share assignor; the shared member-epoch fence; and the production snapshot/apply replay adapters. It exhaustively checks two member IDs, one topic with one or two partitions, four logical timeout ticks, epochs through six (five bumps from the initial epoch 1), and one crash/replay in every reachable ordering. A stale heartbeat sends the member epoch minus one, which Kafka accepts when it is the previous member epoch or 0 (a rejoin) and fences otherwise. The run reaches exactly 54,860 unique states, pinned by PINNED_UNIQUE_STATES in the model file, below its depth-64 and one-million-state truncation guards. Properties require unique (member, topic, partition) coordinates, bounded assignments for members at the target epoch, nonnegative fenced epochs, and exact durable replay projection; reachability witnesses cover unknown-member, stale, and forward heartbeat rejection, timeout, metadata reassignment, replay, and two-member membership. Cross-member partition overlap remains intentional KIP-932 behavior when members outnumber partitions. Request decoding, actor mailbox delivery, offsets-log append durability, cache publication, wall-clock scheduling, metadata snapshot consistency, and share-state persister I/O remain outside the model. A failed offsets-log append is covered by an adapter test: the actor returns COORDINATOR_LOAD_IN_PROGRESS, publishes no partial batch, and relies on durable replay after restart.

The broker catalog's own description of this model, reproduced from its verification document.

The share-partition model (share_partition/state_model) holds the production KIP-932 AcquisitionState and drives its materialize, acquire, acknowledge, renew, expire_locks, defer_internal, promote_deferred, to_persist_batches, and load_from over every interleaving of consumer operations, time advance, KFC-1 deferral, a leader reload through the persisted batches, and a log-start advance. Deferral is over-approximated: any offset can be deferred at any point, which covers every deferral a log and a clock could produce. Properties require a sorted, gap-free window that exactly covers [start_offset, end_offset), exactly one owner for every acquired batch (so no offset is held by two members), lock bookkeeping that matches the delivery state, a bounded delivery count, and the share-partition start offset inside its range, plus the log-start and deferral properties in the configs that enable those actions. A transition check requires a nondecreasing start offset and delivery count, keeps an acknowledged offset terminal, and leaves promote_deferred as the only route out of Deferred. Two-member concurrency over three offsets with an in-flight limit of 3, or a record lock limit of 2, reaches exactly 7,969 or 1,521 unique states; failover with reload reaches 623; deferral over the failover window 1,118; one-member deferral over three offsets 5,012; and log-start advance with reload 6,477. Each count is pinned by its PINNED_UNIQUE_STATES_* constant in the runner, below the depth-80 and 200,000-state guards. The share-state persister, the fetch path, and wall-clock time remain outside the model.

The broker catalog's own description of this model, reproduced from its verification document.

The break-glass lifecycle model (break_glass/state_model) drives one proposal through every interleaving of approve, withdraw, expire, and consume over a small set of principals and a logical clock that expires the proposal at 2 ms. Each transition builds a BreakGlassProposalRecord from the state and calls the production approve::decide for an approval or withdrawal and gate::authorize for a consume, against a real MetadataImage. Properties require that no interleaving consumes the proposal twice, that none consumes it with fewer than required_approvals distinct approvers, and that a withdrawn proposal is never consumed; witnesses cover a consume, a withdrawal, an expiry, full approval, and a fully approved proposal that expired unspent. The two-of-three-approvers config, whose principals include the proposer, who cannot approve, and one principal outside the approver set, and the three-of-four config reach exactly 36 and 114 unique states, pinned by PINNED_UNIQUE_STATES_TWO_OF_THREE and PINNED_UNIQUE_STATES_THREE_OF_FOUR, below the depth-20 and 200,000-unique guards. Signature verification, controller submission, and metadata durability remain outside the model.

The broker catalog's own description of this model, reproduced from its verification document.

The break-glass cross-spend model (break_glass/cross_spend_model) puts two open proposals in one MetadataImage and runs every interleaving of approve, withdraw, expire, and consume against them, with the same production approve::decide and gate::authorize calls and the same clock bound as the lifecycle model. Each request carries a hand-written covered_by set, taken from KFC-9's target-matching rule rather than from the broker's own covers, so the headline property is not a tautology. Properties require that no proposal is spent on a request it does not cover (no_cross_spend), that each proposal is spent at most once, that no spend is under-approved, and that a withdrawn proposal is never consumed; witnesses cover each proposal spent, both spent, and one approved while the other is requested. Three configs, one action on two topics, a topic that looks like a partition of another, and two proposals that both cover one partition, each reach exactly 432 unique states, pinned by PINNED_UNIQUE_STATES_TWO_TOPICS, PINNED_UNIQUE_STATES_PARTITION_LOOKALIKE, and PINNED_UNIQUE_STATES_BOTH_COVER, below the depth-12 and 1,000,000-unique guards. Removing the partition-target limit from gate::covers fails only the lookalike config, and removing the consumed check fails all three. no_under_approved is a guard here, not an independent check, because approve::decide already refuses a second approval from one principal.

The broker catalog's own description of this model, reproduced from its verification document.

The compaction model (compact_model) runs one pass of a cleaner over an abstract log per Compact step, the production should_index_key and retain_decision by default, and records the log the pass consumed in the next state. Five always properties check each pass's output against its input with rules computed from the two logs alone: control-not-deduped (a marker whose horizon has not elapsed survives), marker-data-precedence (a marker survives while the pass reads data of its own transaction in front of it, as Kafka decides per transaction rather than per producer), tombstone-aging (no elapsed tombstone survives; an unexpired newest tombstone does), idempotent-stamp (the output is the input with deletions and None -> now + delete.retention.ms stamps only), and no-data-loss (the set of keys with a live newest value is unchanged). The basic run (logs up to 4 entries) and the wide run (up to 5) reach exactly 144,128 and 1,102,770 unique states, pinned by PINNED_UNIQUE_STATES_BASIC and PINNED_UNIQUE_STATES_WIDE in compact_model/runner.rs, below the depth-40 and 1,500,000-unique guards. The legacy cleaner, which indexes control keys and dedups markers by them, is run through the same pass and checker, which reports exactly control-not-deduped and marker-data-precedence as broken, with the recorded five-action counterexample.

The broker catalog's own description of this model, reproduced from its verification document.

The leader-epoch reconciliation model drives the production epoch_and_offset_for_entries lookup on both sides of a fetch and the production checkpoint truncation (truncate_to), with Kafka's LeaderEpochFileCache.assign, Partition.readRecords divergence gate, and AbstractFetcherThread.getOffsetTruncationState follower rules as the environment. Replicas hold logs of per-offset leader epochs; elections are clean or unclean, and the new leader assigns its epoch at its log end. The reconciliation_two_replicas config (two replicas, epochs through 5, three records per leader log) reaches exactly 35,274 unique states, and reconciliation_three_replicas (three replicas, epochs through 3, two records) exactly 20,212, pinned by PINNED_UNIQUE_STATES_TWO and PINNED_UNIQUE_STATES_THREE in leader_epoch_model, below its depth-64 and two-million-state truncation guards. Properties require a follower the leader has accepted to be a prefix of the leader's log, no truncation to drop a record the follower shares with the leader, every diverging_epoch to change the follower (no livelock), the leader never to answer OFFSET_OUT_OF_RANGE, and every checkpoint to stay strictly increasing. Reachability witnesses cover a divergent suffix really truncated, a gap epoch resolved to the leader's floor epoch, a KIP-279 step-back round, and full convergence after a divergence. A third config (two replicas, epochs through 4, three records; 10,865 unique states, PINNED_UNIQUE_STATES_NO_ASSIGN) drops assign-at-election and must find a counterexample to leader_places_every_follower_epoch while the safety properties still hold: without it a newly elected leader that has not written cannot place a follower's newer epoch. The broker assigns the epoch at promotion, as Partition::install_local_leadership records it at the log end, so the first two configs describe production and the third is the regression the assignment prevents. Replacing the gap branch's floor epoch with the requested epoch fails the proptest driver described next. A proptest driver runs the same step function over random 400-step schedules on four replicas. Log start above 0, tiered storage, the below-log-start OFFSET_OUT_OF_RANGE, the follower's ListOffsets-based out-of-range recovery, wire encoding, and I/O remain outside the model.

The broker catalog's own description of this model, reproduced from its verification document.

The KRaft model (kraft_model) runs the production QuorumStateMachine for every node over an unordered network. Replication is the one abstracted exchange: the records a fetch returns are applied when the follower sends it, and only when the leader's log extends the follower's (the high watermark reaches a follower on the same terms). A follower whose log disagrees with the leader's is never overwritten; the production handle_fetch answers its fetch with a diverging epoch, the production handle_fetch_response truncates it, fetches again at once from the truncated end, and re-arms the fetch timer, as Kafka's KafkaRaftClient.handleFetchResponse and pollFollowerAsVoter do, and the divergent_log_truncated witness requires that path to run in both crash configs. Its three_voters_append config checks leader completeness under a stale majority: three voters, one client append, leader epochs through two, at most two in-flight messages, and at most one crashed node at a time, whose omission model drops that node's traffic and so leaves it behind the committed prefix. The pinned run reaches 839,339 unique states, asserted by PINNED_UNIQUE_STATES_THREE_VOTERS_APPEND, below its depth-60 and 8,000,000-state truncation guards. The leader_completeness property requires every node that believes it leads epoch e to hold each entry committed in an epoch at or below e, stamped with the epoch it committed under. The stale_candidate_refused witness requires a vote refused for log recency alone: the transition that delivers the request also runs a copy of the voter's real machine on the same request with the candidate's log end replaced by the voter's own, and only a refusal that copy grants counts. It would disappear if the config stopped reaching a stale-majority election. Removing the log-recency conjunct from handle_vote_request makes this config fail. The other configs cover election and log-matching safety with three voters and no appends (three_voters_election_safety, 10,750 states), committed-log linearizability with two voters (two_voters_linearizable, 46,521), election safety under message loss, duplication, and one crash at a time (three_voters_faults, 1,128,704), and stateless appenders (two_voters_append_via_linearizable, 256,973), each pinned by its PINNED_UNIQUE_STATES_* constant. Wire encoding, disk durability, wall-clock timing, volatile-state loss on restart, and behavior beyond the stated bounds remain outside the model.

The broker catalog's own description of this model, reproduced from its verification document.

The throttle bucket model drives the production plan_consume cap-and-grant arithmetic at every commit and steps the TokenBucket protocol one shared-memory access at a time: the lock-free rate-mirror read of the unthrottled fast path, the lock acquire, the clock read, the last_refill claim, the available commit, and the release for a consume; the lock acquire, the group store, the mirror publish, and the release for a reset, with a separate burst per configuration. A reset keeps the balance: it refills the old configuration to now, caps the balance at the old and then at the new burst, and starts a bucket that had no rate, or gets none, full. Its bucket_basic config checks two consumers, one reset between bursts 2 and 1, two clock units, and requests up to two; the run reaches exactly 56,259 unique states, pinned by PINNED_UNIQUE_STATES_BASIC. Its bucket_wide config checks two consumers, two resets among (rate 1, burst 3), (2, 1), (0, 0) and (1, 0), two clock units, and requests up to two; the run reaches exactly 372,204 unique states, pinned by PINNED_UNIQUE_STATES_WIDE. Its bucket_fractional config meters two storage units to a token, as production meters micro-tokens, and checks two consumers, one reset from (rate 1, burst 3) to (1, 1), two clock units, and requests up to two whole tokens, so its rates are half a token per second and the second burst holds half a token; the run reaches exactly 33,964 unique states, pinned by PINNED_UNIQUE_STATES_FRACTIONAL. Each commit also drives the production whole-token request cut, whole_token_request. All three stay below the depth-80 and 4,000,000-state truncation guards. Properties require available <= burst and exact token conservation per configuration: available + granted + capped + in-flight claimed refill == base + rate * (last_refill - t0), where base is the balance the reset started the configuration with, so a claimed refill can neither vanish nor be granted twice, and every grant is a whole number of tokens. Reachability witnesses cover overlapping consumers, a reset overlapping a consume, an in-flight claim, a granted and a capped refill, a shrinking reset, a drained bucket, and a reset that keeps a balance under the new burst. Debt is outside the model: try_consume never creates it, and record differs from a consume only in what it does with the part it cannot grant, which it keeps as debt, at most what the refill repays in max_wait for record_bounded; the unit tests in consume.rs cover both. RED witnesses step the former lock-free seqlock design (a generation re-check followed by two compare-and-exchanges) and must find both of its bugs: a whole reset between the generation re-check and the available commit that lets available exceed the new burst, and a failed commit that drops the refill its claim took. Two scripted schedules replay each bug concretely against the seqlock and show that the lock makes the same interleaving impossible. The clock is modeled in whole seconds with rates in whole storage units and memory as sequentially consistent; the part-unit remainder is covered by unit tests in consume.rs.

The broker catalog's own description of this model, reproduced from its verification document.

The audit spool model (spool_model) drives the production spool_append_decision for every spool append, a record's or a loss marker's, the add_loss_state helper behind PendingLosses::add, the settle_loss_batch kernel that PendingLosses::commit and PendingLosses::reconcile apply, and the replay-recovery classifier behind Spool::open. The loss path is PendingLosses as the serial writer drives it: a concurrent AuditHandle::emit loss or a crash can fall between any two of persist_with's steps (snapshot, sidecar write, marker append subject to spool capacity, sync, in-memory commit, commit write), and a poisoned reopen stops before reconciliation as Spool::open does. It checks three record IDs, two loss events, a two-record spool, sync cadence two, and at most two crashes, in every reachable ordering. The run reaches exactly 71,351 unique states, pinned by PINNED_UNIQUE_STATES in the model file, below its depth-64 and 4,000,000-state truncation guards. Properties require every durably admitted record to remain delivered or durably pending, at-most-once automatic delivery, exact loss accounting (every loss is reported by exactly one durable marker, is still pending, or was held only in memory at a crash), distinct marker generations, and every durable marker settled exactly once. Reachability witnesses cover torn append recovery, retry after a definite sink failure, fail-stop poison after an uncertain delivery, cleanup after a committed cursor, a marker refused by a full spool, loss-marker reconciliation after reopen, and a concurrent loss carried past a marker. The test superseded_settlement_loses_and_rereports_losses keeps the settlement that PendingLosses applied before settle_loss_batch, in which a commit left the remainder in the marker's generation and reconciliation zeroed the whole count, and requires the checker to find losses_accounted, marker_generations_unique, and markers_settled_once counterexamples for it. Filesystem and directory-sync semantics, storage hardware, sink durability, explicit operator recovery of poisoned replay, and behavior beyond the stated bounds remain outside the model. Adapter tests cover malformed, missing, stale, and committed poison plus loss-counter saturation.