How Do You Prove an AI-Assisted Filesystem Is Reliable?---Writing a COW Filesystem from Scratch，Part 6

"Trust, but verify." —— Reagan, to Gorbachev.

From the first day of writing singlefs, a pile of problems sat in front of me. For example:

So how do you prove the system isn't wrong?

Worse, in a filesystem it is easy to verify that something "was written", and hard to verify that something "was written wrong". The bytes you wrote read back just fine. Much later you may suddenly discover that the data was never actually stored — so what was it that got stored back then? Or every write goes through normally, the tests are all green, and one day after a power loss the disk never mounts again.

Luckily, singlefs has self-describing headers and a reverse index. Any block on disk can raise both hands and answer "who I am, whom I belong to, which generation I'm from". The data can account for where it went.

Data can state its own identity, but checking block by block is far too slow, and it can only check the result, not the process. So we need a rig that records the stream of data a transaction writes, has two unrelated parties each record the same process, and compares the two item by item. If they match, then at least what the program believes it wrote is what the disk actually received: nothing landed in the wrong place, and nobody quietly changed the order.

Concretely, we boot a QEMU VM with two virtual disks (virtio) and the write cache set to write back (like real hardware, writes go into the cache first). In front of each disk sits a layer of QEMU's built-in write-logging filter ( blklogwrites ). It stands outside the VM and logs every write (with its data) and every FLUSH.

The two recordings share not a single line of code:

The comparison rule lives in crates/singlefs-checker-tier/src/device_log.rs: the program's copy must be an item-by-item prefix of the disk's copy, and after the prefix only FLUSHes may follow (the system adds one on its own when the VM shuts down).

pub fn compare_allowing_trailing_flushes ( expected: & [ DeviceEvent ], // what the program thinks it sent observed: & [ DeviceEvent ], // what the disk actually received ) -> DeviceLogComparison { if observed.len () >= expected.len () && observed [.. expected.len ()] == * expected { let tail = & observed [ expected.len ().. ]; // once the prefix matches, any non-FLUSH event in the tail is a divergence if let Some ( position ) = tail.iter ().position (| event | * event!= DeviceEvent:: Flush ) { let index = expected.len () + position; return DeviceLogComparison { divergence: Some (( index, None, Some ( observed [ index ].clone ()))), trailing_flushes: position, }; } return DeviceLogComparison { divergence: None, trailing_flushes: tail.len () }; } // the prefix itself doesn't match: report the first divergence DeviceLogComparison { divergence: first_divergence ( expected, observed ), trailing_flushes: 0, } } Enter fullscreen mode Exit fullscreen mode Matching alone isn't enough, because a gate that is always green is no gate at all. So we run six scenarios in total, two of which are deliberately broken control groups:

There is also a third, independent path: the FLUSH count in the VM's /sys/block statistics must equal the number of barriers the program issued plus the number of FUA (forced-persistence) writes.

The point of the two control groups is to prove that when a barrier is dropped or writes are merged, this reconciliation can tell. If it said green even with a barrier missing, then "it matches" would prove nothing.

A QEMU bug, while we're here: when the number of data segments in a single write reaches 1023 or more, this write-logging filter exceeds the system's limit of 1024 segments per I/O. The host returns an invalid-argument error, the VM gets an I/O error, and formatting (mkfs) hits a wall. We patched QEMU: when over the limit, copy the data into one contiguous buffer first, then log it. The script that builds QEMU checks sha256 at every step.

This lets us prove: every write, barrier, forced persistence and discard the program issues reaches a real virtual block device intact and in the same order; merged writes and dropped barriers can both be told apart by the red/green controls.

What it can't prove: this gate does not simulate power loss. And a FLUSH on the virtual disk ultimately lands as a single sync call on the host; the cache of the host's own physical disk is out of reach. So what it verifies is the virtual block device layer, not the persistence semantics of a real disk.

Having shown the writes are fine, the next question is: is the order right?

An atomic commit in a COW filesystem ultimately rests on one ordering: write the content first, then write the pointer to it. If a reader sees the new pointer, it must be able to see the new content.

CPUs and compilers both reorder reads and writes for performance. Whether this ordering holds under the CPU memory model is left to herd7. herd7 is a memory-model checker, and we use the Linux kernel memory model (LKMM). Tests are written as small programs called litmus tests, kept under litmus/: 8 files in 4 pairs:

The simplest one ( litmus/commit-publish.litmus ):

P0 ( int * blk, int * gen ) // writer: commits a transaction { WRITE_ONCE ( * blk, 1 ); // write the block content first smp_wmb (); // write barrier WRITE_ONCE ( * gen, 1 ); // then write the version number pointing to it } P1 ( int * blk, int * gen ) // reader: mount or concurrent read { int r0; int r1; r0 = READ_ONCE ( * gen ); smp_rmb (); // read barrier r1 = READ_ONCE ( * blk ); } exists ( 1: r0 = 1 / \ 1: r1 = 0 ) // bad outcome: saw the new version number, read the old block Enter fullscreen mode Exit fullscreen mode It declares Never: herd7 must rule that this bad outcome cannot occur under any reordering.

This one file alone isn't enough. There are two more rules.

First, every "never occurs" gets a control group. commit-publish-nofence.litmus is the same code with both barriers removed, and it must be ruled "sometimes occurs". A script checks statement by statement that the control group is exactly the original minus its barriers. The reason is written in the control group's file header:

If this one is also ruled Never, the pattern can't happen in the first place, and commit-publish being ruled Never proves nothing.

This rule was learned the hard way: once, 10 unrelated "never occurs" tests all got through the gate on the strength of a single "sometimes occurs".

Second, bind them to the real code. Each litmus file header says which functions it models:

* singlefs-expect: Never * singlefs-models: crates/singlefs-core/src/transaction.rs:: publish_first_file writer (P0) * singlefs-models: crates/singlefs-core/src/recovery.rs:: choose_root reader (P1: pick the root first, then read units down the tree) Enter fullscreen mode Exit fullscreen mode The named function must be found exactly once in that file. Another test parses the writer's steps out of the litmus file and compares them item by item with the commit order the program actually recorded. Change the code, and this check has to be redone.

So we've proven that at the CPU memory-model layer, the COW commit order holds: a reader will not see the pointer and then fail to read the content.

What it can't prove: herd7 deals with reordering between the CPU and memory, not the order in which things are persisted to disk. "The pointer has been persisted but the data hasn't" is the business of FLUSH and forced persistence, which belongs to the real-device reconciliation before and the crash point replay next. Also, the binding to the code only compares the writer's steps; on the reader's side it only checks that the function exists.

The order is fine too. So can we recover correctly after a power loss?

The idea is simple: record every write request to the block device, cut it off at every moment the power could fail, then remount, recover, and check whether the recovered disk is valid and consistent with the history.

It sounds unremarkable, but it is the most terrifying part of the whole project.

Record: run the write path all the way through once, recording every write, barrier and forced persistence.

Cut: each barrier or forced persistence cuts the write stream into segments. The disk at the moment of power loss = all earlier segments fully persisted + each write in the current segment either "landed / didn't land", in any combination. A write is only "protected" by a later barrier on its own disk; as long as one disk hasn't let it through, the segment isn't closed. An in-place overwrite has one more outcome than an ordinary write — half-written, so neither old nor new can be read. That is tearing.

How do you count the combinations? The comment in the code says it bluntly ( crates/singlefs-checker-tier/src/crash.rs ):

/// Each write in the segment takes any of its states, in any combination, minus the one where the whole segment persisted: /// with m of the n writes being in-place overwrites, 3^m · 2^(n−m) − 1 states; when m = 0, any proper subset, 2^n − 1. EveryProperSubset, Enter fullscreen mode Exit fullscreen mode 3^m · 2^(n−m) − 1 Enter fullscreen mode Exit fullscreen mode Each in-place overwrite has three outcomes — "didn't land, landed, torn" — and an ordinary write has two. Multiply them, then subtract the one where "everything landed". Exponential explosion.

Judge: for every power-loss state, run four things in order:

The record checker deserves a word of its own. It does not go through the recovery code and does not parse the trees. It takes only four things — the disk before the power loss, the recorded write stream, the disk after the power loss, and which writes had persisted — and compares bytes. This path is a must: when we deliberately removed the barrier in front of the root pointer, the outcome check didn't flag a single state red; only the record checker went red, on exactly 1 state.

CRASH_AMPLIFICATION_TOTAL items=7 failed=0 states=2563727926 red=0 seconds=27288 Enter fullscreen mode Exit fullscreen mode 2.56 billion power-loss states, 0 red, 7 hours 35 minutes.

That is why milestone three nearly tore this part down and rewrote it around pruning and reuse: without that, no number of hosts would be enough. To put it fancily: heterogeneous GPU computing and a reusable verdict library.

Heterogeneous GPU computing: split the work between CPU and GPU. The CPU records efficiently; the GPU judges. Measured: fully judging one state on the CPU (writable mount + pool-level checker) takes about 19.5 ms; on the GPU, about 4 µs — a gap of nearly five thousand times. So recovery, the outcome check, the record checker and the pool-level checker's 109 rules were written all over again, in another language with other algorithms: six GPU shaders (WGSL), about 23,000 lines in total. The GPU version must agree with the CPU version state by state and bit by bit, with dedicated cross-check tests. If a table won't fit in VRAM, it reports "can't judge" and the whole run stops; it never quietly falls back to the CPU.

Reusable verdict library: each block's verdict is stored by key in a long-lived library. The key layout ( crates/singlefs-checker-tier/src/verdict_store.rs ):

block key (72 bytes) = digest of this segment's writes and the starting disk image (32) ‖ plan digest (32) ‖ block start (8) verdict key = block key ‖ judging-method fingerprint (32) Enter fullscreen mode Exit fullscreen mode The "judging-method fingerprint" is computed like this: take every function used to judge this block, strip comments, fingerprint each one, add the compile switches, the toolchain version and the versions of the dependencies used, and digest them together. File paths, function names, line numbers and commit hashes never enter the key. So when you change one function, only the verdicts that use it need to be rerun; everything else is reused as is.

We used to take the shortcut of using a digest of the whole library as the key; changing one character of the judging method invalidated everything, and we ended up re-judging an extra 3.9 billion states — function-level fingerprints were forced out of us that way.

On top of that, every run randomly draws a few already-judged entries from the library as sentinels, and forces one more to be re-judged. If a sentinel gets re-judged, or the forced re-judgement disagrees with the library entry, the reuse mechanism itself is broken, and this gate goes red immediately.

This lets us prove that for the write paths the tests cover, at the model level, a power loss at any moment can be recovered from correctly. But the volume is so large that full runs can only catch up in batches each milestone, or a little at a time when the machines are idle.

What it can't prove: it cuts the write stream the program recorded itself, assuming that recording is genuine — that part is backed by the first gate, the real-device reconciliation. Whether a real disk's FLUSH actually works is out of range. The fast tier we run day to day saves time by treating data blocks as either "landed whole" or "not landed at all", so it can't see the "data block only half landed" class; that's why commits still require the full run. And as of today, the full run hasn't been completed.

Everything above only proves that the program operates according to its own understanding. But is that understanding itself right?

We wrote an ideal filesystem in memory that cares only about semantics — not performance, and not crashes: crates/singlefs-harness/src/model.rs, 13,535 lines. It lives in memory, so it runs stably and its answers are unambiguous.

Then the same random sequence of operations drives both the ideal model and the real implementation at once (the implementation runs on an in-memory test disk). Before calling the implementation at each step, we ask the model: should this step "succeed", "be refused", or is "anything within some range" acceptable? The model's answer looks like this:

/// The model's answer for one step. pub struct ModelAnswer { pub operation: ModelOperationKind, /// Reasons it must be refused: if non-empty, it must be refused pub required_refusals: BTreeSet < ModelRefusalReason >, /// Roots that should be written on success, in order pub expected_roots: Vec < ModelRoot >, /// What should be read back after a cold start pub expected_read_back: Option < ModelReadBack >, /// When raising the rollback floor, what the ceiling should be pub rollback_floor_ceiling: Option < ModelCheckpointTxg >, // …… } Enter fullscreen mode Exit fullscreen mode When the implementation finishes, its result is translated and compared item by item against the model's answer. Disagreements fall into 28 kinds: should have succeeded but refused, should have refused but succeeded, wrong refusal reason, secretly wrote to disk before refusing, wrong roots written, wrong file content, wrong read-back after a cold start…… Any error the model has never seen is recorded as "unexplained" and not let go.

There are currently 20 kinds of random operations, with 16 different mixes. The most commonly used mix, when "mounted, with files present", is: overwrite 52, raise the rollback floor 16, roll back 10, mount 6, delete a file 3, crash recovery that discards the newest version 3.

Only when the model and the implementation agree step by step can we say our semantics — that is, the intent of each operation — was faithfully carried out by the implementation.

There is also a smaller RefFS (reference filesystem, crates/singlefs-reference-filesystem ). It has no external dependencies at all, uses only the Rust standard library, and walks through POSIX operations in memory. It answers just one question: is the content read back after a power loss within the allowed range?

/// States recovery may read back after a crash: {S_j: j = lo, or j is exactly the end of some explicit publish or rollback, lo ≤ j ≤ hi}, in ascending index order. pub struct AllowedSet { pub lower_bound: StateIndex, pub upper_bound: StateIndex, pub allowed: Vec < AllowedState >, } Enter fullscreen mode Exit fullscreen mode In plain words: between "the last version known to be persisted" and "the moment of power loss", the version right after each explicit commit may be what recovery produces; nothing else may. The ideal model handles "what it should be without a power loss"; RefFS handles "what may be seen after a power loss". They split the work.

What it can't prove: we wrote the model, and we wrote the implementation, and both understand the semantics from the same design documents. If both misunderstand together, both go green together. Also, right now we only check that the differential testing "ran", not that every kind of operation was actually "reached" by it; a newly added write path may never have been differentially tested for a single step.

But what if one of the most critical judgements in the implementation is wrong precisely on inputs that random operations will never hit?

Tests can only try finitely many inputs. Formal verification is different: first write down, in mathematics, the properties this code must satisfy (the spec), then have a prover prove that the code satisfies them for every possible input. If it can't be proven, the code isn't accepted.

We prove Rust code with Verus. Take replay_core ( crates/singlefs-replay-prefix/src/lib.rs ), the core function that, during recovery from a power loss, "takes the replayable stretch out of the journal". Its signature carries preconditions (requires) and conclusions (ensures):

pub fn replay_core <...> ( root_instance: PrefixKernelInstanceGeneration, root_checkpoint_txg: PrefixKernelCheckpointTxg, chosen_root_source: RootSource, records: & [ CoreRecord < RootSource > ], // …… ) -> ( replayed: Result < CoreOutcome < RootSource >, CoreFailure > ) requires records_ascend_by_instance_and_counter ( records @ ), // precondition: journal records are in order every_counter_has_a_successor ( records @ ), ensures replay_follows_the_prefix_rules (... ), // which stretch is taken follows the rules replaying_an_applied_record_twice_leaves_the_root_as_once (... ), // replaying the same record twice equals once replaying_from_the_landed_root_is_a_fixed_point (... ), // replaying again from the result changes nothing // and one more: the replay result is never older than the starting point Enter fullscreen mode Exit fullscreen mode Two shorter ones:

// Whether a record may be reclaimed is this one comparison; not one character more or less pub fn released_record_can_be_reclaimed ( released: bool, generation: u64, floor: u64 ) -> ( answer: bool ) ensures answer == ( released && generation <= floor ) Enter fullscreen mode Exit fullscreen mode // Losing power twice during garbage collection gives the same result as losing it once run_ring_next ( run_ring_next ( state, RunRingStep:: Crash ), RunRingStep:: Crash ) == run_ring_next ( state, RunRingStep:: Crash ) Enter fullscreen mode Exit fullscreen mode The key point: what is proven is exactly the code that runs, not a separately written model. The recovery path calls these functions directly; in a normal build, Verus's spec and proof parts are erased, and the remaining code is compiled into the product as usual. To keep "the version that was proven" and "the version that runs" from quietly drifting apart, the intermediate code produced by the two builds is also compared item by item and required to be identical.

All the proven code lives in one crate, crates/singlefs-replay-prefix, which depends only on Verus's standard library and has four files:

113 proof obligations in total, and zero occurrences across the four files of back-door constructs like "assume it holds" or "skip the proof".

But formal verification isn't almighty. Its most insidious failure isn't "can't prove it" — it's proving it while proving nothing. So four more things are guarded:

One, the vacuity check. If a precondition can never hold, anything can be "proven" from it. So for each precondition, an assert(false) is inserted at the top of the function, one separate copy per location, and the proof must fail. If it passes, the precondition contradicts itself, and that proof goes red.

Two, must-red worlds. 231 deliberately broken locations are registered. After breaking each one, Verus must report an error, and the error must land on the designated function. For example:

break: negate the conclusion original: is_last_record == is_last_record_of_its_publish(*record), mutated: is_last_record ==!is_last_record_of_its_publish(*record), expect: 7 proof errors Enter fullscreen mode Exit fullscreen mode Only a proof that can show it goes red counts as a proof.

Three, a pinned toolchain. The Verus version, the versions and content fingerprints of the six packages it depends on, and the Rust compiler version — if any one doesn't match, it turns red immediately.

Four, a pinned table of exhaustive counterexamples. We ran a separate experiment that exhaustively enumerates the real journal-replay function within a bounded size: about 49.75 million valid inputs and about 64.51 million adversarial inputs. Every counterexample found is pinned into a table exactly as is; it has 360 rows now. On every commit, the current code replays it row by row.

I have to admit formal verification is expensive, and to this day it covers only a few of the most central judgements: which stretch to take from the journal, which root to choose, scanning the journal ring, the compaction plan, the reclamation threshold. How on-disk bytes get parsed into these functions' inputs, disk barriers, encoding and decoding, checksums, multiple disks, integer overflow — none of that is in the proof. The README in that code directory says so itself: "this cannot be called a complete crash-recovery proof of the whole filesystem".

One more thing must be made clear: Verus proves "the code conforms to the spec"; it cannot prove "the spec itself is right". If the spec is wrong, the proof still goes through. Whether the spec is right depends on the reasoning in the design documents, and on the earlier gates corroborating one another.

So, could the verification itself be fake? Tests that don't reach the code, assertions written backwards, sample points that happen to fall where two variants give the same result — in all these cases the tests are still all green, but they judge nothing.

The idea is simple: deliberately break the code and see whether verification turns red. If it turns red, that check can tell this kind of error apart. If it stays green after you break things, that check is decoration.

One, every bug fixed leaves a landmine behind. crates/mutations.tsv has 5,981 rows in total. Each row says which file to change, which original text to replace with what, which tests to run, and which test must go red. For example:

name: free count not decremented after allocation ( the space - accounting check must go red ) file: crates / singlefs - core / src / allocator.rs original: self.free_slots -= span; mutated: // mutation: free count not decremented must fail: cold_start_reads_the_second_content_and_the_pool_checker_stays_green Enter fullscreen mode Exit fullscreen mode The table header records where it came from: every time a round of adversarial review finds a problem and it gets fixed, a mutation is left behind that "goes red if you revert it"; if the fix is quietly undone, this goes off first. Some day someone (most likely some agent) quietly reverts a fix, and the landmine goes off first. The original text must be found exactly once in the file; if the code changes and the original text can no longer be found, that row is recorded as "anchor lost", which is also red.

Two, broad mutation. Landmines are planted by people, so there are always places nobody thought of. There's therefore also a tool that generates mutations automatically ( scripts/mutation/broad-mutation.py, using cargo-mutants under the hood): flip a comparison operator, add or subtract one from a constant, delete a statement…… Counted once on 2026-09-30, it could generate 1,765 mutations from the checker and 3,326 from the core code. Every one must reach a verdict, and a single survivor blocks the commit. A few details:

The "must-red worlds" from the previous gate follow the same idea: break the proof, and the prover must report an error.

When a mutation survives, the laziest move is to write "these two variants are equivalent anyway" and walk away. The project's rules forbid that and split "survived" into eight categories. The most commonly abused one is this: it only happens to give the same result on the few test inputs I picked; change the input and it differs. In that case you must add an input; you may not fudge it as equivalent. The criterion is one sentence:

When a mutation isn't caught, ask once: with a different sample point, is it still the same value?

What it can't prove: mutation proves that "assertions can go red", not that "coverage is complete". Breakages not written in the table will never be tried, and the kinds of mutations that can be generated automatically are limited too.

Finally: pick up any disk — how do you decide whether it's a valid singlefs disk?

That's the pool-level checker. One thing first: it is not something that runs at mount time. Mounting goes through the core's own recovery and validation code; the checker is an independent auditor, called from tests, crash point replay and the GPU cross-checks. Mounting and auditing each judge the same thing once, with two separate bodies of code.

There is only one entry point ( crates/singlefs-checker/src/walk.rs ):

pub fn check_pool_image ( reader: & dyn ImageReader ) -> Vec < ( & 'static str, InvariantVerdict ) > Enter fullscreen mode Exit fullscreen mode The input is bytes only: ImageReader gives just "how many disks, how big each is, and read some bytes at some position on some disk". It touches no runtime memory state at all. The output is one verdict per rule:

/// The verdict of one invariant on one image. "Not applicable" must carry a reason; it may never silently count as holding. pub enum InvariantVerdict { Holds, // holds Violated ( String ), // violated, saying where NotApplicable ( & 'static str ), // not applicable, reason required PartiallyJudged ( String ), // everything judged is right, but part couldn't be judged: not red, not holding either } Enter fullscreen mode Exit fullscreen mode It first reads the system configuration disk by disk, then picks the newest valid root, scans the journal and replays that version, and then walks the disk once in each of two directions:

The indexes built from the two directions must be exactly identical. Finally, the space usage found by the scan is reconciled, disk by disk, against the accounts recorded on disk.

The list of rules the checker judges lives in crates/singlefs-checker/invariants/: 109 implemented, matching IMPLEMENTED_INVARIANTS: [&str; 109] in the code one to one. A few of them:

Every implemented rule comes with a broken disk that was "deliberately damaged to trigger exactly that rule".

The pool-level checker may not share a single line of logic with the core code; it shares only one module of format constants. Its Cargo.toml has exactly one dependency:

[ dependencies ] singlefs-format = { path = "../singlefs-format" } Enter fullscreen mode Exit fullscreen mode That format module isn't even allowed to contain if, match or for; it holds only constants. The design discipline has this line:

What is forbidden is not "traversal". It is two things: "not yet having the answer at the moment you need it", and "the auditor and the audited using the same code". The runtime and the checker must use different algorithms.

If the two shared a piece of parsing code and that code was wrong, both would be wrong the same way, and the reconciliation would still be all green. So the gate holds the line strictly: apart from the format constants, the two modules' dependencies may not overlap at all; and the functions called by the "follow the references" direction and the "scan block by block" direction may overlap only in format parsing and constants.

The checker is also a specification: it defines "what this format actually is". The format of all of singlefs is defined by the checker's source code; the documentation and everything else take it as the reference.

What it can't prove: it only looks at one static disk. Not a single encryption-related rule is implemented yet, and the rule that "forward references and the reverse index agree with each other" is still on the to-do list. The rules say it outright: "the checker reported nothing" does not mean "the disk is healthy". Errors not written into the list are invisible to it.

Every gate has its own shortcomings, and none of them can guarantee the code is correct on its own. But they back each other up:

The system these gates form is like the Berlin Wall: it's not tall. Want to get over it? Big Brother is watching you.

How would you prove this wall is solid, Comrade Gorbachev?