Keep a spacecraft working as its computers fail.
Onboard software for the processors you already fly. A small Rust decision core, checked with the Kani model checker, to be wrapped as components for NASA JPL's F´ framework.
01 · The problem
Triple redundancy stops at the second failure.
Classic TMR votes on three computers and stops when it can no longer form a majority. On a mission no one can service, that throws away the last computer's whole remaining life.
Mru Flight keeps going: vote on three, compare on two, self-check on one. Until TMR stops, it decides exactly as TMR would. After that, it keeps working.
Proved
Never less than TMR
While TMR can run, both decide the same. A Kani proof covers every possible input.
Proved
Only agreed results
Two votes, or a clean self-check on the last computer. Nothing else is delivered.
Measured
Small enough to fly
About 1.5 MB per process on ARM64. The core is no_std, allocates nothing and has no dependencies.
Requirements and limits
What it needs, and what it does not do.
| Processors | Three replicas of the same task. Continues on two, then one. |
| Targets today | Decision core: bare-metal ARM Cortex-M, no_std. Demo: static Linux binaries for 64-bit and 32-bit ARM, tested under emulation. |
| Framework | F´ components designed, not yet built: RedundancyManager, HealthRegistry, ReplicaHost. |
| Throughput cost | None with two or three replicas alive. Half rate on the last one. |
| Known limit | On the last replica, a stuck fault is caught only by the periodic known-answer test, every 64 ticks by default. In one test run, 24 wrong results got out first. |
| Flight heritage | None yet. |
02 · The road to orbit
What exists, and what comes next.
Mru Flight follows Mru Field. Field data on Earth comes first, then orbit.
Decision core and demo
Rust core with Kani proofs, a demo on real processes with injected faults, static ARM builds. v0.1.1.
F´ components
RedundancyManager, HealthRegistry and ReplicaHost as thin C++ shells around the Rust core.
Hardware in the loop
Real boards with injected faults: bit flips, resets, power cuts.
In orbit
A flight experiment, logging real radiation upsets next to the satellite's own dosimetry.
For
Mission teams who can't send a technician.
- Smallsat and constellation operators
- Lunar and deep-space mission teams
- Agencies, primes, and rad-hard and FPGA vendors
Questions
Do we need new flight hardware?
No. Mru Flight is software for the processors you already fly, starting with F´.
What does it cost us in throughput?
Nothing while three or two computers are alive. On the last one, self-check runs at half speed, because it does every computation twice.
What is the risk?
On one computer, a stuck fault is caught by a periodic known-answer test. Until then, a few wrong results can get out. We measure and publish that trade.
How is it priced?
Per mission, with support and qualification evidence. We discuss terms once we know the mission and its hardware.