# Mru docs

> Reference for Mru's open core, for unattended missions with no repair path: the shrinking-quorum decision crate and its fault-injection demo (Rust, no_std, nine Kani proofs: four on the core, five on the C interface), the Dusk simulator and the Mru 2049 browser flight simulator. The quorum demo ran once in orbit on ESA's OPS-SAT PRETTY satellite (exp4051, 18 Oct 2026); the F´ components have not run on flight hardware. Code under Apache 2.0.

---

# Mru Docs

URL: https://docs.mru.space/

Overview

# Mru documentation

Reference for Mru's open core, for unattended missions with no repair path: the shrinking-quorum runtime, the Dusk simulator, and the tools around them.

## Where to start

[

Concepts

### Degradation-first design

The Degradation-First Principle and the shrinking quorum that applies it: what is proved, what is tested, and what it costs.

](https://docs.mru.space/concepts/shrinking-quorum/#degradation-first)[

Core runtime

### The `quorum` crate

Vote on three, compare on two, self-check on one. `no_std`, no allocation, checked with Kani.

](https://docs.mru.space/core/quorum-crate/)[

Simulation

### Dusk

A Monte Carlo of redundancy policies on hardware that only ever decays. 10,000 missions in about two seconds.

](https://docs.mru.space/simulation/dusk/)[

Integrations

### F´ and OPS-SAT

Ran in orbit on OPS-SAT PRETTY, 18 Oct 2026 (exp4051), after the software environment and FlatSat tests. F´ components around the Rust core, a C interface for other frameworks, and the operations note and package for the experiment.

](https://docs.mru.space/core/fprime/)[

Lab

### Mru 2049

A browser flight simulator on real astronomical data. 109,389 stars, planets correct for any date.

](https://docs.mru.space/lab/2049/)

## Quickstart

You need a Rust toolchain. Clone the runtime, run its tests, then run the demo with two replicas killed.

```
# the runtime and its demo
git clone https://github.com/mruspace/flight
cd flight
cargo test --workspace
cargo run --release --bin quorum -- --policy shrink --ticks 20000 --seed 1 \
  --upset-rate 0.001 --fault kill:0@5000 --fault kill:1@10000
```

Run the same seed with `--policy tmr` to compare. The first two lines of each run:

```
policy=shrink ticks=20000 seed=1 upset_rate=0.001
useful=14989 detected=11 wrong=0 halted_at=never alive_at_end=1 stopped=completed last_useful=20000 kat_tests=174

policy=tmr ticks=20000 seed=1 upset_rate=0.001
useful=9990 detected=9 wrong=0 halted_at=10000 alive_at_end=1 stopped=halted last_useful=9999 kat_tests=0
```

flight v0.3.1 on an Apple M4. The counts depend only on the seed.

Fixed TMR halts at tick 10000, when the second replica dies. The shrinking quorum keeps running on the last replica, which checks its own work.

Then the simulator, which needs no dependencies:

```
git clone https://github.com/mruspace/dusk
cd dusk
cargo run --release --bin dusk              # 10,000 missions, about 2 s
cargo run --release --bin dusk -- --sweep   # sensitivity, about 1 minute
```

Times on an Apple M4 with 10 cores.

## Where the code lives

| Repository | What it is | Language | Status |
| --- | --- | --- | --- |
| [mruspace/flight](https://github.com/mruspace/flight) | Decision core, demo program, bench, C interface and F´ components | Rust, C++ | v0.3.1 |
| [mruspace/dusk](https://github.com/mruspace/dusk) | Redundancy Monte Carlo | Rust | 0.1.0 |
| [mruspace/2049](https://github.com/mruspace/2049) | Browser flight simulator | TypeScript | Lab |

Code Apache 2.0 · Whitepaper CC BY 4.0, doi:10.5281/zenodo.23305299 · Questions: [Get in touch](https://mru.space/contact/)

---

# Shrinking quorum

URL: https://docs.mru.space/concepts/shrinking-quorum/

[Docs](https://docs.mru.space/) / [Concepts](https://docs.mru.space/concepts/shrinking-quorum/) / Shrinking quorum

# Shrinking quorum

A redundancy policy for unattended missions with no repair path: vote on three replicas, compare on two, self-check on one. It keeps running on the last replica, where fixed TMR stops.

Kani proves that, with two or more replicas alive, `decide()` gives the same outcome under both policies, for every set of three replies. The shrinking quorum also sets `diagnose` at two replicas, so it can retire a stuck replica and continue where fixed TMR stays in disagreement. Over a whole run, never less than fixed TMR is tested, not proved.

## The trouble with a fixed threshold

Classic triple modular redundancy (TMR) runs three processors on the same work and takes the majority. Two can still detect a disagreement. One cannot outvote anything, so the system stops.

Most fault tolerance assumes someone can step in eventually. With a ground team in reach, stopping is safe: the team finds the fault and commands a fallback. With no one in reach, stopping throws away the last processor's whole remaining life.

Fixed TMR is the baseline on these pages because both policies give the same outcome while two or more replicas live. It is not what most spacecraft fly. Most fly dual-string radiation-hardened processors with EDAC, watchdogs and autonomous fault protection. Stepping down from three to two to one is not new either: the Space Shuttle's redundant set of general-purpose computers did it, and Meyer gave degradable systems a measure, performability, in 1980. See [Prior art](https://docs.mru.space/concepts/prior-art/).

What Mru adds: the step-down runs with no ground team, the decision core is small and checked with Kani, and the trade data is published ([Dusk](https://docs.mru.space/simulation/dusk/), [bench](https://docs.mru.space/core/bench/)).

## Three modes

The policy picks a mode from the number of live replicas. This is the whole rule, from `quorum::mode`:

| Live replicas | Fixed TMR | Shrinking quorum |
| --- | --- | --- |
| 3 | Vote · masks one bad result | Vote · masks one bad result |
| 2 | Compare · loses the tick on a mismatch | Compare · runs a known-answer test to find the bad one |
| 1 | Halted, for good | Self-check · computes twice, delivers on a match, half speed |
| 0 | Halted | Halted |

```
pub fn mode(policy: Policy, alive: usize) -> Mode {
match (policy, alive) {
    (_, 0) => Mode::Halted,
    (Policy::Shrink, 1) => Mode::SelfCheck,
    (Policy::Tmr, 1) => Mode::Halted,
    (_, 2) => Mode::Compare,
    _ => Mode::Vote,
}
}
```

## Degradation-first

The shrinking quorum applies the whitepaper's design principle:

Principle: "A system intended to operate for millennia without intervention must treat its own physical decay (of power, computation, memory, and thermal capacity) not as an exceptional fault to be handled, but as the constant, governing condition around which every architectural decision is made."

Corollary: "Capability is a depleting resource to be spent, not a fixed budget to be defended. The objective is not to preserve function but to maximize the cumulative useful work extracted across the entire descent from full capability to silence."

W. Binns, [Mru whitepaper](https://mru.space/mru-whitepaper.pdf), version 1.1.1, section 5, doi:10.5281/zenodo.23305299.

For the shrinking quorum, the figure of merit is useful work over the whole decline, not correct operation at full strength. [Dusk](https://docs.mru.space/simulation/dusk/) measures it, along with the wrong results it costs.

## What is proved and what is tested

### Proved (per tick)

Four Kani proofs on `decide()`. Each reply is any of `Absent`, `Single` or `Pair`, with any `u64` values, so each proof covers every set of three replies to `decide()`.

-   [`identical_while_tmr_can_run`](https://github.com/mruspace/flight/blob/v0.3.1/quorum/src/lib.rs#L331): with two or more replies present, both policies give the same outcome. It compares the outcome only, not the mode or `diagnose`.
-   [`tmr_stops_below_two`](https://github.com/mruspace/flight/blob/v0.3.1/quorum/src/lib.rs#L343): with fewer than two replies present, the fixed TMR outcome is `Halted`.
-   [`shrink_halts_only_with_nothing_left`](https://github.com/mruspace/flight/blob/v0.3.1/quorum/src/lib.rs#L352): the shrinking quorum's outcome is `Halted` if and only if no reply is present.
-   [`delivers_only_agreed_values`](https://github.com/mruspace/flight/blob/v0.3.1/quorum/src/lib.rs#L362): if either policy delivers a value, at least two replies agree on it, or exactly one replica is alive and it returned `Pair(v, v)`.

CI runs `cargo kani -p quorum -p quorum-ffi` on every change. Five more proofs show that the C interface gives the core's answer. The proofs do not cover the health record, the diagnosis, the known-answer test, timing, or the system over a run. See [Kani proofs](https://docs.mru.space/core/quorum-crate/#proofs).

### Tested (per run)

Never less useful work than fixed TMR over a whole run is a test result, with these scopes:

-   **Scenario tests.** `scripts/scenarios.sh` in CI: ten seeds, two kill faults per run, 20,000 ticks. Kill faults only.
-   **Bench.** 150 pairs of runs per host, five fault schedules, on three hosts with general-purpose processors. The three replicas are processes on one host, not separate processors. No pair below fixed TMR. See [Bench](https://docs.mru.space/core/bench/#results).
-   **OPS-SAT.** One run in orbit on the SEPP, 5,250 ticks: 2,745 correct, 0 wrong, every fault on its tick. One seed, one schedule. See [On OPS-SAT](https://docs.mru.space/core/quorum-cli/#opssat).
-   **Dusk.** 10,000 simulated missions. The two policies are identical until fixed TMR stops, by construction of the model, and a unit test checks it over 200 seeds. See [Dusk](https://docs.mru.space/simulation/dusk/).

## Two replicas

With two replicas left, `decide()` compares them. Equal values are delivered. Unequal values give `Detected`, and nothing goes out that tick. Under the shrinking quorum it also sets `diagnose`. Fixed TMR does not.

The demo then runs a known-answer test (KAT) on both replicas: a fixed input whose result is known. There are three cases.

-   **Both pass.** Nothing is retired. The tick is lost, and nothing escalates. A persistent fault that the KAT cannot see keeps every tick `Detected`.
-   **Both fail or time out.** Both are retired, and the run halts. Fixed TMR would keep comparing.
-   **One fails.** It is retired. The survivor goes on in self-check.

This is the current behavior. The first two cases are gaps: no escalation for a fault the KAT cannot see, and a halt where fixed TMR would go on.

## What it costs

On one replica, a stuck fault is caught only by the periodic known-answer test, and only if it changes the test's answer. Until then, wrong results get out. Fixed TMR never produces those, because it never lives that long. The bench measures how many faults the test catches: [known-answer test coverage](https://docs.mru.space/core/bench/#kat).

Trade: In Dusk's default run, 20.1% of missions (95% CI 19.3% to 20.9%) deliver at least one wrong result under the shrinking quorum, and 0.0% under fixed TMR. Fixed TMR comes out ahead only if one wrong result costs more than 136 years of useful work (95% CI 131 to 142). The run assumes no ground support after launch.

## Command path

Self-check on one replica can deliver a few wrong results before the KAT catches a stuck fault. The KAT runs every `--kat-period` ticks, 64 by default. An upset that hits both self-check runs alike can also get through.

This mode is for data products, not spacecraft commands, unless the mission adds its own command safety layer. Integrators can gate commands on `Verdict.mode`: issue a command only when the mode is `Vote` or `Compare` and the outcome is `Deliver`. See the [example](https://docs.mru.space/core/quorum-crate/#gate).

## Health and diagnosis

A replica outvoted `STRIKES` = 3 times within `STRIKE_WINDOW` = 200 ticks is diagnosed with a known-answer test. Pass, and its strikes are cleared, on the assumption that the upsets were transient. Fail, and it is retired. The strike record has unit tests, not proofs.

## Graceful Degradation Index

The whitepaper scores a degrading system by the ratio of capability delivered to hardware surviving. 1.0 means every surviving part is doing useful work. Dusk measures the simpler cousin, total useful work across the whole decline.

## Open questions

-   **Common-mode faults**, such as shared power, clock or thermal. Dusk models correlated deaths with `--p-corr`. The demo models an upset that hits both self-check runs alike with `--common-mode`. Neither models shared power, clock or thermal faults.
-   **Input agreement between replicas.** In the demo, all replicas get the same input because it is a function of the tick. Real sensor inputs need an agreement step. Mru does not provide one yet.
-   **Replica determinism under interrupts and scheduling.** The replicas must compute the same bits. In the demo this holds only because the task is a pure function of the tick. Neither Dusk nor the bench tests it.
-   **KAT coverage on real hardware.** Dusk sets self-check coverage as a parameter, `--coverage`. The bench's stuck fault returns the same wrong value for every input, so the KAT always sees it. Neither measures the share of real hardware faults a KAT catches.

## Related

-   [The `quorum` crate](https://docs.mru.space/core/quorum-crate/): the decision core, in Rust
-   [Dusk](https://docs.mru.space/simulation/dusk/): 10,000 missions, 1.34× the useful work of fixed TMR. This assumes no ground support after launch. The gain falls to 1.00× when support never ends ([ground support](https://docs.mru.space/simulation/dusk/#ground)). Against three-string cold standby it is 0.92× to 1.60×, depending on how fast an unpowered spare ages ([baselines](https://docs.mru.space/simulation/dusk/#baselines)).
-   [Prior art](https://docs.mru.space/concepts/prior-art/): TMR, degradable systems, the Space Shuttle and deep-space fault protection
-   [Research log № 002](https://mru.space/research/dusk-results/): the results, written up

Updated 19 Oct 2026 · [Edit on GitHub](https://github.com/mruspace/docs/edit/main/src/pages/concepts/shrinking-quorum.astro) · [Questions? Get in touch](https://mru.space/contact/)

---

# Architecture status

URL: https://docs.mru.space/concepts/architecture/

[Docs](https://docs.mru.space/) / [Concepts](https://docs.mru.space/concepts/shrinking-quorum/) / Architecture status

# Architecture status

The whitepaper describes six layers and the parts they share. This page shows where each part stands today: what is built, where the code is, and what evidence supports it.

For the design itself, read the [architecture overview](https://mru.space/architecture/) or the [whitepaper](https://mru.space/mru-whitepaper.pdf). Section numbers on this page refer to the whitepaper.

## Status levels

Each part has one of five levels. A part moves up only with the evidence the level names.

| Level | Meaning |
| --- | --- |
| Paper | Described in the whitepaper. No code. |
| Spec | A written specification: interfaces, data formats and the properties to prove. No code. |
| Prototype | Code with tests or proofs, run on general-purpose processors. Not measured on target hardware. |
| Bench-tested | Measured on target-class processors with injected faults. Results published. |
| Deployed | Ran in orbit or at a field site. Logs published. |

## Layers 0 to 5

Only Layer 1 has code today. Layers 0 and 2 to 5 are not built. They exist only in the whitepaper.

| Layer | Whitepaper | Code | Status | Evidence |
| --- | --- | --- | --- | --- |
| 0 · Survival kernel | §7 | Not built | Paper | None |
| 1 · Hardware consensus and health | §8 | [`quorum` crate](https://docs.mru.space/core/quorum-crate/), [demo](https://docs.mru.space/core/quorum-cli/), [F´ components](https://github.com/mruspace/flight/tree/main/fprime) | Deployed, partial | Nine Kani proofs, the scenario checks and 45 F´ unit tests in CI, a known-answer test coverage campaign, an F´ system test against the demo, two F´ deployments (`MruOpsSat`, and`MruQuorum` with each replica in a process of its own) run full length in ESA's OPS-SAT experiment environment under emulation, [bench](https://docs.mru.space/core/bench/) on general-purpose processors, Dusk, and the quorum demo on the SEPP flight processor: OPS-SAT PRETTY FlatSat (16 Oct 2026) and in orbit (18 Oct 2026, exp4051), [logs published](https://github.com/mruspace/flight/tree/main/opssat/results). The F´ components stay Prototype. |
| 2 · Navigation and orientation | §9 | Not built | Paper | None |
| 3 · Science and knowledge triage | §10 | Not built | Paper | None |
| 4 · Communication | §11 | Not built | Paper | None |
| 5 · Bounded self-modification | §12 | Not built | Paper | None |

## Layer 1, part by part

Section 8 gives Layer 1 five parts. The shrinking quorum is built. The health registry is partly built. The other three are not started.

| Part | Status | What exists |
| --- | --- | --- |
| Shrinking quorum | Deployed | `quorum::mode` and `quorum::decide`: vote on three, compare on two, self-check on one. `no_std`, no allocation, builds for ARM Cortex-M. The F´ component `RedundancyManager` runs it through a C interface that Kani proves equal to the core. The quorum demo ran it on the OPS-SAT SEPP, a Cortex-A9 flight processor, on the FlatSat and in orbit: three software replicas on one processor, faults from a schedule. `RedundancyManager` has not run there. The F´ deployments run it with F´'s own services and are built for the SEPP; the second puts each replica in a process of its own on the SEPP's two cores, with a real process kill. |
| Node health registry | Deployed, partial | `quorum::Health` counts strikes per replica. Three strikes within 200 ticks start a known-answer test, which retires or clears the replica. The F´ component `HealthRegistry` holds the record. The whitepaper's score of error rate, response time and gate use is not built. `quorum::Health` ran in the OPS-SAT runs and retired the stuck replica at tick 122; the F´ `HealthRegistry` did not run. |
| Memory scrubbing | Paper | Listed as the F´ `ScrubScheduler`, not started. The demo's radiation sensor checks a memory block for bit flips. It counts upsets. It does not scrub. |
| Hardware inventory and cannibalization | Paper | Not started. `RedundancyManager` can admit a spare into a replica slot after a known-answer test; choosing when is the inventory's job. Dusk models salvaged spares in simulation only. |
| Power accountant | Paper | Listed as the F´ `PowerAccountant`, not started. `RedundancyManager` can put a replica on standby, the hook it will use. |

F´ component status from [docs/fprime-design.md](https://github.com/mruspace/flight/blob/main/docs/fprime-design.md) in mruspace/flight.

## Shared parts

These parts serve every layer.

| Part | Whitepaper | Status | What exists |
| --- | --- | --- | --- |
| Duty-cycle scheduler | §4.5 | Paper | None. The whitepaper does not yet assign it to a layer. |
| Memory tiers | §4.3 | Paper | None. |
| Degradation model and mission phases | §13 | Paper | None. Dusk models processor loss, not the power phases. |
| Simulation framework | §14 | Prototype, partial | [Dusk](https://docs.mru.space/simulation/dusk/) models processor failures, correlated failures, salvaged spares and upsets. It does not model power decay, thermal limits, memory decay or science targets. |

Section 14 names six metrics. Dusk reports useful work, wrong results and the day output ends, which is survival duration. The other five need power and science models that Dusk does not have yet. Dusk's parameters are illustrative, not calibrated. The [bench](https://docs.mru.space/core/bench/) measures useful work, survival and the Graceful Degradation Index on real processes.

## Products and research

-   **Mru Flight** is Layer 1 for spacecraft. The F´ components `RedundancyManager`, `HealthRegistry` and `ReplicaHost` are built and tested: 45 unit tests with the two test-only components, a system test against the demo's counts on the bench schedules, and two F´ deployments, the second with each replica in a process of its own. They have not run on flight hardware. The quorum demo, without F´, [ran in orbit on ESA's OPS-SAT PRETTY satellite](https://docs.mru.space/core/quorum-cli/#opssat) on 18 Oct 2026 (exp4051), as three software replicas on one Linux payload processor with faults from a schedule. Results matched the prediction written before the run.
-   **Mru Field** is the same Layer 1 core for systems on Earth that are hard to reach. See [Mru Field](https://mru.space/field/).
-   **Dusk** is the first part of the §14 simulation framework.
-   **Mru 2049** is not part of the layers. It is a [browser flight simulator](https://docs.mru.space/lab/2049/) on real astronomical data.

## What comes next

In order:

-   **Run the full bench on target-class processors.** The quorum demo has run once on a flight processor, on the FlatSat and in orbit; the 300-run [bench](https://docs.mru.space/core/bench/) with reboots and power cuts has not.
-   **Calibrate Dusk** with radiation or flight data. Its policy model is already [checked against the bench](https://docs.mru.space/core/bench/#model).
-   **Specify Layer 0.** The instruction set, the format of behavior programs, the integrity check against Tier 0, and the properties to prove. Code starts after the specification.

## Related

-   [Architecture overview](https://mru.space/architecture/): the six layers and the descent, on mru.space
-   [Shrinking quorum](https://docs.mru.space/concepts/shrinking-quorum/): the Layer 1 rule, what is proved and what is tested
-   [Qualification path](https://docs.mru.space/concepts/qualification/): what exists against the NASA and ECSS software standards
-   [Dusk](https://docs.mru.space/simulation/dusk/): 10,000 missions, 1.34× the useful work of fixed TMR. This assumes no ground support after launch. The gain falls to 1.00× when support never ends. See [Ground support](https://docs.mru.space/simulation/dusk/#ground).

Updated 19 Oct 2026 · [Edit on GitHub](https://github.com/mruspace/docs/edit/main/src/pages/concepts/architecture.astro) · [Questions? Get in touch](https://mru.space/contact/)

---

# Prior art and related work

URL: https://docs.mru.space/concepts/prior-art/

[Docs](https://docs.mru.space/) / [Concepts](https://docs.mru.space/concepts/shrinking-quorum/) / Prior art

# Prior art and related work

The shrinking quorum builds on decades of work in fault-tolerant computing. Stepping down from three replicas to two to one is not new. This page lists the work Mru draws on and how Mru relates to each.

## TMR and its origins

-   **von Neumann, 1956.** Shows that reliable computation can be built from unreliable components through redundancy. Mru: the shrinking quorum is one use of that idea, with the redundancy shrinking as parts fail.

    J. von Neumann, "Probabilistic Logics and the Synthesis of Reliable Organisms from Unreliable Components," in C. E. Shannon and J. McCarthy (eds.), Automata Studies, Princeton University Press, 1956, pp. 43-98.

-   **Lyons and Vanderkulk, 1962.** Triple modular redundancy with a majority vote, applied to reliability. Mru: fixed TMR in this form is the baseline on these pages. With three replicas, the shrinking quorum votes the same way.

    R. E. Lyons and W. Vanderkulk, "The Use of Triple-Modular Redundancy to Improve Computer Reliability," IBM Journal of Research and Development, 6(2):200-209, 1962. [doi:10.1147/rd.62.0200](https://doi.org/10.1147/rd.62.0200)


## Degradable systems and performability

-   **Meyer, 1980.** Defines performability, a measure that combines performance and reliability for systems that degrade. Mru: Dusk's figure of merit, useful work summed over the whole decline, is a measure of this kind. The whitepaper cites Meyer for it.

    J. F. Meyer, "On Evaluating the Performability of Degradable Computing Systems," IEEE Transactions on Computers, C-29(8):720-731, 1980. [doi:10.1109/TC.1980.1675654](https://doi.org/10.1109/TC.1980.1675654)


## Byzantine agreement

-   **Lamport, Shostak and Pease, 1982.** Sets the limits of agreement when faulty components can give conflicting information to different parts of a system. Mru: the shrinking quorum assumes replicas that are damaged, not malicious. It does not solve input agreement: all replicas must already have the same input. See [Open questions](https://docs.mru.space/concepts/shrinking-quorum/#open-questions).

    L. Lamport, R. Shostak and M. Pease, "The Byzantine Generals Problem," ACM Transactions on Programming Languages and Systems, 4(3):382-401, 1982. [doi:10.1145/357172.357176](https://doi.org/10.1145/357172.357176)


## Redundancy management on the Space Shuttle

-   **Sklaroff, 1976.** The Shuttle's general-purpose computers ran as a redundant set. Voting detected and identified two failures. The remaining two used comparison and self-test to tolerate a third. Mru: degradation from voting to comparison to self-test is not new. Mru does it with no ground team.

    J. R. Sklaroff, "Redundancy Management Technique for Space Shuttle Computers," IBM Journal of Research and Development, 20(1):20-28, 1976. [doi:10.1147/rd.201.0020](https://doi.org/10.1147/rd.201.0020)

-   **Spector and Gifford, 1984.** A case study of the Shuttle's primary computer system. Mru: a reference for how a flown redundant system was designed and managed.

    A. Spector and D. Gifford, "The Space Shuttle Primary Computer System," Communications of the ACM, 27(9):872-900, 1984. [doi:10.1145/358234.358246](https://doi.org/10.1145/358234.358246)


## Autonomous fault protection on deep-space missions

-   **Avizienis et al., 1971 (STAR).** JPL's self-testing and repairing computer, designed for outer-planet spacecraft. Standby spares replaced failed units by automatic recovery. Mru: autonomous recovery in deep space is decades old. The shrinking quorum steps down instead of relying on spares. The F´ `RedundancyManager` can admit a spare after a known-answer test.

    A. Avizienis, G. C. Gilley, F. P. Mathur, D. A. Rennels, J. A. Rohr and D. K. Rubin, "The STAR (Self-Testing And Repairing) Computer: An Investigation of the Theory and Practice of Fault-Tolerant Computer Design," IEEE Transactions on Computers, C-20(11):1312-1321, 1971. [doi:10.1109/T-C.1971.223133](https://doi.org/10.1109/T-C.1971.223133)

-   **Rasmussen, 2008.** Fundamentals of fault-tolerant design for spacecraft guidance, navigation and control, from JPL. Mru: the shrinking quorum is one autonomous response to processor loss. It is not a full fault-protection system and does not replace one.

    R. D. Rasmussen, "GN&C Fault Protection Fundamentals," 31st Annual AAS Guidance and Control Conference, Breckenridge, CO, 2008. Jet Propulsion Laboratory. Companion presentation: [NASA NTRS 20100020171](https://ntrs.nasa.gov/citations/20100020171).


## What Mru adds

-   **Autonomy with no ground team.** The step-down from three replicas to one runs on board, with no command from the ground.
-   **A small decision core with proofs.** The [quorum crate](https://docs.mru.space/core/quorum-crate/) is `no_std` with no allocation. Kani proves four properties of `decide()` for every set of three replies. See [Kani proofs](https://docs.mru.space/core/quorum-crate/#proofs) for the scope of each.
-   **Published trade data.** [Dusk](https://docs.mru.space/simulation/dusk/) and the [bench](https://docs.mru.space/core/bench/) publish what the step-down buys in useful work and what it costs in wrong results, with the code to reproduce them.

Updated 11 Oct 2026 · [Edit on GitHub](https://github.com/mruspace/docs/edit/main/src/pages/concepts/prior-art.astro) · [Questions? Get in touch](https://mru.space/contact/)

---

# Qualification path

URL: https://docs.mru.space/concepts/qualification/

[Docs](https://docs.mru.space/) / [Concepts](https://docs.mru.space/concepts/shrinking-quorum/) / Qualification path

# Qualification path

What exists today, and the NASA and ECSS software standards it relates to. No qualification evidence exists yet. Mru makes no compliance claim.

## Standards

This page maps Mru to four software standards, two from NASA and two from ECSS:

| Number | Title |
| --- | --- |
| NPR 7150.2 | NASA Software Engineering Requirements |
| NASA-STD-8739.8 | Software Assurance and Software Safety Standard |
| ECSS-E-ST-40C | Space engineering: Software |
| ECSS-Q-ST-80C | Space product assurance: Software product assurance |

The tables below map by topic, not by clause. No clause of any standard has been checked against Mru.

## What exists

These activities run today. They are engineering evidence, not qualification evidence: none was planned, reviewed or recorded under a standard.

| Activity | What exists | Related standards |
| --- | --- | --- |
| Unit tests | Unit tests of the core and the C interface, run in CI on every change. See [the quorum crate](https://docs.mru.space/core/quorum-crate/). | NPR 7150.2, ECSS-E-ST-40C |
| Formal proofs | Nine Kani proofs, four on the core and five on the C interface, run in CI on every change. Each has a stated scope. See [Kani proofs](https://docs.mru.space/core/quorum-crate/#proofs). | NPR 7150.2, NASA-STD-8739.8, ECSS-E-ST-40C, ECSS-Q-ST-80C |
| Continuous integration | Build and test on Linux x86\_64, Linux ARM64 and macOS, plus static ARM Linux binaries tested under emulation and a bare-metal ARM Cortex-M build. | NPR 7150.2, ECSS-E-ST-40C |
| Scenario tests | `scripts/scenarios.sh` runs the demo program and checks its output: faults, limits, resets and the comparison with fixed TMR. | NPR 7150.2, ECSS-E-ST-40C |
| Bench | 300 runs per host with injected faults on three general-purpose processors, and a known-answer test coverage campaign on the last replica. Not radiation testing, not target hardware. See [Bench](https://docs.mru.space/core/bench/). | NPR 7150.2, ECSS-E-ST-40C |
| F´ unit tests and system test | 45 unit tests of the F´ components, a 60-case system test against the demo's counts, and the first deployment against the demo in CI. Not run on flight hardware. See [F´ components](https://docs.mru.space/core/fprime/#tests). | NPR 7150.2, ECSS-E-ST-40C |
| F´ requirements and design notes | Drafts in the flight repo: numbered requirements with a verification method each, and the design notes. Not baselined or reviewed by a program. See [fprime-requirements.md](https://github.com/mruspace/flight/blob/v0.3.1/docs/fprime-requirements.md). | NPR 7150.2, ECSS-E-ST-40C |
| OPS-SAT experiment exp4051 | One run each in ESA's software environment, on the PRETTY FlatSat and in orbit on the SEPP, 18 Oct 2026. Not radiation testing; no real upset in the window. See [On OPS-SAT](https://docs.mru.space/core/quorum-cli/#opssat). | NPR 7150.2, ECSS-E-ST-40C |

## Not started

| Activity | Status | Related standards |
| --- | --- | --- |
| Hardware-in-the-loop testing on target-class processors | Not started | NPR 7150.2, ECSS-E-ST-40C |
| Radiation testing | Not started | Hardware topic, outside the four software standards above |
| Software classification and criticality | Not started | NPR 7150.2, NASA-STD-8739.8, ECSS-Q-ST-80C |
| Requirements traceability | Not started | NPR 7150.2, ECSS-E-ST-40C |
| Independent verification and validation | Not started | NPR 7150.2, NASA-STD-8739.8, ECSS-E-ST-40C |
| Tool qualification (compiler, Kani, test tools) | Not started | NPR 7150.2, ECSS-Q-ST-80C |
| Coding standard compliance | Not started | NPR 7150.2, ECSS-Q-ST-80C |
| MC/DC structural coverage | Not started | NPR 7150.2, ECSS-E-ST-40C |
| Software development and assurance plans | Not started | NPR 7150.2, NASA-STD-8739.8, ECSS-E-ST-40C, ECSS-Q-ST-80C |

Status as of 22 Oct 2026, flight v0.7.0. The F´ components, the deployment and the C interface have numbered requirements, each with a verification method, but no trace to mission or standard requirements.

## Related

-   [Architecture status](https://docs.mru.space/concepts/architecture/): what is built, layer by layer
-   [Shrinking quorum](https://docs.mru.space/concepts/shrinking-quorum/#guarantees): what is proved and what is tested

Updated 19 Oct 2026 · [Edit on GitHub](https://github.com/mruspace/docs/edit/main/src/pages/concepts/qualification.astro) · [Questions? Get in touch](https://mru.space/contact/)

---

# quorum crate API reference

URL: https://docs.mru.space/core/quorum-crate/

[Docs](https://docs.mru.space/) / [Core runtime](https://docs.mru.space/core/quorum-crate/) / quorum crate

# 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\_std no allocation no dependencies 9 Kani proofs v0.3.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.3.1" }
```

## Example

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

// read_replicas, send and run_known_answer_test are your code.
let mut health = Health::new();
for tick in 0u64.. {
    let replies: [Reply; REPLICAS] = read_replicas(tick);
    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); }
    }
}
```

## Gate commands on the mode

On one replica, self-check can deliver a few wrong results before the periodic known-answer test catches a stuck fault. Use that mode for data products, not spacecraft commands, unless the mission adds its own command safety layer. This example issues a command only when the mode is `Vote` or `Compare` and the outcome is `Deliver`. See [Command path](https://docs.mru.space/concepts/shrinking-quorum/#command-path).

```
//! Gate commands on the mode. Only a result that two or more replicas agree
//! on (vote or compare) may command the spacecraft. A result from the last
//! replica's self-check goes out as a data product only.
use quorum::{decide, Mode, Outcome, Policy, Reply, REPLICAS};

/// What to do with one tick's result.
enum Action {
    /// Agreed by two or more replicas: may be used as a command.
    Command(u64),
    /// Self-check on the last replica: data product only.
    Data(u64),
    /// Nothing to send this tick.
    Hold,
}

fn gate(replies: &[Reply; REPLICAS]) -> Action {
    let verdict = decide(Policy::Shrink, replies);
    match (verdict.mode, verdict.outcome) {
        (Mode::Vote | Mode::Compare, Outcome::Deliver(x)) => Action::Command(x),
        (Mode::SelfCheck, Outcome::Deliver(x)) => Action::Data(x),
        _ => Action::Hold,
    }
}

fn main() {
    use Reply::{Absent, Pair, Single};
    let ticks = [
        [Single(7), Single(7), Single(9)], // vote: two agree on 7
        [Absent, Single(7), Single(7)],    // compare: both say 7
        [Absent, Single(7), Single(9)],    // compare: mismatch
        [Absent, Absent, Pair(7, 7)],      // self-check on the last replica
        [Absent, Absent, Absent],          // nothing left
    ];
    for replies in &ticks {
        match gate(replies) {
            Action::Command(x) => println!("{replies:?}: command {x}"),
            Action::Data(x) => println!("{replies:?}: data product {x}"),
            Action::Hold => println!("{replies:?}: hold"),
        }
    }
}
```

Its output, from `cargo run` against v0.3.1:

```
[Single(7), Single(7), Single(9)]: command 7
[Absent, Single(7), Single(7)]: command 7
[Absent, Single(7), Single(9)]: hold
[Absent, Absent, Pair(7, 7)]: data product 7
[Absent, Absent, Absent]: hold
```

## 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. `to_raw()` and `Health::from_raw(strikes, count)` turn the record into plain arrays and back, to save it across a reset or hand it to C.

From C or C++, use the [C interface](https://docs.mru.space/core/fprime/#c), `quorum.h`. Kani proves that `quorum_mode`, `quorum_decide`, `quorum_health_strike` and `quorum_health_clear` give this crate's answer.

## Kani proofs

Nine proofs: four on the core in `quorum`, five on the C interface in `quorum-ffi`. CI runs`cargo kani -p quorum -p quorum-ffi` on every change. In the core proofs, each reply is any of`Absent`, `Single` or `Pair`, with any `u64` values.

| Proof | Property | Scope |
| --- | --- | --- |
| [identical\_while\_tmr\_can\_run](https://github.com/mruspace/flight/blob/v0.3.1/quorum/src/lib.rs#L331) | With two or more replies present, both policies give the same outcome. | Every set of three replies with two or more present. Outcome only, not mode or `diagnose`. |
| [tmr\_stops\_below\_two](https://github.com/mruspace/flight/blob/v0.3.1/quorum/src/lib.rs#L343) | With fewer than two replies present, fixed TMR's outcome is `Halted`. | Every set of three replies with fewer than two present. |
| [shrink\_halts\_only\_with\_nothing\_left](https://github.com/mruspace/flight/blob/v0.3.1/quorum/src/lib.rs#L352) | The shrinking quorum's outcome is `Halted` if and only if no reply is present. | Every set of three replies. |
| [delivers\_only\_agreed\_values](https://github.com/mruspace/flight/blob/v0.3.1/quorum/src/lib.rs#L362) | A delivered value has two agreeing replies, or exactly one replica alive that returned `Pair(v, v)`. | Every set of three replies, under both policies. |
| [decide\_is\_the\_core](https://github.com/mruspace/flight/blob/v0.3.1/quorum-ffi/src/lib.rs#L314) | `quorum_decide` gives the core's verdict. An unknown reply kind counts as absent. | C interface: policy 0 or 1, any reply kind and values. |
| [bad\_policy\_halts](https://github.com/mruspace/flight/blob/v0.3.1/quorum-ffi/src/lib.rs#L330) | Any other policy code halts `quorum_decide` and `quorum_mode`. | C interface: any policy code above 1. |
| [mode\_is\_the\_core](https://github.com/mruspace/flight/blob/v0.3.1/quorum-ffi/src/lib.rs#L340) | `quorum_mode` gives the core's mode. | C interface: policy 0 or 1, any `u32` count. |
| [strike\_is\_the\_core](https://github.com/mruspace/flight/blob/v0.3.1/quorum-ffi/src/lib.rs#L359) | `quorum_health_strike` gives the core's answer and record. A replica above 2 changes nothing. | C interface: any record with counts in the `u32` range, any replica and cycle. |
| [clear\_is\_the\_core](https://github.com/mruspace/flight/blob/v0.3.1/quorum-ffi/src/lib.rs#L384) | `quorum_health_clear` gives the core's record. A replica above 2 changes nothing. | C interface: any record with counts in the `u32` range, any replica. |

Each proof name links to its source at v0.3.1.

### Not covered

-   **`Health` in the core.** Unit tests only.
-   **Diagnosis and the known-answer test.** They run in the demo and in F´, not in the core.
-   **Timing.** The proofs say what `decide()` returns, not how long it takes. The[bench](https://docs.mru.space/core/bench/#core) measures that.
-   **The system over a run.** Never less than fixed TMR over a whole run is tested, not proved. See[Tested (per run)](https://docs.mru.space/concepts/shrinking-quorum/#tested).

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

Updated 11 Oct 2026 · Source: quorum/src/lib.rs · [Edit on GitHub](https://github.com/mruspace/docs/edit/main/src/pages/core/quorum-crate.astro) · [Questions? Get in touch](https://mru.space/contact/)

---

# quorum CLI reference

URL: https://docs.mru.space/core/quorum-cli/

[Docs](https://docs.mru.space/) / [Core runtime](https://docs.mru.space/core/quorum-crate/) / quorum CLI

# The `quorum` program

Three replica processes, a voter built on the core, fault injection, and enforced resource limits. It reports what it delivered and what that cost.

## Synopsis

```
quorum [--policy shrink|tmr] [--ticks N] [--seed S]
   [--upset-rate R] [--common-mode C] [--kat-period P]
   [--fault kill|corrupt|stuck|hang|sensor:I@T | stuckbit:I@T/LOC.BIT.V] ... [--faults-file F]
   [--max-memory-mb M] [--max-cpu-seconds S] [--cpu-percent P]
   [--max-seconds S] [--reply-timeout-ms T]
   [--sensor-mb M] [--sensor-every N]
   [--log file.csv] [--progress-every N] [--summary file.txt]
   [--checkpoint file] [--checkpoint-every N]
```

An unknown option prints this list. Every run is reproducible from its seed.

## Run settings

| Option | Default | Meaning |
| --- | --- | --- |
| \--policy | shrink | `shrink` or `tmr` |
| \--ticks | 10000 | Results to compute |
| \--seed | 1 | Seed for random upsets and where they land |
| \--upset-rate | 0 | Chance per replica per tick of a bit flip in working memory |
| \--common-mode | 0.05 | Share of single-replica upsets that hit both self-check runs alike |
| \--kat-period | 64 | Ticks between known-answer tests on the last replica |

## Faults

Schedule a fault as `kind:replica@tick`. Repeat the option, or read a schedule with `--faults-file`.

| Kind | What happens |
| --- | --- |
| kill | The replica process dies. |
| hang | The replica stops answering. The voter drops it after the reply timeout. |
| stuck | The replica returns the same wrong value from then on. |
| corrupt | One bit flips in the replica's working memory during its next computation. (In v0.2.0, a corrupt fault on an odd tick in self-check mode was lost. Fixed in v0.3.0.) |
| stuckbit | `stuckbit:I@T/LOC.BIT.V`: from tick T, bit BIT of LOC is forced to V (0 or 1), in both self-check runs and in the known-answer test. LOC is `in` (the input, bits 0 to 63), `block` (the 4 KiB working block, bits 0 to 32767), `acc` (the hash accumulator, 0 to 63) or `out` (the result, 0 to 63). Added in v0.3.0. See [known-answer test coverage](https://docs.mru.space/core/bench/#kat). |
| sensor | A flip in the radiation-sensor block, to test logging and repair. Needs `--sensor-mb`. The replica number is ignored. |

## Limits

Safe on shared hardware. Each process enforces its own memory and CPU-time limits. The voter enforces the CPU share and the run time.

| Option | Default | Meaning |
| --- | --- | --- |
| \--max-memory-mb | 128 | Memory limit per process (Linux only) |
| \--max-cpu-seconds | off | CPU-time limit per process |
| \--cpu-percent | off | Cap on the voter's CPU share |
| \--max-seconds | off | Maximum run time |
| \--reply-timeout-ms | 2000 | Drop a replica that does not answer in time |

## Radiation sensor

`--sensor-mb M` holds M MB of memory in a known pattern and checks it every `--sensor-every` ticks (default 1000). Every flipped bit is logged with its location, then repaired. On flight hardware, this measures the real upset rate. It must leave at least 32 MB under `--max-memory-mb`. In orbit it found one flip, the injected self-test, and no real upset.

## Output

`--log file.csv` writes every event: stuck, hang, lost, retired, cleared, killed, detected, wrong, stopped, halted and sensor flips. `--progress-every N` adds running totals. `--summary file.txt` writes the final report for downlink.

The run from the [Quickstart](https://docs.mru.space/#quickstart), `--policy shrink --ticks 20000 --seed 1 --upset-rate 0.001 --fault kill:0@5000 --fault kill:1@10000`, prints:

```
policy=shrink ticks=20000 seed=1 upset_rate=0.001
useful=14989 detected=11 wrong=0 halted_at=never alive_at_end=1 stopped=completed last_useful=20000 kat_tests=174
footprint: voter_max_rss=1936KiB replica_max_rss=1824KiB cpu=0.429s wall=0.420s
limits: memory=128MB/process cpu_time=none cpu_share=none max_run=none reply_timeout=2000ms
```

flight v0.3.1 on an Apple M4. The footprint line varies by host.

`last_useful` is the tick of the last correct result. With a scheduled stuck, hang or corrupt fault, the output adds a `detection:` line (also for `stuckbit`, since v0.3.0): the faults injected, how many the voter caught, and the mean and longest ticks from fault to first reaction. The [bench](https://docs.mru.space/core/bench/) runs this program over a matrix of faults.

## Resets and power cuts

`--checkpoint file` saves the run's state every `--checkpoint-every` ticks (default 100). The voter writes a new file, flushes it to storage and renames it over the old one, so a power cut leaves either the old checkpoint or the new one. It writes out and syncs the event log first.

After a reset, the same command resumes from the checkpoint. Dead, stuck and hung replicas stay that way. The ticks after the last checkpoint run again and give the same results, so the run ends with the same counts as one that was never interrupted. A `resumed` line in the log marks where it picked up. A checkpoint from a run with other options is refused. A finished run removes its checkpoint.

The scenario checks test this on every change: they kill the voter with `kill -9` in the middle of a run and compare the counts. `scripts/board.sh` runs the same test on a board, with reboots or power cuts.

## On OPS-SAT

For experiment exp4051 on ESA's OPS-SAT PRETTY satellite, run by ESA's OPS-SAT Space Lab and TU Graz. The same v0.3.1 package ran in orbit on 18 October 2026 at 09:45 UTC, after ESA's software environment test (15 October) and the TU Graz FlatSat test (16 October). Results matched the prediction written before the run: 227 s in total, both runs exit 0, every fault on its scheduled tick, the shrinking quorum 2,745 correct and 0 wrong over 5,250 ticks, fixed TMR 239 correct then a detected disagreement on every tick to 4,500. Three software replicas on one processor in user space, scheduled faults, no real upset in the window; not a hardware-redundancy test.

| Run | Host | Shrinking quorum | Fixed TMR | Total | Exit |
| --- | --- | --- | --- | --- | --- |
| Software environment, 15 Oct 2026 | ESA Linux VM, ARMv8, two cores | 14,886 correct, 0 wrong, 29,532 ticks | 239 correct, detected to tick 19,250 | 222 s | 0, 0 |
| FlatSat, 16 Oct 2026 | SEPP, Cortex-A9, TU Graz | 2,745 correct, 0 wrong, 5,250 ticks | 239 correct, detected to tick 4,778 | 224 s | 0, 0 |
| In orbit, 18 Oct 2026 | SEPP, Cortex-A9, OPS-SAT PRETTY | 2,745 correct, 0 wrong, 5,250 ticks | 239 correct, detected to tick 4,500 | 227 s | 0, 0 |

Counts from the summary files and totals from the start and end times in run-info.txt, in the[result files](https://github.com/mruspace/flight/tree/main/opssat/results). The same binary ran on all three hosts; the software environment is a Linux VM, not the flight processor. Fixed TMR delivered 0 wrong results on every host; its last correct result is tick 239, then a detected disagreement on each tick to the tick shown. Both runs overran the 110 s cap by about 3 s because the limit is checked once per tick and the last tick was a 64 MB scan; fixed in v0.4.0, where the scan checks the limit every 1 MiB and the sleep stops at the cap.

On the flight processor at the 5% CPU share the voter made about 45 ticks per second on the FlatSat, and in orbit about 46 for the shrinking quorum and 40 for fixed TMR ([operations note](https://github.com/mruspace/flight/blob/main/docs/opssat.md)). `opssat/run` is the entry point the OPS-SAT runner executes: the shrinking quorum and fixed TMR one after the other, same seed and fault schedule, all output in a folder for downlink, finished inside a five-minute window. `opssat/package.sh` builds the package from a checksum-verified release binary. `opssat/run.sh` starts, checks and stops a long run on any Linux system. Tagged releases ship each static Linux binary (three ARM, one x86\_64) with both launchers, the fault schedules and the operations note.

Updated 19 Oct 2026 · Source: demo/src/main.rs · [Edit on GitHub](https://github.com/mruspace/docs/edit/main/src/pages/core/quorum-cli.astro) · [Questions? Get in touch](https://mru.space/contact/)

---

# F´ components for the shrinking quorum

URL: https://docs.mru.space/core/fprime/

[Docs](https://docs.mru.space/) / [Core runtime](https://docs.mru.space/core/quorum-crate/) / F´ components

# F´ components

Layer 1 as components for NASA JPL's F´ framework, version 4.4.1. Every decision comes from the [`quorum` crate](https://docs.mru.space/core/quorum-crate/), through a C interface that Kani proves equal to it.

F´ v4.4.1 C++14 45 unit tests v0.7.0

The source is in [fprime/](https://github.com/mruspace/flight/blob/v0.7.0/fprime) of mruspace/flight. The requirements and the design were written and approved in F´'s own order, requirements first, then the model, then the code: [requirements](https://github.com/mruspace/flight/blob/v0.7.0/docs/fprime-requirements.md), [design and results](https://github.com/mruspace/flight/blob/v0.7.0/docs/fprime-design-fpp.md).

## Components

| Component | Kind | What it does |
| --- | --- | --- |
| `RedundancyManager` | active | Asks the replicas for a result each cycle, decides with the core, delivers or rejects, steps the mode down as replicas are lost, and runs known-answer tests. |
| `HealthRegistry` | passive | Holds the strike record per replica: three outvotes within 200 cycles start a diagnosis. |
| `ReplicaHost` | active, one per replica | Runs the payload and answers requests and known-answer tests. A disabled host does not answer. |
| `FaultInjector` | passive, test builds only | Sits between the manager and the replicas in a test topology: silence (kill, hang), a stuck value, and bit flips in a replica's working memory, with the same random upsets as the demo for a seed. |
| `RunRecorder` | passive, test builds only | Stands in for the ground in an experiment: checks every delivered result against the payload computed without a fault, counts correct and wrong results, and reads the manager's last telemetry for the summary. The manager never sees it. |

In a flight topology the manager connects to the replicas directly, so no test code is in the flight path.

The replicas run as three threads of one deployment. Three processes, and then separate processors, use the same components.

## RedundancyManager

| Element | Name |
| --- | --- |
| Input ports | `schedIn` (rate group, once per cycle), `replyIn[3]`, `pingIn` |
| Output ports | `requestOut[3]`, `enableOut[3]`, `resultOut`, `healthStrike`, `healthClear`, `pingOut` |
| Commands | `SET_POLICY`, `STANDBY_REPLICA`, `ADMIT_REPLICA` |
| Parameters | `KatPeriod` (64 cycles), `StateSavePeriod` (1,000 cycles; 0 saves on change only) |
| Telemetry | `CurrentPolicy`, `CurrentMode`, `LiveReplicas`, `Retired`, `Slots` on change; `Delivered`, `Caught` each cycle |
| Events | Mode changes, caught disagreements (throttled), diagnoses, retirements with their reason, standby and admission, the state file, and the halt |

The full model: RedundancyManager.fpp in fprime/Mru/Components/RedundancyManager.

A replica is retired when its known-answer result is wrong or missing, or after three missed cycles in a row. The event gives the reason: a diagnosis that failed or was not answered, a periodic test on the last replica that failed or was not answered, or lost.

F´ returns 0 for a parameter that was never loaded. The manager then uses the model's defaults, so a topology that skips `loadParameters()` does not run the known-answer test every cycle.

## Spares and standby

Each of the three slots is ACTIVE, STANDBY or RETIRED. Only ACTIVE slots get requests. These follow section 8 of the [whitepaper](https://mru.space/mru-whitepaper.pdf), where salvaged processors join as spares and declining nodes are set aside.

-   **STANDBY\_REPLICA** disables an ACTIVE slot to save power. It is refused if the policy could not run on the slots left. A power accountant will use it; that accountant is not built.
-   **ADMIT\_REPLICA** enables a STANDBY slot, or new hardware in a RETIRED slot, and asks for its known answer. The slot becomes ACTIVE only if the right answer arrives by the end of the next cycle.

## Resets

The manager saves the policy, the slot states and the cycle counter when one of them changes, and every `StateSavePeriod` cycles. The record is 21 bytes with a CRC-32. It writes a new file, flushes it and renames it over the old one, so a power cut leaves the old state or the new one. At start it restores a valid file and reports it, or starts with all slots ACTIVE and warns. Strikes are not saved: after a reset each replica starts a fresh window.

## Deployment

`MruOpsSat` is the first F´ deployment of the components. It runs them with F´'s own services: the command dispatcher, the event manager, the telemetry database, health pings and a command sequencer (the `CdhCore` subtopology), driven by a Linux timer every 100 ms. The faults and the policy come from F´ command sequences, as an operator would send them. It has no communications stack: events are written as text lines and the summary as a file.

It is built as a static, optimized 32-bit ARM binary for the SEPP, the Cortex-A9 payload processor of OPS-SAT PRETTY. In ESA's OPS-SAT experiment environment, on a laptop under emulation, the package ran full length on 22 Oct 2026: 148 seconds, 0 wrong results, the counts of the demo within the system test's rule, a restore from the state file after a kill, and 1.2% to 1.5% CPU in the timed run. It has not run on the SEPP. See [the operations note](https://github.com/mruspace/flight/blob/v0.7.0/docs/opssat.md).

A second deployment puts each replica in a process of its own: `MruQuorum`, the manager process, starts three `MruReplica` processes, linked through F´'s GenericHub over Unix socket pairs (no network), and pins them to the SEPP's two cores. The kill is real: the manager sends SIGKILL to a replica process at the start of a cycle. In ESA's environment under emulation it gave the same counts and events as the first deployment, with the three processes pinned in every segment. It has not run on the SEPP.

On one processor the manager and the replicas share the processor. A manager that falls behind used to close cycles before their answers were dispatched, so healthy replicas looked silent and were retired as lost. Since v0.6.0 a cycle that closes late, with other messages still in the manager's queue or every expected answer missing at once, counts against no replica; with an answer missing it is withheld and counted (MRU-RM-023). In a container starved of processor time, the old rule halted 9 of 15 runs and the new one none; no run gave a wrong result.

## One cycle

The order follows a tick of the demo, so the same seed gives the same counts:

-   **Close the last cycle.** Decide it if it is not yet decided, with a missing reply as absent. Count missed replies, and fail tests that had a full cycle to answer.
-   **Start the next.** Ask every ACTIVE slot. On the last replica, ask for two results on even cycles only, and add the known-answer test every `KatPeriod` cycles.
-   **Decide as soon as every answer is in.** Strikes, the test of two disagreeing replicas, and the periodic test follow at once.

A replica that dies stops answering, so the manager finds the death by silence. When a death leaves one replica, the cycles until it is marked lost end as caught disagreements. The demo kills its replicas itself and knows at once; this is the one place the counts differ.

## C interface

`quorum-ffi` builds the core as a `no_std` static library with a C header, [quorum.h](https://github.com/mruspace/flight/blob/v0.7.0/quorum-ffi/include/quorum.h). It is not tied to F´: any C or C++ framework can use it.

```
uint8_t quorum_mode(uint8_t policy, uint32_t alive);
quorum_verdict quorum_decide(uint8_t policy, const quorum_reply *replies);
void quorum_health_init(quorum_health *health);
bool quorum_health_strike(quorum_health *health, uint32_t replica, uint64_t cycle);
void quorum_health_clear(quorum_health *health, uint32_t replica);
```

Only plain values cross. The health record lives in the caller's memory. Out-of-range input gets the safe answer: a policy that is not 0 or 1 halts, an unknown reply kind counts as absent, a replica above 2 changes nothing, and a null pointer does the same. Five Kani proofs show that `quorum_mode`, `quorum_decide`, `quorum_health_strike` and `quorum_health_clear` give the core's answer for every valid input, and the safe answer for a bad policy, an unknown reply kind or a replica above 2. Unit tests check the null pointers. See [Kani proofs](https://docs.mru.space/core/quorum-crate/#proofs).

## Verification

| Check | Result |
| --- | --- |
| Kani, core and C interface | 9 of 9 proofs |
| C test of quorum.h | Sizes, layout and known cases pass |
| F´ unit tests | 44, by requirement: HealthRegistry 5, ReplicaHost 5, FaultInjector 8, RedundancyManager 23, RunRecorder 4. Built with address and undefined-behavior sanitizers. |
| System test against the demo | 60 cases: the five [bench](https://docs.mru.space/core/bench/) schedules, both policies, three upset rates, two seeds, 4,000 cycles. 36 identical to the demo. In the other 24, a kill that leaves one replica costs 2 correct results and adds 3 caught disagreements. Wrong results are identical in all 60. |
| Deployment against the demo | The `MruOpsSat` package with short caps: each segment's counts against the demo on the same faults, the events on their cycles, the restore from the state file, and a second run in the same folder. |

All of these run in CI on every change. The expected counts are written by the demo itself, and CI checks they are current.

## Build and test

```
# in a clone of mruspace/flight
git submodule update --init --recursive
cd fprime
python3 -m venv fprime-venv && . fprime-venv/bin/activate
pip install -r requirements.txt
fprime-util generate && fprime-util build
fprime-util generate --ut && fprime-util check --all
# the deployment, from the repository root, in the build container
cd .. && ./opssat/fprime/build.sh  # static 32-bit ARM build and its sequences
```

The build calls `cargo` to compile the core, so it needs a Rust toolchain. On macOS 27, the CMake that F´ v4.4.1 pins fails; CMake 4.4 works. Linux works with the pinned version.

## Limits

-   **Not on flight hardware.** The components run in tests and in the deployment on general-purpose processors, the ARM build under emulation. The OPS-SAT run used the quorum demo, not these components, so they stay at Prototype in the [architecture status](https://docs.mru.space/concepts/architecture/).
-   **No ground link yet.** The first deployment has no communications stack. A deployment with commands and telemetry from the ground is planned.
-   **Not built:** the retry of a cycle after a disagreement on two replicas (the whitepaper's "dual with checkpointing"), the health score by error rate and response time, the power accountant, and memory scrubbing.

Updated 19 Oct 2026 · Source: fprime/Mru/Components · [Edit on GitHub](https://github.com/mruspace/docs/edit/main/src/pages/core/fprime.astro) · [Questions? Get in touch](https://mru.space/contact/)

---

# Bench results for Layer 1

URL: https://docs.mru.space/core/bench/

[Docs](https://docs.mru.space/) / [Core runtime](https://docs.mru.space/core/quorum-crate/) / Bench

# Bench

Layer 1 measured on real processors with injected faults: the shrinking quorum against fixed TMR, on the same faults, over 300 runs per host.

Every number on this page comes from `scripts/bench.sh` in [mruspace/flight](https://github.com/mruspace/flight), run on the hosts listed under [Hosts](https://docs.mru.space/core/bench/#hosts). The raw results, one JSON and one CSV file per host, are in [bench/results](https://github.com/mruspace/flight/tree/main/bench/results). This is lab evidence on general-purpose processors. It is not radiation testing and not flight data. See [Limits](https://docs.mru.space/core/bench/#limits).

## Method

Each run starts the [quorum program](https://docs.mru.space/core/quorum-cli/): three replica processes and a voter. Every decision comes from the [`quorum` crate](https://docs.mru.space/core/quorum-crate/), the same `no_std` code meant for flight. Each tick, the replicas hash a 4 KiB block of working memory. An upset flips one bit in that block during the computation, so the fault travels through the real calculation.

The bench runs every combination of:

-   **Policy:** fixed TMR and the shrinking quorum, on the same seed and faults.
-   **Seed:** 1 to 10. The seed sets where and when upsets land.
-   **Upset rate:** 0.0001, 0.001 and 0.01, the chance per replica per tick of a bit flip.
-   **Fault schedule:** five schedules, below.

Each run is 20,000 ticks. That makes 300 runs per host.

| Schedule | Faults (tick) | What it tests |
| --- | --- | --- |
| none | Upsets only | Voting masks random upsets. |
| staggered-kills | Replica 0 dies at 5,000, replica 1 at 10,000 | Loss of two replicas, one at a time. |
| common-mode | Replica 0 dies at 2,000, replica 1 at 4,000 | Self-check on the last replica for 80% of the run. An upset can hit both of its runs alike (share 0.05). |
| stuck | Replica 1 stuck at 4,000, replica 0 dies at 9,000 | A replica that returns the same wrong value, found by health scoring. |
| last-stuck | Replicas 0 and 1 die at 5,000 and 10,000, replica 2 stuck at 15,000 | A stuck fault on the last replica, found only by the periodic known-answer test. |

Known-answer test on the last replica every 64 ticks. Common-mode share 0.05. Both are the program's defaults.

## Metrics

Section 14 of the [whitepaper](https://mru.space/mru-whitepaper.pdf) names six metrics. A run of three processes supports three of them, plus two measures of its own.

| Metric | How the bench measures it |
| --- | --- |
| Mission Score | Correct results: ticks that delivered the right value. |
| Survival Duration | The tick of the last correct result. |
| Graceful Degradation Index | Correct results divided by capacity. Capacity is the most a checked design can deliver on the replicas still healthy at each tick: one result per tick with two or more, one every other tick with one (it must compute twice to check itself). 1.0 means every healthy replica did useful work. |
| Wrong results | Delivered values that were not correct. Nothing flagged them. |
| Detection latency | Ticks from a stuck, hang or corrupt fault to the voter's first reaction to that replica: an outvote, a caught disagreement, or its removal. |

Energy Efficiency, Decision Quality and Thermal Compliance need power, science and thermal models. The bench does not measure them.

## Results

At an upset rate of 0.001, mean of 10 seeds. The ratio column gives the mean, and the lowest single seed in brackets.

| Schedule | Correct, TMR | Correct, shrink | Shrink / TMR | GDI, TMR | GDI, shrink |
| --- | --- | --- | --- | --- | --- |
| none | 19,999.9 | 19,999.9 | 1.00 (1.00) | 1.000 | 1.000 |
| staggered-kills | 9,988.5 | 14,985.0 | 1.50 (1.50) | 0.666 | 0.999 |
| common-mode | 3,994.7 | 11,987.3 | 3.00 (3.00) | 0.333 | 0.999 |
| stuck | 8,989.5 | 14,483.8 | 1.61 (1.61) | 0.620 | 0.999 |
| last-stuck | 9,988.5 | 12,486.2 | 1.25 (1.25) | 0.799 | 0.999 |

20,000 ticks per run. Results for all three upset rates are in the JSON files.

In all 150 pairs of runs, the shrinking quorum delivered at least as many correct results as fixed TMR on the same seed and faults. This is a test result over these runs, not a proof. On the same replies, both policies give the same outcome each tick, as the [Kani proofs](https://docs.mru.space/core/quorum-crate/#proofs) show. The runs differ because the shrinking quorum keeps going and retires bad replicas: TMR halts at the second loss, or, in the stuck schedule, keeps comparing a good replica with a stuck one and rejects every result.

## Wrong results

Fixed TMR delivered no wrong result in any run. It stops instead. The shrinking quorum pays for its extra work with a small number of wrong results on its last replica. The table gives the mean per run.

| Schedule | Upset rate 0.0001 | 0.001 | 0.01 |
| --- | --- | --- | --- |
| none | 0 | 0 | 0 |
| staggered-kills | 0 | 0.3 | 1.7 |
| common-mode | 0 | 0.3 | 3.6 |
| stuck | 0 | 0.2 | 1.7 |
| last-stuck | 20.0 | 20.1 | 20.7 |

Shrinking quorum, mean of 10 seeds per cell, 20,000 ticks per run.

There are two sources:

-   **Common-mode upsets in self-check.** An upset that hits both runs alike gives two equal wrong values. The count follows the model: in the common-mode schedule at 0.01, about 8,000 self-checked results, 80 upsets and a share of 0.05 give 4.0 expected. The bench measured 3.6.
-   **A stuck last replica.** Self-check cannot see a fault that gives the same wrong value twice. Only the known-answer test finds it. In last-stuck, the fault came at tick 15,000 and the test caught it at 15,040, after 20 wrong results. The run then stopped.

## Survival and detection

| Schedule | Last correct result, TMR | Last correct result, shrink | Detection latency |
| --- | --- | --- | --- |
| staggered-kills | 9,999 | 20,000 | None to detect: the voter injects kills itself |
| common-mode | 3,999 | 20,000 | As above |
| stuck | 8,999 | 20,000 | 0 ticks |
| last-stuck | 9,999 | 14,998 | 40 ticks |

Upset rate 0.001, mean of 10 seeds. Runs end at tick 20,000. At 0.01, two shrinking-quorum runs caught a disagreement on the last tick, so their last correct result was tick 19,998.

With three replicas, a stuck replica is outvoted on the tick it fails, and health scoring retires it two ticks later. On the last replica, detection waits for the next known-answer test, at most 64 ticks. A shorter `--kat-period` gives fewer wrong results and less throughput.

## Known-answer test coverage

On the last replica, self-check cannot see a fault that gives the same wrong answer twice. Only the periodic known-answer test can catch it, and only if the fault changes the test's answer. `scripts/kat-coverage.sh` measures this: it kills two replicas, injects one fault into the last one, and records whether the voter caught it, how fast, and how many wrong results got out first. Results: [2026-10-11-darwin-arm64-kat.json](https://github.com/mruspace/flight/blob/main/bench/results/2026-10-11-darwin-arm64-kat.json).

Scope. These figures come from the demo task on a general-purpose processor: three replica processes on one host, each hashing a 4 KiB block with FNV-1a, with faults the voter injects by command. The test sends one input (tick 0) and compares one 64-bit result. The fractions are properties of that task, that input and this fault model. They are not properties of flight hardware or of any flight software. A stuck-at bit is one bit of the input, the working block, the hash accumulator or the result, forced to 0 or 1 from a chosen tick. A bit flip changes one bit of the working block during one computation. The campaign does not cover faults in the voter, the operating system or the links between processes. It is not a radiation test, and the F´ components do not model stuck-at bits.

| Fault on the last replica | Faults | Detected | Ticks to detect, mean (max) | Wrong before detection, mean (max) | Missed, wrong results | Missed, no effect |
| --- | --- | --- | --- | --- | --- | --- |
| Stuck result (same wrong value every time) | 256 | 100% | 31.5 (63) | 15.5 (31) | 0 | 0 |
| Hang | 64 | 100% | 0.5 (1) | 0 (0) | 0 | 0 |
| Stuck-at bit in the result | 128 | 50% | 31.5 (63) | 7.9 (17) | 64 | 0 |
| Stuck-at bit in the hash accumulator | 128 | 98% | 31.8 (63) | 15.6 (31) | 2 | 0 |
| Stuck-at bit in the working block (128 of 65,536) | 128 | 46% | 32.9 (62) | 8.2 (18) | 69 | 0 |
| Stuck-at bit in the input | 128 | 50% | 31.5 (63) | 15.2 (31) | 10 | 54 |
| Bit flip in working memory, common-mode share 0 | 400 | 100% | 0 (0) | 0 (0) | 0 | 0 |
| Bit flip, common-mode share 0.05 | 400 | 94% | 0 (0) | 0 (0) | 23 | 0 |
| Bit flip, common-mode share 0.2 | 400 | 79% | 0 (0) | 0 (0) | 84 | 0 |

Test every 64 ticks. Missed, wrong results: the test never caught the fault and wrong results were delivered. Missed, no effect: the fault changed nothing in the run. Bit flips are caught by self-check, not by the known-answer test; the share is the chance that both runs get the same flip.

-   **One test input sees about half of the stuck-at bits.** A stuck bit shows only when it changes the answer to the one test input. A stuck-at-0 bit on the input never does, because the input is 0. The input faults marked "no effect" changed nothing only because these short runs never set those bits.
-   **A missed stuck-at bit keeps delivering wrong results.** For a stuck bit in the result, about half of all later results are wrong, and nothing flags them.
-   **Fix, planned:** a second test input would make most of these visible. It is not built.

### Test period

| Period, ticks | Stuck results detected | Ticks to detect, mean (max) | Wrong before detection, mean (max) | Tests per delivered result | Extra CPU, measured (median) |
| --- | --- | --- | --- | --- | --- |
| 8 | 100% | 3.5 (7) | 1.5 (3) | 0.2499 | 22.1% |
| 16 | 100% | 7.5 (15) | 3.5 (7) | 0.1250 | 10.4% |
| 32 | 100% | 15.5 (31) | 7.5 (15) | 0.0625 | 4.4% |
| 64 | 100% | 31.5 (63) | 15.5 (31) | 0.0312 | 1.9% |
| 128 | 100% | 63.5 (127) | 31.5 (63) | 0.0156 | 0.4% |
| 256 | 100% | 127.5 (255) | 63.5 (127) | 0.0078 | 1.5% |

Stuck results: 256 per period, one for every phase of the test. The test count is exact. The CPU column is the median of 10 runs of 100,000 ticks against the same runs with no test, on one host. It includes the request round trip, so it is above the share of extra computations. From period 32 up, it is smaller than the run-to-run spread (about 6% of the median): read it as a few percent at most, not a precise value.

## Cost of the core

The `bench` crate times `quorum::decide()` and `Health::strike()` with `std::time::Instant`: the median of 9 rounds of 2,000,000 calls. Each figure includes the loop and the copy of the replies, so it is an upper bound.

| Host | decide(), per call | Health::strike(), per call |
| --- | --- | --- |
| Apple M4 | 2.45 to 3.24 ns | 1.33 ns |
| Arm Neoverse-N2 | 2.51 to 4.41 ns | 3.40 ns |
| AMD EPYC 7763 | 3.79 to 7.63 ns | 6.15 ns |

The range covers all six input cases and both policies. Per-case figures are in the JSON files. On the shared CI machines, two runs of the same code differed by up to 10%.

Built for a bare-metal ARM Cortex-M target (`thumbv7em-none-eabihf`), the core is 902 bytes of code with rustc 1.99.0, and 1,178 bytes with rustc 1.86.0. In the runs, no process used more than 2.1 MB of memory.

## Hosts

The same 300 runs on three hosts gave the same counts, run for run. Only the timing differs. In CI, the static ARM binaries also run a short bench under emulation (64-bit ARM, and 32-bit ARM with hard and soft float), and the build fails if any count differs from a native run.

| Processor | System | Compiler | Results file |
| --- | --- | --- | --- |
| Apple M4 | macOS, Darwin 27.0 | rustc 1.86.0 | 2026-10-11-darwin-arm64 |
| Arm Neoverse-N2 | Linux 6.17, GitHub Actions ubuntu-24.04-arm | rustc 1.99.0 | 2026-10-11-linux-aarch64 |
| AMD EPYC 7763 | Linux 6.17, GitHub Actions ubuntu-latest | rustc 1.99.0 | 2026-10-11-linux-x86\_64 |

Release build: lto = true, codegen-units = 1. Each file records the commit it ran.

## Limits

-   **Not radiation.** Upsets are bit flips that the voter injects at chosen rates. The rates are test settings, not a model of any orbit.
-   **Not target hardware.** The bench hosts are general-purpose processors. The quorum demo has run on a flight processor, on the OPS-SAT FlatSat and in orbit, but this bench has not. See the [architecture status](https://docs.mru.space/concepts/architecture/).
-   **Processes, not separate processors.** The three replicas share one processor and one memory. A real failure can take more than one of them at once.
-   **Chosen faults.** The five schedules set when replicas fail. Failure times in a real mission are random. For statistics over thousands of missions, see [Dusk](https://docs.mru.space/simulation/dusk/).
-   **Short runs.** 20,000 ticks per run. The bench does not model aging, power or temperature.

## Run it

```
# in a clone of mruspace/flight
./scripts/bench.sh           # 300 runs, about 3 minutes on an Apple M4
./scripts/bench.sh --quick   # 2 seeds, 5,000 ticks, about 15 s
cargo run --release -p bench # the cost of the core only
```

The script writes `bench/results/<date>-<host>.json` and `.csv`, with the host, processor, commit and build flags. The same seeds give the same counts on every run.

## Model check

`dusk --bench` replays these schedules through [Dusk](https://docs.mru.space/simulation/dusk/)'s policy model with the same deaths, upset rate and self-check coverage, and compares the means. On each host's results, 17 of 18 rows agree within 3 standard errors on both correct and wrong results. The 18th, the shrinking quorum's correct results in the common-mode schedule at 0.01, is 3.4 standard errors low. Its two phases, rerun over 200 seeds, matched the model: 40.38 results lost against 40.42 expected with two replicas, and 19.17 caught and 0.90 wrong against 19.00 and 1.00 with one.

This checks the policy model against the code. It does not calibrate the environment: the bench sets the upset rate and the failure times itself. The stuck and last-stuck schedules are not modeled, because Dusk has only processors that die, not ones that return wrong values.

## What comes next

-   **Flight-class boards.** The same bench on target-class processors, with reboots and power cuts. The scripts and procedure are in [docs/board.md](https://github.com/mruspace/flight/blob/main/docs/board.md). No `scripts/board.sh` run has been done yet; the OPS-SAT package ran on the FlatSat and in orbit without reboots or power cuts.
-   **Calibrate Dusk's environment** with real upset and failure data, from a radiation beam test or from flight.

Updated 19 Oct 2026 · Source: scripts/bench.sh · [Edit on GitHub](https://github.com/mruspace/docs/edit/main/src/pages/core/bench.astro) · [Questions? Get in touch](https://mru.space/contact/)

---

# Dusk simulator reference

URL: https://docs.mru.space/simulation/dusk/

[Docs](https://docs.mru.space/) / [Simulation](https://docs.mru.space/simulation/dusk/) / Dusk

# Dusk

A Monte Carlo of redundancy policies on hardware that only ever decays. It asks what a shrinking quorum buys, and what it costs, on the same simulated hardware.

Rust no dependencies deterministic per seed [dusk.mru.space ↗](https://dusk.mru.space/)

## Run it

```
cargo run --release --bin dusk                 # the default scenario, about 2 s
cargo run --release --bin dusk -- --spares 2   # add salvaged processors
cargo run --release --bin dusk -- --sweep      # sensitivity and cold standby, about 2 minutes
cargo run --release --bin dusk -- --ground     # against TMR with a ground team, about 12 s
cargo run --release --bin charts               # redraw the charts and data.json, about 2 minutes
```

The package has two programs. `dusk` is the default, and `--bin charts` redraws the charts. Times are for an Apple M4 with 10 cores. Results depend only on the seed, never on the thread count.

## Options

| Option | Default | Meaning |
| --- | --- | --- |
| \--runs | 10000 | Missions per policy |
| \--seed | 1 | Base seed |
| \--threads | all cores | Worker threads |
| \--horizon-years | 1000 | Mission horizon |
| \--nodes | 3 | Processors at launch |
| \--spares | 0 | Salvaged processors |
| \--shape | 1.5 | Weibull shape |
| \--scale-years | 125 | Weibull scale |
| \--p-corr | 0.1 | Chance a death kills another |
| \--p-upset | 0.001 | Bad-result upsets per node-day |
| \--coverage | 0.99 | Lone self-check coverage |
| \--selfcheck-throughput | 0.5 | Lone output vs a vote |
| \--cold-aging | 0.1 and 1.0 | How fast an unpowered spare ages, relative to a powered one. The report shows both ends; give a value to show one. |

## The fault model

Each mission is a day-by-day fault-injection run.

-   **Processors die** on a Weibull lifetime. Shape 1.5 and a 125-year scale give a median life of about 98 years.
-   **Deaths can be correlated.** With probability `p_corr`, a death also kills one other processor that day.
-   **Spares are salvaged** from instruments as they die, already aged by the same radiation.
-   **Upsets corrupt a day's result**, at the rate that gets past EDAC and scrubbing.
-   **The comparison is paired.** Every policy sees the same fault history, so any difference is the policy.

## Default results

```
policy                     useful      p10      p50      p90      service   wrong days     risk
                           mean y                                  mean y   mean / run   P(>=1)
fixed TMR                    99.0     37.6     92.7    168.9         99.0        0.000     0.0%
standby simplex              83.1     38.4     78.3    134.0        166.4        0.603    43.2%
shrinking quorum            132.6     64.3    126.6    208.3        166.4        0.246    20.1%
TMR + unchecked simplex     166.2     76.9    156.7    267.9        166.4       24.715    87.2%
cold standby, aging 0.1     144.7     69.7    139.3    226.7        289.8        1.043    61.3%
cold standby, aging 1.0      83.1     38.4     78.3    134.0        166.4        0.603    43.2%
```

1.34× the useful work of fixed TMR in total (95% CI 1.33× to 1.35×). This assumes no ground support after launch. The gain falls to 1.00× when support never ends. See [Ground support](https://docs.mru.space/simulation/dusk/#ground). Never less on any single mission, by construction: the two policies are identical until fixed TMR stops. Fixed TMR comes out ahead only if one wrong result costs more than 136 years of useful work (95% CI 131 to 142), next to a risk of 20.1% against 0.0%.

Cold standby is the nearest model here of dual-string with autonomous switchover. Standby simplex is the same design with spares that age as fast as a powered processor, so it equals cold standby at aging 1.0. See [Baselines](https://docs.mru.space/simulation/dusk/#baselines).

## What the columns mean

Each mission runs one day at a time. On each day the policy runs in one mode, set by the number of live processors, and the lowest-numbered live processors do the work. These are the definitions in `src/model.rs`.

-   **Useful.** The sum over days of throughput credit for a correct delivered result: 1.0 for a vote day with at most one upset, 1.0 for a pair day with no upset, 0.5 (`--selfcheck-throughput`) for a single self-check day with no upset, 1.0 for an unchecked day with no upset, and 0 for lost, wrong and idle days. Shown as the mean in years, with the 10th, 50th and 90th percentiles.
-   **Service.** The first day the policy can never produce output again, or the horizon. For fixed TMR, the first day with fewer than two live processors. For the others, the first day with none left. The model ends the run that day, so a spare due to join later is not used. Shown as the mean in years.
-   **Wrong days.** Days whose delivered result was corrupted by an upset that nothing caught. One day is one result. Only a lone processor can make one: its self-check misses an upset with probability 1 minus `--coverage`, and an unchecked processor delivers every upset. Shown as the mean per mission.
-   **Risk.** The share of missions with at least one wrong day, with a paired bootstrap 95% CI.

A vote day with two or more upsets and a pair day with any upset are lost: the policy catches the disagreement and delivers nothing.

## Baselines

Fixed TMR is one baseline, not what most spacecraft fly. Two more act with no ground team, on the same fault histories.

-   **TMR + unchecked simplex** steps down on its own, but its last processor does not check itself. It isolates the value of self-check. The shrinking quorum does 80% of its useful work and makes 1.00% of its wrong results (95% CI 0.96% to 1.04%). Risk: 87.2% against 20.1%.
-   **Cold standby** keeps one processor powered and switches on the next, in order, when it dies. The active one self-checks. Here it has three strings, on the same hardware as TMR. Correlated deaths follow the powered fault history, which slightly under-counts them for an unpowered spare.

How fast an unpowered spare ages is not known, so `--sweep` varies it from 0.1 to 1.0 of the powered rate. Against cold standby, the shrinking quorum does 0.92× the useful work at 0.1 (95% CI 0.91× to 0.92×) and 1.60× at 1.0 (95% CI 1.59× to 1.60×). Cold standby does more useful work below an aging rate of about 0.20. At every rate it has more missions with a wrong result: 43.2% to 61.3%, against 20.1%. With two strings (`--nodes 2`), the shrinking quorum does 1.05× to 1.49× the useful work of cold standby.

## Sweeps

`--sweep` varies each parameter the model cannot pin down. Across every row, the gain over fixed TMR is 1.11× to 1.68×. Every row assumes no ground support after launch.

## Ground support

The 1.34× above assumes no ground support after launch. `--ground` compares the shrinking quorum with fixed TMR plus a ground team. When TMR drops to one processor, the team commands it into self-check after an answer time, if support has not ended. The gain falls as support lasts longer:

```
10000 missions, seed 1; shrinking quorum's useful work vs TMR + ground fallback

ground support ends        1 day   30 days  180 days   95% CI at 30 days
at launch                  1.34x     1.34x     1.34x   1.33x to 1.35x
after 10 years             1.33x     1.33x     1.33x   1.33x to 1.34x
after 25 years             1.31x     1.31x     1.31x   1.30x to 1.32x
after 50 years             1.25x     1.25x     1.25x   1.24x to 1.25x
after 100 years            1.11x     1.11x     1.11x   1.10x to 1.11x
after 200 years            1.01x     1.01x     1.01x   1.01x to 1.01x
never                      1.00x     1.00x     1.00x   1.00x to 1.00x
```

With support that never ends, the gain is 1.00×: the ground does by hand what the shrinking quorum does alone. With 49 years of support, Voyager's so far, the charts program gives 1.25×. Answer time barely matters. What matters is whether anyone is still there.

## Checked against the bench

`--bench FILE` replays the schedules of the [Layer 1 bench](https://docs.mru.space/core/bench/) through the model and compares the means. On the published results, 17 of 18 rows agree within 3 standard errors. Details are on the [bench page](https://docs.mru.space/core/bench/#model). This checks the policy model against the real code. It does not calibrate the environment.

## What this does not claim

Note: The parameters are illustrative, not calibrated. The claim is the shape of the trade, and the sweep shows where it holds.

Updated 11 Oct 2026 · [Edit on GitHub](https://github.com/mruspace/docs/edit/main/src/pages/simulation/dusk.astro) · [Questions? Get in touch](https://mru.space/contact/)

---

# Mru 2049 browser flight simulator

URL: https://docs.mru.space/lab/2049/

[Docs](https://docs.mru.space/) / [Lab](https://docs.mru.space/lab/2049/) / Mru 2049

# Mru 2049

A browser flight simulator on real astronomical data. Fly anywhere in the solar system and out to the nearby stars. Its purpose is to show scale. There is no combat, economy or progression.

TypeScript three.js · WebGPU 109,389 stars no server

## Run it

```
npm install
npm run dev
npm run check   # types, tests and lint
```

The data files in `public/` are committed, so a fresh clone flies without building any assets.

## Controls

| Input | Effect |
| --- | --- |
| Mouse | Pitch and yaw, rate based |
| Space | Full throttle. The ship handles the arrival |
| W / S | Throttle, logarithmic, 1 m/s to 1000 light years per second |
| Shift | Hold for ten times the throttle rate |
| A / D | Roll |
| X | Full stop |
| O | Match orbit with the nearest body |
| F | Find an object by name |

## URL switches

- **?webgl**: Force the WebGL2 backend
- **?debug=sky**: The star pass alone, amplified 400×
- **?debug=scene**: The scene pass alone, with no sky
- **?debug=depth**: Linear depth
- **?debug=alpha**: The scene pass's alpha channel

## How it is put together

```
sim     Ship state, date, flight. All Float64. Never imports three.js
ephem   Body positions and orientations from astronomy-engine
scene   Meshes, materials, and the per-frame rebase
render  Renderer, post chain, auto-exposure, textures
stars   Star catalog, point-source flux, the instanced star field
input   Keyboard, pointer and touch, into one control struct
ui      HUD and panels. Never renders inside the frame loop
tools   Build-time scripts. Their output is committed
```

## The coordinate system

-   **Float64 on the CPU.** All state is meters in the heliocentric J2000 mean equatorial frame. It never enters a shader.
-   **Floating origin.** The camera sits at exactly (0,0,0) and never moves.
-   **Reverse-Z depth**, behind a runtime toggle.
-   **Distant-body rescale.** Anything past 1e8 m is drawn at 1e8 m and scaled to keep its angular size.

Updated Sep 2026 · [Edit on GitHub](https://github.com/mruspace/docs/edit/main/src/pages/lab/2049.astro) · [Questions? Get in touch](https://mru.space/contact/)