Technical Report — Version 1 RadFI is an algebraic fault injection operator for the empirical validation of Linux filesystem resilience theorems. Where the BEAMFS recovery calculus defines a recovery operator G that drives a corrupted filesystem state back to consistency or to fail-closed, RadFI defines a perturbation operator ε that injects controlled bit-flips into the bio-layer payload of an instrumented filesystem, modelling the action of a Single-Event Upset on volatile memory transit between user space and storage. This methodology paper formalises ε as a partial function over the BEAMFS-compatible state space, states a faithfulness theorem (Theorem IV. 1) bounding the total variation distance between RadFI's perturbation distribution and the canonical SEU distribution via Le Cam's binomial-to-Poisson approximation, and derives a Linux kernel implementation path through kprobe-based runtime instrumentation. Three perturbation families are treated: write-side bit-flips on bio payloads bound for storage, read-side bit-flips on bio payloads returning from storage (DRAM-bidirectional model), and targeted block-level injection through a sector-granularity filter. Empirical contributions: - Falsification of BEAMFS v1 Theorem IV. 1 (2026-04-28). RadFI v0. 1. 0 produced a controlled bit-flip pattern that the BEAMFS v1 recovery operator failed to correct, exhibiting a state s such that G (ε (s) ) ⊭ and G (ε (s) ) ≠ ⊥. This counter-example led the BEAMFS author to retract v1 Theorem IV. 1 and revise the threat model from radiation-only (v1) to full electromagnetic resilience (v2 EMR). - Confirmation of BEAMFS v2 INLINE recovery (2026-04-29). Byte-level disk corruption of a BEAMFS v2 INLINE-formatted filesystem (RS (255, 239) ×16 per-block protection scheme) was successfully recovered by the kernel module's readfolio path, with autonomic in-place repair persisting the correction byte-perfect to disk. Methodological position. A filesystem resilience theorem must be subject to empirical falsification, and the falsification instrument must itself be a formally specified algebraic operator whose own faithfulness is theorem-bound. RadFI is the first such instrument we are aware of in the Linux filesystem ecosystem. Companion paper: BEAMFS v2 Technical Report (uploaded as a separate Zenodo record on the same date). Cross-references between the two papers are established by GitHub tag and commit hash; Zenodo DOIs are added in subsequent revisions. Implementation: The RadFI reference implementation source is held in the private repository roastercode/radfi pending coordinated public release with this methodology paper. The present paper is published in the public BEAMFS repository at github. com/roastercode/beamfs, sub-directory papers/2026-04-radfi-v1/, GPG-signed under tag v1. 1. 0-radfi-paper-latex (commit 00afee5). License: CC-BY-4. 0 (paper text). GPL-2. 0 for referenced source code.
Aurelien Desbrieres (Wed,) studied this question.