The `quorum` crate

The decision core of the shrinking quorum. Each tick it decides what the system may deliver, given what three replicas returned.

no_stdno allocationno dependencies4 Kani proofsv0.1.1

Install

The crate is not on crates.io yet. Depend on the repository at a tag:

# Cargo.toml
[dependencies]
quorum = { git = "https://github.com/mruspace/flight", tag = "v0.1.1" }

Example

use quorum::{decide, Health, Outcome, Policy, Reply};

let mut health = Health::new();
let replies = [Reply::Single(42), Reply::Single(42), Reply::Single(7)];
let v = decide(Policy::Shrink, &replies);

if let Outcome::Deliver(x) = v.outcome { send(x); }
for (i, outvoted) in v.dissent.iter().enumerate() {
if *outvoted && health.strike(i, tick) { run_known_answer_test(i); }
}

API

const REPLICAS: usize = 3

Number of replicas.

const STRIKES: usize = 3

Strikes within STRIKE_WINDOW ticks that trigger a diagnosis.

const STRIKE_WINDOW: u64 = 200

Length of the strike window, in ticks.

enum Policy

Shrink	Vote on three, compare on two, self-check on one.
Tmr	Vote on three, compare on two, stop on one (classic fixed TMR).

enum Mode

Vote, Compare, SelfCheck (one replica computes everything twice and compares with itself), Halted.

enum Reply

Absent	The replica is dead or did not answer.
Single(u64)	One result.
Pair(u64, u64)	Two results of the same computation (self-check).

enum Outcome

Deliver(u64)	Deliver this result.
Detected	A disagreement was caught; deliver nothing this tick.
Halted	The policy cannot continue with the replicas left.

struct Verdict

Field	Type	Meaning
mode	Mode	The mode used this tick.
outcome	Outcome	What to do with this tick.
dissent	[bool; 3]	Replicas that were outvoted (vote mode only).
diagnose	bool	Two replicas disagree and nothing tells which is wrong: run a known-answer test on both (shrinking quorum only).

fn mode(policy, alive) -> Mode

The mode a policy runs in with alive live replicas.

fn decide(policy, &[Reply; 3]) -> Verdict

Decide what to deliver from the replicas' replies.

struct Health

Strike record per replica. Health::new() is const. strike(i, tick) returns true when replica i has three strikes inside the window and must be diagnosed. clear(i) forgets its strikes after it passes.

Kani proofs

Run with cargo kani -p quorum. Each holds for every possible input.

Proof	Property
identical_while_tmr_can_run	With two or more replicas alive, both policies decide the same.
tmr_stops_below_two	Fixed TMR halts below two replicas.
shrink_halts_only_with_nothing_left	The shrinking quorum halts only at zero.
delivers_only_agreed_values	A delivered value had two votes, or a clean self-check.

Targets and builds

CI builds and tests on every change:

Linux ARM64, Linux x86_64 and macOS (Apple silicon)
Bare-metal ARM Cortex-M, thumbv7em-none-eabihf, as no_std (build only)
Static ARM Linux binaries of the demo, 64-bit and 32-bit (hard and soft float), tested under emulation

PreviousShrinking quorum NextThe quorum CLI

Updated 7 Oct 2026 · Source: quorum/src/lib.rs · Edit on GitHub · Questions? Request information

The quorum crate