---
title: "Mru Flight: a first prototype"
url: https://mru.space/research/flight-prototype/
description: "A no_std Rust core with four Kani proofs and a fault-injection demo. With one replica stuck and one dead: 14,490 correct results vs 8,993 for fixed TMR."
---

[Research](https://mru.space/research/) / [Releases](https://mru.space/research/?kind=releases) / № 004

№ 004 · Release

# Mru Flight: a first prototype

Onboard software that keeps a spacecraft doing useful work as its computers fail. A small, verified Rust core, and a demo on real processes with faults injected.

By **Will Binns** Published **7 Oct 2026** 9 min read Release **v0.1.1** Code [**mruspace/flight**](https://github.com/mruspace/flight)

## What it is

Dusk showed what a shrinking quorum is worth in simulation. This is where the policy becomes flight software. It has two parts.

The **decision core** is a Rust crate that decides, each tick, whether to vote, compare or self-check, and keeps the health record of each replica. It has no dependencies and allocates nothing, so the same code can run on flight hardware and be checked by a model checker.

The **demo** runs three real replica processes and a voter built on the core. It injects faults: kill, hang, stuck, and bit flips in working memory, the way radiation would.

Status:Early prototype, TRL 3. The F´ components come next.

## What the core guarantees

-   **Never less than fixed TMR.** While TMR can still run, both policies decide the same.
-   **It stops only with nothing left.** Fixed TMR stops below two replicas.
-   **Only agreed results go out.** Two votes, or a clean self-check on the last replica.

Unit tests check every combination of a small value domain. Kani checks every possible input, in CI, on every change.

Note 1:Kani is a model checker for Rust from AWS. Four proofs, listed in the [docs](https://docs.mru.space/core/quorum-crate/#proofs).

![Correct results over 20,000 ticks. Both lines match until tick 9,000. Then fixed TMR stops at 8,993 correct results. The shrinking quorum reaches 14,490.](https://mru.space/charts/flight-correct-light.svg)

Fig. 1 · Same seed, same faults: random upsets, replica 1 stuck from tick 4,000, replica 0 dead at tick 9,000.

## One run, two designs

Fixed TMR masks the stuck replica while it has three. Once another replica dies, it is left comparing a good replica with a stuck one, and every result is rejected. The shrinking quorum retired the stuck replica two ticks after it failed, then carried on with self-check on the last good one.

| Scenario, 20,000 ticks | Fixed TMR | Shrinking quorum |
| --- | --- | --- |
| Random upsets only | 20,000 | 20,000 |
| Replicas die at 5,000 and 10,000 | 9,990, halts | 14,989 |
| One dies, one stuck | 9,990, stuck | 14,988 |

Note 2:Illustrative scenarios, not a reliability estimate. For statistics over thousands of missions, see [№ 002](https://mru.space/research/dusk-results/).

## The honest cost

On one replica, a stuck fault is caught only by the periodic known-answer test, every 64 ticks. In one run, the demo delivered 24 wrong results before the test caught the fault and the system stopped. Fixed TMR would have stopped long before and delivered none.

A shorter test period trades throughput for a smaller window. That is the trade the whitepaper and Dusk put numbers on.

Note 3:The tests also caught a real flaw: health scoring once retired healthy replicas after random upsets. Diagnosing before retiring fixed it.

## Small enough to fly

| Platform | Voter | Each replica | Binary |
| --- | --- | --- | --- |
| Linux ARM64 | ~1.5 MB | ~1.5 MB | ~0.5 MB |
| Linux x86\_64 | ~2.0 MB | ~2.0 MB | ~0.5 MB |
| macOS, Apple silicon | ~1.5 MB | ~1.4 MB | ~0.5 MB |

Note 4:Measured in CI on every change, over 20,000 results.

## What comes next

1

F´ components around the Rust core: RedundancyManager, HealthRegistry, ReplicaHost.

2

Measurements on representative processors.

3

A hardware-in-the-loop bench with real boards and injected faults.

4

In orbit: a flight experiment on a real satellite.

5

On Earth: the same software on an unattended ocean node. [Mru Field](https://mru.space/field/)

Cite this

W. Binns, *Mru Flight*, version 0.1.0, 2026. github.com/mruspace/flight. See CITATION.cff.

[Previous · № 003 Mru 2049: the sense of scale](https://docs.mru.space/lab/2049/) [Back to The log](https://mru.space/research/)