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.