№ 005 · Release
Mru Flight 0.2.0: measured, and in F´
Layer 1 measured on real processors with injected faults, against fixed TMR on the same faults. And the same core, inside NASA JPL's F´ framework, giving the same counts.
What is new
№ 004 showed the decision core and a demo. Version 0.2.0 adds three things:
- A bench. 300 runs per host on three processors, the shrinking quorum against fixed TMR on the same faults.
- F´ components. The core inside NASA JPL's F´, through a C interface that Kani proves equal to it.
- Resets. The demo saves its state and resumes after a crash or power cut, with the same counts.
Measured
| Faults | Fixed TMR | Shrinking quorum | Ratio |
|---|---|---|---|
| Upsets only | 19,999.9 | 19,999.9 | 1.00 (1.00) |
| Two replicas lost, one at a time | 9,988.5 | 14,985.0 | 1.50 (1.50) |
| Two lost early | 3,994.7 | 11,987.3 | 3.00 (3.00) |
| One stuck, one lost | 8,989.5 | 14,483.8 | 1.61 (1.61) |
| Two lost, the last one stuck | 9,988.5 | 12,486.2 | 1.25 (1.25) |
In all 150 pairs of runs, the shrinking quorum delivered at least as many correct results as fixed TMR. The counts are the same, run for run, on an Apple M4, an Arm Neoverse-N2 and an AMD EPYC 7763.
The cost, measured
The extra work has a price on the last replica. Upsets that hit both of its runs alike gave up to 3.6 wrong results per run. A replica that got stuck gave 20, before the periodic known-answer test caught it 40 ticks later.
Dusk, the simulator, predicts these counts. Run on the same schedules, its policy model agrees with the bench within 3 standard errors in 17 of 18 comparisons. That checks the model against the code. It does not calibrate the environment: that needs radiation or flight data.
Inside F´
Four components for F´ v4.4.1: RedundancyManager, HealthRegistry, ReplicaHost, and FaultInjector for tests. Every decision still comes from the Rust core. A C interface carries it, and Kani proves that each of its functions gives the core's answer.
- The same counts. On the bench schedules, 36 of 60 runs match the demo exactly. In the rest, a replica that dies is found by silence, which costs 2 correct results. Wrong results match in all 60.
- Spares and standby. A slot can take a spare after a known-answer test, or be set aside to save power.
- Resets. Policy, slots and cycle survive a reset.
37 unit tests and 9 Kani proofs run on every change.
What comes next
The same bench on a target-class board, with reboots and power cuts. The scripts are ready.
A full F´ deployment on that board, with commands and telemetry from the ground.
Real upsets: a radiation beam test, then flight.
On Earth: the same software on an unattended ocean node. Mru Field
Cite this
W. Binns, Mru Flight, version 0.2.0, 2026. github.com/mruspace/flight. See CITATION.cff.