Verification

krabka uses two formal test tiers. Creusot proves contracts for small, executable kernels. Stateright checks all reachable states inside each model’s stated bounds. Neither tier proves the whole broker.

Development evidence

A human maintainer and AI coding agents codeveloped krabka-broker. The development process does not use authorship as evidence of correctness. Pull requests apply the same build, test, proof, model-check, and compatibility gates to human and AI changes.

An AI-generated test can repeat the implementation’s mistake. krabka therefore uses checks with independent failure signals. Mutation testing inserts faults that the tests must detect. Creusot sends contracts to automated provers, and Stateright explores bounded event orderings. Differential and acceptance suites also run live, digest-pinned Kafka brokers as reference systems.

The checks do not prove the whole broker. This catalog states the formal boundary in detail. The repository README describes the mutation and container tiers. Mutation testing stands in for authorship only while it is actually running, so the sweeps are scheduled weekly per crate and the mutation sweep baseline records the last run in which each swept crate came back with no survivor.

A mutation skip narrows that evidence, so the README’s skipping a mutant rule bounds it. A function-level #[cfg_attr(test, mutants::skip)] is accepted for an I/O-only wrapper with no in-process signal, or for orchestration whose every branch calls into a separately mutation-tested kernel, and it must carry a // cargo-mutants: <reason> line saying which — aspect check-mutants-skip fails the build otherwise. An equivalent mutant of a single expression belongs in .cargo/mutants.toml’s exclude_re instead, so the function’s other mutants stay in the sweep. Integration coverage is explicitly not a reason: the sweep runs unit tests and ordinary tests/*.rs only, so a skip resting on the container suites removes precisely the code this tier would otherwise measure.

Catalog Boundary

This catalog covers safety-critical, deterministic decisions implemented in this repository. These decisions admit, reject, select, fence, order, or recover state in KRaft, storage, security, and protocol handling. A decision belongs in the Creusot ledger when a contract can describe its safety rule. It belongs in the Stateright inventory when the rule depends on a bounded sequence of events, crashes, or interleavings. Host orchestration and external systems remain outside both tiers as described below.

The closure audit enumerated the workspace crates, traced every ledger caller and model entry point to production code, checked its proof artifact or bounded model and adapter tests, and searched the remaining mutation boundaries. Apart from the barrier coordinator partitioner named under Outside Both Tiers, the audit found no unlisted decision inside this boundary. A cross-check of the kernel source against the ledger found every public executable function of krabka-verified in a ledger row, and every kernel that a row names in the source. The tables below are the authoritative inventory; counts are not used because one row can contain several related kernels.

Every pull request runs the Creusot package-discovery check and all discovered proof-bearing packages. The same CI workflow explicitly runs the five Bazel test targets that contain every Stateright entry point in this inventory. The explicit run is separate from impact-based test selection, so an unrelated change cannot skip the model checks. A new proof-bearing package must pass the discovery check. A new Stateright entry point must be added to this inventory and to one of the explicit model-bearing targets, or that target list must be extended.

Creusot Proof Ledger

The contract audit critiques every original proof module, distinguishes decision-table contracts from aggregate invariants, and records the remaining host assumptions. A proved implication about admission does not establish that valid requests are accepted; admission-completeness contracts must also rule out rejecting everything.

Cross-module theorems

The proof/test-only composition module calls the existing kernels through their contracts and checks relationships across module boundaries. All compositions export usable relational guarantees or witnesses. A historical control replacing all fifteen then-remaining bodies with true proved those files and passed all composition tests. Append, reservation, audit-loss settlement, scheduled delivery and read-committed Fetch compositions now return actual computed witnesses, with exact admission and relational contracts plus independent oracles. The audit records the historical weakness and repairs. The preceding thirteen-entry control proved all affected files and passed all 53 then-existing composition tests; read-committed Fetch has since been repaired. The twelve-entry checkpoint control proved all twelve replacements and passed all 57 composition tests; audit-loss settlement has since been repaired and consumed by marker admission. Scheduled delivery now exports its greatest frontier to a transaction-stability consumer proving the greatest prefix allowed by both gates and HWM; inherited delivery/LSO values cannot replace those derived frontiers. Placement now exports actual voter identities and installer admission into the exact rack-loss survivor witness, which proves capacity for the original majority after one rack loss. Offset-index validation exports exact byte cursors to a complete-batch seek composition proving the indexed scan finds the same first match as a full scan; structural row validity alone cannot establish truthful batch positions. Validated epoch reconciliation exports its actual cut to retained snapshot selection and replay; neither discarded-tail snapshots nor invented earlier floors can suppress reconstruction. Constructed sparse rows now export attained prefix maxima into retained-record selection and then cross-tier ListOffsets visibility; a pruned match cannot suppress a later retained one. Validated remote and local time scans now export actual cursors into a consumer that checks prefix bounds against decoded records and returns the first retained match. Completed logical trim now supplies the read floor independently of producer replay progress; physical eviction supplies the cache frontier used to reroute the same retained match to committed remote coverage. Validated time cursors now compose with constructed prefix maxima into complete closed-interval scans; equal maxima require a strict lower start, and later regressions prevent using the upper cursor to bound the scan tail. The derived transaction/HW/delivery offset prefix now gates this interval scan, preserving the first retained match strictly below its maximal limit while ignoring inherited LSO. A minimum-equivalent transaction projection preserves visibility but cannot validate omitted entries. Remote interval coverage now derives whole-segment blocking for local retention and composes with the size/time prefix and checked deletion successor. Its target bounds every offset selected for eviction by an actual supplied remote interval, including gaps between local segments. An independent progress guarantee selects every unblocked prefix eligible by size or expiry, including their mixed handoff. Independent prefix-byte bounds justify each selected non-expired row, excluding paired selectors and reference models that skip the size pass or ignore its debt. Selected segments remain covered at successor exhaustion. Complete truthful metadata and durable physical deletion remain external. Witness-returning compositions carry their aggregate guarantees in the exported contracts. The connections are: allocation, append, acknowledgement, recovery, and scan frontiers agree; sequential reservations are adjacent and disjoint; consuming both frontier contracts makes successive batches recover and acknowledge strictly in order; transaction-derived LSO returns the greatest read-committed prefix bounded by every unstable start, HW and delivery, and that prefix determines the complete remote/local abort-row union; a newly advanced consensus HWM gives the Fetch limit quorum support; archived offset-index row validation establishes global ordering and bounded floor/ceiling lookups; and replaying an audit settlement returns the exact conserved pending state before generation exhaustion; its witness and marker admission preserve concurrent losses, reject duplicate admission and permit the fresh remainder marker; restored time-index cursors are monotone and remain within their segment; validated epoch reconciliation cuts bound truncated consumer Fetch; snapshot selection after truncation yields a replay cursor inside the surviving log; narrowing Fetch returns witnesses for exactly all overlapping restored aborts; remote/local source union preserves every qualifying wire abort row exactly once; the actual maximum activation time is due exactly when every batch is due; that aggregate theorem composes with a complete batch walk, delivery watermark, and Fetch cap to hide waiting batches while replication remains ungated; replica fencing, append/truncation, and HWM advancement preserve bounded Fetch; and restored record selection respects batch spans and agrees with whole-batch classification; actual prefix maxima construct sparse time-index rows; strict predecessor scanning returns the global first matching record; and arbitrary sparse-index construction agrees with a full scan even with timestamp regressions and offset gaps; remote candidate selection preserves the same first-record result with padding and unsorted conservative bounds; and validated remote and local scan starts agree; completed trim steps converge without frontier regression; admitted trim reconciliation preserves its caps, makes retry a no-op, and bounds snapshot reload cursors; and diskless eviction reconciliation preserves committed object coverage and HWM safety lag; the full WAL placement fold establishes the quorum installer’s distinct identity invariant; and a complete placement of at least three voters retains a majority after one configured rack fails; installed voter validation, explicit durable votes, quorum advancement, and consumer Fetch produce a concrete majority of distinct supporting nodes whenever an advance exposes retained records. The unsynced leader end is excluded as an extra vote. Watermark maximality and the exact HWM/LSO/delivery minimum exclude stalled advancement or an artificially empty Fetch. The proved explicit-vote count equivalence lemma connects the host’s offset clamp to the same count model; floor-only/inherited-watermark cases remain explicit. Checking actual copied batch bytes also composes with live append, Produce acknowledgement, and recovery over an arbitrary-length prefix: logical frontiers agree, byte progress equals the actual encoded lengths, and complete valid copies that fit their file extent cannot be rejected wholesale. Checkpoint admission also composes with whole-batch truncation and exact Fetch clamping, preserving valid interior floors and treating empty recovery as a reset. Covering-read validation and the trim planner then connect physical copying to logical Fetch: every offset in the retained window has a concrete copied batch with identical bytes, and every offset before either floor is excluded. Promotion checkpoints a higher canonical floor in the follower before rebasing; an injected first-append failure and reopen regression checks that ordering. The byte-quorum composition connects identity/epoch admission, validated actual WAL copies, observed durable completion, installed identities, explicit quorum votes and consumer Fetch. A fresh advance above the retained floor exports a distinct matching-copy majority; complete valid copies must reach log end. The canonical reference is validated through the covering-copy theorem, including an interior logical floor. That theorem and its layout validator now export arbitrary batch order and checked extents; WAL authorization and byte-count definitions are available to crate-local proof consumers. Independent sorted-ledger tests and consistent wrong-helper contracts reject mismatched or unfinished copies. Accurate decoded bytes, current lineage, actual fsync/checkpoint completion, identity provenance and inherited watermark evidence remain host obligations. The network leader continues to trust authenticated offset reports; the model consumes inspected copy evidence and does not prove that authentication makes those reports true.

The append/reservation witness composition returns the actual computed append, reservation, recovery, acknowledgement and scan results with exact admission and equality guarantees. Its pair consumer calls those exported contracts to establish adjacent non-overlapping batch ranges and strictly increasing acknowledgement frontiers. No batch bytes, controller serialization or fsync/quorum completion are inferred from the coordinate witnesses. Complete transaction-index admission now returns the original selected row indices, with exact overlap membership and invalid-index rejection. The abort-source union composition joins those witnesses to inclusive remote overlap, half-open local selection, Fetch visibility, and the production wire-row deduplicator. It proves that every qualifying pair from either supplied source survives exactly once, even when the marker owner lies beyond the data window. The derived-stability composition first obtains actual LSO and Fetch witnesses from the transaction-state composition. It replaces the inherited scalar LSO before selecting abort rows, so the same maximum prefix bounded by every unstable start, HW, delivery and the requested cut determines all qualifying unique rows from both indexes. Complete or minimum-equivalent transaction projection, coherent lineage, index enumeration, requested-floor authorization, bytes and client filtering remain host obligations. RemoteReader therefore scans later finished indexes; remote Fetch also merges local index rows. The native archive/eviction regression checks remote-only, local-only and duplicated markers. Complete current-lineage enumeration, truthful objects, coherent frontiers, and client-side record/control filtering remain external. Exact restore selection now returns original row indices and a complete archived frontier instead of a success flag. The filtered-restore retry composition connects those witnesses to actual rewrite-header/record admission, modulo producer sequence arithmetic and snapshot retry reconstruction. Its returned coordinates name every qualifying original record exactly once in source order. The original retry sequence and acknowledgement frontier survive both partial and empty rewrites, including wrap. The materializer keeps the original offset span independently of survivor count; a native encoded restore/reopen fixture checks recovered producer metadata and retry classification. This projects one admitted last non-transactional data batch, with truthful ordered decoded rows; encoding, snapshot durability, complete replay and PID routing remain external. Actual control-key classification then composes with matching-producer closure, abort intervals, strict marker/HWM release, and the maximal read-committed Fetch prefix. Replicated control batches share native append’s semantic bookkeeping while retaining their original wire bytes; the promotion regression compares transaction and producer state before and after reopen. The marker-admission composition connects the production transaction-version fence and producer/coordinator generation admission to that same control-marker pipeline. Rejected pending markers preserve the previous Fetch limit and produce no abort interval. Admitted markers retain their unstable start until HW passes the marker’s last offset; afterward the prefix is maximal under all remaining starts and caps, and strictly advances when no competing start or delivery cap blocks it. COMMIT publishes offsets only on the offsets partition; ABORT returns its exact interval and never publishes offsets. Complete PID-keyed pending state, serialized application, successful durable append and actual offset publication remain host obligations. A completed trim now syncs retained bytes and publishes its WAL range before native prefix removal or log-floor advancement. The publication-stage composition then connects each old/new checkpoint to whole-batch recovery and exact Fetch membership, including partial native floor advancement and a previously uncheckpointed tail. A 24-case fault table checks the actual adapter. Snapshot admission also composes with modulo-2^31 sequence reconstruction, retained-batch retry classification, append coordinates, and acknowledgement frontiers. For a snapshot-only reload, a same-epoch retry names the original last batch and offset; older epochs fence and the successor sequence appends. A real snapshot write/reopen test exercises that broker projection, including sequence wraparound. PID lookup and decoding remain host obligations. The truncation/snapshot composition now returns the selection and replay cursor as witnesses. Its contracts state newest-survivor completeness and the exact replay cursor, so bounds alone cannot justify losing a valid snapshot or skipping the replayed tail. Corrupt-snapshot fallback also composes with newest selection and exact replay construction. It preserves original candidate identities across removals, skips only corruption, stops on read I/O failure, and returns the exact fallback cursor when no non-corrupt survivor exists. Read classifications and directory effects remain host obligations; production tests distinguish corruption from I/O errors. Faithful batch decoding and filesystem durability remain external. Debt-first quota credit and full-request charge now compose with the grant kernel: a charge and full refund restore the refilled signed balance and next consume budget exactly when the debt is representable. Saturated or capped-away debt makes unconditional restoration false. The bounded-debt composition proves the exact balance after charge and repayment, debt clearance once credit reaches the cap, and a guaranteed consume budget from credit beyond it. These are integer credit guarantees; effective micro-token conversion, clock claims, rate/wait rounding, sensor identity, and serialized publication remain host obligations. The production refill now uses quota_refill to retain fractional micro-token credit while claiming each nanosecond interval once. Its composition with plan_consume proves that splitting an interval cannot create or lose a consume budget, even while repaying debt or reaching the burst. A rational-time ledger also fixes the exact final debt and fraction. The host preserves that fraction across nonzero rate changes and discards it when capped; its native regressions cover repeated clocks, rate changes, and large refills. Rate/wait floating-point conversion, clock provenance, and atomic publication remain outside the pure proof. The production bounded-charge adapter now derives its integer debt cap with quota_debt_cap. Rounding floating micro-tokens upward could retain debt beyond the requested wait: one micro-token per second retained one at a half-second bound, while the clock earned zero. The cap now floors the credit earned by the wait converted to nanoseconds. The elapsed-time composition connects that cap to charge, partitioned refill, whole-token selection and grant. It exports exact retained debt and final ledger, proves debt clears at the converted deadline, and proves enough extra time grants the full probe. Exact retention rejects a forget-all-debt implementation; deadline repayment rejects rounding upward. Matching local contracts for each wrong helper still prove, while the composition and independent native oracle fail. The real bucket regression checks both retained debt and deadline clearance at fractional rates. Rate, burst and quantum remain fixed, with no intervening operation; host time conversion, clock provenance, serialized claims and publication stay external. The arbitrary consume-trace composition joins that refill with the actual whole-token request selector and plan_consume. Its scaled ledger accounts for every grant, debt repayment, fractional credit, and credit discarded at the burst across repeated or backward clocks. A final request covering the burst must drain every whole token: conservation alone would allow permanent starvation. Independent signed-ledger tests and a zero-grant negative control check both properties. The trace uses a fixed positive configuration and serialized steps; unlimited zero-rate grants, rate changes, and intervening charges/refunds are outside its scope. The timestamp/ListOffsets composition connects the actual sparse scan and complete pending-transaction fold to isolation selection and the final response clamp. It resolves exactly when a matching record exists in the visible window, preserves global first-match identity through timestamp regressions and offset gaps, and strictly excludes every pending transaction start for read-committed consumers. Scanning the complete window before clamping agrees with finding the first match inside the visible prefix: once the global first match lies outside that prefix, no later record can be visible. This needs ordered offsets, not ordered timestamps. Replica/debug requests retain their log-end bound. Complete window decoding, truthful sparse bounds, cross-tier enumeration, epoch lookup, and coherent captured state remain host obligations; scheduled-delivery Fetch/LATEST caps are separate from positive-timestamp ListOffsets. The retained-tier union composition then combines floor-aware first matches with the production candidate merger and exclusive response clamp. It proves the global first retained visible match across overlapping local/remote windows, preserving the selected record timestamp rather than returning the request time. A real upload-gap regression catches the former remote-first short circuit. Both readers enforce the logical floor, including a cut inside one batch; per-tier object enumeration, byte decoding, and coherent capture remain external. Their sessions are under verif/krabka_verified_rlib/composition. They add no production runtime work. The audit states each theorem’s remaining identity, serialization, completeness, and durability assumptions; none proves the surrounding I/O or extends a bounded model to arbitrary executions.

A coherent recovered data window composes that snapshot-row theorem with the five-slot producer decision and acknowledgement arithmetic. It returns the first matching row’s original physical span and exclusive frontier, even with sequence wrap aliases, and derives non-duplicate policy from the newest row. A real sparse log spans an entire sequence wrap and checks the older alias after snapshot-plus-tail replay. Complete replay, window generation/eviction, faithful metadata projection, timestamps, and persisted bytes remain host facts; a snapshot stores only the last batch, so arbitrary restart equivalence is not claimed.

Token-description isolation composes a complete User-owner ACL scan with connection admission and token visibility. Matching permission rows grant only All/DescribeTokens, a matching deny wins, and any resource ACL suppresses the no-ACL fallback even when its principal or operation does not match. Token authentication and an excluding owner filter refuse visibility despite owner, requester, renewer, superuser, or ACL privilege. Faithful matching facts, complete enumeration, token-service configuration, the independent Describe grant for this token, HMAC generation, and response encoding remain host obligations.

Production kernels

The contract attributes beside each function are the source of truth. A proof applies only when its caller establishes every listed precondition. An empty precondition cell means that the contract accepts all values of the Rust input types.

Creusot also creates sessions for logic functions, lemmas, private helper functions, and generated Clone implementations. These sessions support the contracts in the ledger. They are not additional production kernels. Public logic functions and lemmas, such as kafka_rank, local_retention_model, or lemma_two_sites_never_survive, state a row’s rule and are named in its contract cell where the rule matters. The field accessor TransactionSnapshot::identity is proved with the transaction kernels and decides nothing on its own.

Run the Creusot Proofs

The .creusot-version file pins the Creusot release. That release pins the Rust nightly that creusot-rustc needs. Its creusot-setup/src/tools_versions_urls.rs file pins the prover binaries and checksums. Its creusot-deps.opam file pins Why3 and Why3find. The local why3find.json file selects the provers and sets the time limits, search depth, tactics, and proof-search profile. It does not set a memory limit.

Install the pinned Creusot release and its provers as the proofs job does. Then run these commands from the repository root:

aspect check-creusot-packages
export PATH="${HOME}/.local/share/creusot/bin:${PATH}"
packages=(krabka-verified)
for package in "${packages[@]}"; do
  cargo creusot --package "${package}"
done

The package check fails if a workspace package that depends on creusot-std or contains a Creusot contract is absent from the explicit proof list. It runs outside the proof image, which carries no Aspect CLI, and it also asserts that tools/creusot/prove.sh – the image’s entrypoint, and the loop above – still names the same packages, so the list and the proofs cannot drift apart. Each cargo creusot command updates its package directory under verif/.

cargo creusot exits with a nonzero status when any goal is unproved. A deliberately false #[ensures] makes the run end with Error: <n> unproved files and exit status 1, and prove.sh runs under set -euo pipefail. An unproved goal therefore fails the CI proof job. CI checks that proof result, not a clean Git diff. Generated .coma files contain an absolute source path, so another checkout can change them without a change to the proof result.

Stateright Model-Check Tier

Stateright enumerates reachable states within explicit bounds. It can find a counterexample in that state space. It does not prove behavior outside the bounds. Each model states its bounds and properties in its module comments.

The current model entry points are:

Some models drive a production kernel directly. Other models compose real decision functions with a small environment. Read the model’s DRIVEN and MODELED notes before you treat its property as a production guarantee.

Every unique-state count cited below is asserted by the model’s own runner against a PINNED_UNIQUE_STATES constant – one per config where a runner drives several – and not merely recorded here. An exhaustive breadth-first search over a fixed model visits a deterministic set of states, so the exact count is a checkable fact rather than a bound. The generated-transition count is not pinned anywhere: it depends on when the search’s worker threads deduplicate, and so varies between runs of the same model.

To change a pin, run the model, read the count the runner prints, and write that number into the constant. A changed count is a changed model, never a retuning knob, so a pull request that moves one must say which transition, action, or state field was added or removed to move it. A count that shrinks with no such explanation is the failure this pin exists to catch: an action generator that dropped a branch, a next_state arm that began returning None, or a derived Hash that stopped considering a field, each of which leaves a smaller search still passing every upper bound.

The paragraphs below take the entry points in table order. Each one names the production code the model drives, what it models instead, its bounds, its properties and reachability witnesses, and its pinned counts, and it ends with what stays outside the model.

Broker Data and Fetch

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 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 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 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 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.

Broker Failover and Placement

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 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 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 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 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.

Broker Quorum WAL

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.

Broker Groups and Transactions

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 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 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 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 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 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 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 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.

Broker Share and Break-Glass

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 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 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 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.

Log

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 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.

KRaft

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.

Throttle

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.

Audit

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.

Outside Both Tiers

Code that is not in the Creusot ledger or the Stateright inventory is in neither tier. This includes most protocol encoding and decoding, authorization, network and async orchestration, file and object-store I/O, and operational configuration. Unit, property, integration, differential, and container tests cover those areas. Those tests are evidence, but they are not a Creusot proof or a Stateright model check.

The barrier coordinator’s __barrier_state partitioner is the one coordinator routing decision without a proof. It applies Kafka’s Utils.abs(murmur2(bytes)) % numPartitions over the group name through the broker’s own murmur2, and JVM golden vectors test it. The group, transaction, and SHARE coordinator partitioners route through the proved java_string_hash_partition, and the KIP-405 metadata partitioner through remote_metadata_partition.

A proved kernel does not prove its caller. The proof starts after the caller establishes the preconditions in the ledger. A Stateright model does not prove the I/O around the decisions that it drives.

The shared SASL session kernels bind credential and positive listener deadlines and enforce expiry on ordinary requests, allowing reauthentication frames through the separate phase gate. An overflowing positive listener cap saturates instead of disappearing. Created-token composition derives coherent deadlines from creation, carries the captured expiry through both SCRAM rounds, and proves exact request admission plus token-API isolation. Credential-free composition proves that PLAIN, regular SCRAM and GSSAPI retain a finite listener ceiling, including clock overflow. Cryptographic success, faithful host snapshots and nondecreasing clocks are explicit external obligations; later token mutation is outside the captured snapshot.

OAuth validation completion binds the finishing clock observation to a still-current and fresh supplied JWKS snapshot. The common host validation path passes its returned completion time into session admission, so asynchronous validation consumes the token’s advertised remaining lifetime. The consumer theorem composes initial cache admission, completion admission, session deadlines and reauthentication principal binding, with exact rejection and service conditions. Successful cryptographic validation, faithful claim/cache projection, accurate clocks and absence of generation ABA remain external obligations; absent cache observations carry no JWKS freshness claim.

Cache publication and OAuth admission connects the production publication-generation kernel to the cache guard, completion clock and initial controller session admission. For any length of exclusive-writer fetch outcomes, each installed key set advances the committed generation by two; failed fetches and exhaustion preserve keys. The final generation equals the initial generation exactly when no keys were installed. An unfinished writer enters an odd generation. This derives the absence of generation ABA for this publisher, instead of assuming it.

Given a stable starting snapshot and a valid unexpired initial credential with no broker cap, the composition authenticates exactly when no keys changed, no writer is in flight and hard cache expiry has not elapsed at completion. It also proves that the computed lifetime ends at the token expiry. A counter at its last even generation safely preserves the old cache and may still serve it while fresh. The controller now supplies the same publication atomics as the data listener; a signed-token wire fixture distinguishes a fresh cache from stale, never-published and in-flight metadata, and a validation fixture changes the observed generation after cryptographic success.

Exclusive CAS ownership, the complete ordered publication trace, faithful atomic/clock/claim observations, actual key replacement and cryptographic correctness remain host obligations. Failed or competing publishers cannot be omitted if they modify keys. This proves admission at authentication; the controller hands the stream to the raft engine and currently has no subsequent credential-expiry gate, despite OAuth advertising a finite lifetime.