refly

A deterministic robot-control runtime with counterfactual replay — re-fly the incident, then re-fly it with the fix.

The problem

You can't fix a bug you can't replay. Robot incidents happen in wall-clock time, against lossy logs and nondeterministic schedulers; the fix gets validated on a fresh run and everyone hopes it would have handled the original. The missing discipline is the flight recorder that can re-fly: bit-exact replay of the incident, and the same tape re-run against the modified controller.

refly is a small, verified, public miniature of that discipline.

How it works

• No wall clock. The runtime advances in fixed sim-time ticks (1 kHz).
• Everything external is on the tape. Operator targets, fault windows, and noise values (never seeds) are recorded as (tick, event) JSON-lines.
• The state is hashed as it records. Digests (FNV-1a over f64::to_bits) land on the tape every 250 ticks. Replay recomputes and compares: a replay either reproduces the run bit-exactly or refuses with the first mismatching tick.
• Counterfactual = same tape, different controller. The world's inputs are replayed verbatim; only the controller config changes. The report diffs the two runs' tool-centre paths and tracking errors.

The plant is the public GLUON 6-DOF arm under first-order velocity tracking with URDF limits; the controller is a resolved-rate TCP tracker on the verified gluon-kinematics FK/IK. Faults are the classics: sensor glitch (bias), command drop windows, command latency.

The demo

$ cargo run --example incident

recorded  2084 events -> …/refly-incident.tape.jsonl
incident  max tcp err    196.9 mm   rms   89.2 mm   final digest ecf9761fed840cd1
replay    max tcp err    196.9 mm   rms   89.2 mm   final digest ecf9761fed840cd1   == BIT-EXACT
fix       max tcp err     60.1 mm   rms   27.0 mm   (same tape, gains kp 6 -> 2.5, damping 0.00001 -> 0.05)

paths diverge by up to 193.1 mm under identical inputs and faults
verdict: the fix bounds the incident's worst error 3.3x tighter —
         demonstrated on the incident, not on a fresh run

Verification

cargo test — the claims are tested, not asserted:

1. Determinism as a property. proptest drives arbitrary gains, scenarios, and fault plans: record then replay must agree on the final digest and the full evidence trace (48 randomized cases).
2. Tampering is detected. Perturb one recorded target by 1e-9 and replay refuses at the first divergent digest.
3. Independent oracle. The plant integrator is mirrored by a dependency-free Python implementation (tools/plant_reference.py); goldens must agree to < 1e-9 after 4000 steps.
4. Physics invariants. Under arbitrary faults, joints never leave the URDF position limits and commands respect the velocity bound.
5. Counterfactual identity. Same config in, zero divergence out.

Honest scope

• The determinism guarantee is same binary, same target: IEEE-754 doubles replayed through identical operations. Cross-platform bit-equality is not claimed.
• The plant is kinematic-level (velocity-tracking lag + limits), one process, sim only. This demonstrates the runtime discipline, not contact dynamics.
• Prior art exists and is good: Copper (deterministic Rust robotics runtime), Drake (reproducible simulation), Rerun (logging/viz). The angle here is the counterfactual-replay-as-evidence workflow, small enough to read in an afternoon and verified against independent oracles.

Layout

src/tick.rs        fixed-step time base (no wall clock)
src/tape.rs        the event tape: inputs + digests, JSON-lines
src/hash.rs        FNV-1a over f64 bits — bit-exact means bit-exact
src/plant.rs       GLUON joints, velocity-tracking lag, URDF limits
src/controller.rs  resolved-rate TCP tracker (gluon-kinematics DLS IK)
src/faults.rs      glitch / drop / latency, applied from tape events
src/runtime.rs     record / replay / counterfactual
tools/plant_reference.py   independent plant oracle

MIT © 2026 William (Viet) Nguyen. Clean-room; the arm model is the public BSD Mintasca GLUON description.