---
title: "Mru Flight: fault tolerance for spacecraft out of reach"
url: https://mru.space/flight/
description: "A no_std Rust decision core with Kani proofs, to run as F´ components. Continues on two, then one processor after fixed TMR stops. Prototype, TRL 3."
---

[Mru](https://mru.space/) / Mru Flight

Mru Flight · Space Prototype · TRL 3

# Mru Flight: fault tolerance for spacecraft out of reach.

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.

[Get in touch](https://mru.space/flight/#request) [Read the release](https://mru.space/research/flight-prototype/)

![Two CubeSats released from the International Space Station above Earth](https://mru.space/_astro/pl16-iss-cubesats.DoZXtQTe_Z1r5SXv.jpg)

Two CubeSats released from the ISS above Earth's limb NASA · Public domain

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.

![Correct results over 20,000 ticks. Fixed TMR stops at 8,993. The shrinking quorum reaches 14,490.](https://mru.space/charts/flight-correct-light.svg)

One run, same seed and faults: one replica stuck at tick 4,000, another dead at 9,000. Fixed TMR: 8,993 correct results. Mru Flight: 14,490.

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.

The road to orbit

## What exists, and what comes next.

Mru Flight follows Mru Field. Field data on Earth comes first, then orbit.

Now

### Decision core and demo

Rust core with Kani proofs, a demo on real processes with injected faults, static ARM builds. v0.1.1.

Next

### F´ components

RedundancyManager, HealthRegistry and ReplicaHost as thin C++ shells around the Rust core.

Bench

### Hardware in the loop

Real boards with injected faults: bit flips, resets, power cuts.

Orbit

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