「信頼せよ、されど検証せよ。」—— レーガンがゴルバチョフに言った。
singlefs を書き始めた初日から、いくつもの問題が目の前に並んでいた。たとえば：
- singlefs のデータフォーマットは他のファイルシステムとまったく違う。既存の検証基準をそのまま持ってくることはできない。
- singlefs のコードは AI の轟音の中で噴き出してくる。人間の目によるレビューはコードの速度に追いつけない。
- singlefs はいちばん下のトランザクションから書いている。メモリ上のデータが正しいかどうかを、テレパシーで判断することはできない。
- ……
では、システムが間違っていないことをどう証明するのか。
しかも、ファイルシステムでは「書き込めた」ことの検証は簡単だが、「書き間違えた」ことの検証は難しい。書いたバイトは普通に読み出せる。ずっと後になって、そのデータが実は一度も保存されていなかったと突然気づくかもしれない——では、あのとき保存したのは一体何だったのか。あるいは書き込みはすべて正常で、テストもオールグリーンなのに、ある日電源が落ちたあと、ディスクが二度とマウントできなくなるかもしれない。
自分たちが正しいことを、どう証明するのか。
幸いなことに、singlefs には自己記述ヘッダと逆引きインデックスがある。ディスク上のどのブロックも、両手を高く挙げて「私は誰か、誰に属しているか、何世代目か」に答えられる。データは自分の行き先を自分で説明できるのだ。
では、自分を証明していこう。
一、実デバイスでの突き合わせ：ディスクが受け取ったものは、プログラムが書いたものか
データは自分の身元を説明できる。だが一ブロックずつ調べるのは遅すぎるし、調べられるのは「結果」だけで「過程」は調べられない。そこで、一回のトランザクションが書き込むデータの流れを記録する装置が要る。同じ過程を、互いに無関係な二人がそれぞれ記録し、一項目ずつ突き合わせる。二つが一致すれば、少なくとも、プログラムが書いたつもりのものを、ディスクは本当に受け取ったことになる。書く場所を間違えてもいないし、順序を誰かにこっそり入れ替えられてもいない。
具体的には、QEMU の仮想マシンを一台立ち上げ、仮想ディスク（virtio）を二枚つなぎ、書き込みキャッシュを write back にする（実機と同じく、書き込みはまずキャッシュに入る）。各ディスクの手前に QEMU 組み込みの書き込みログフィルタ（blklogwrites）を一枚かぶせる。これは仮想マシンの外側に立ち、すべての書き込み（データごと）とすべての FLUSH を記録する。
二つの記録はコードを一行も共有しない：
- プログラム側：被テストプログラム自身のレコーダー。ホスト上で同じ引数でもう一度走らせ、同じバイト列を得る。
- ディスク側：QEMU が仮想マシンの外で記録したデバイスログ。
突き合わせのルールは crates/singlefs-checker-tier/src/device_log.rs に書いてある。プログラム側の記録は、ディスク側の記録の項目単位のプレフィックスでなければならない。プレフィックスの後ろに続いてよいのは FLUSH だけだ（仮想マシンのシャットダウン時にシステムが自分で一つ足す）。
pub fn compare_allowing_trailing_flushes(
expected: &[DeviceEvent], // プログラムが送ったつもりのもの
observed: &[DeviceEvent], // ディスクが実際に受け取ったもの
) -> DeviceLogComparison {
if observed.len() >= expected.len() && observed[..expected.len()] == *expected {
let tail = &observed[expected.len()..];
// プレフィックスが一致した後、末尾に FLUSH 以外のイベントが一つでもあれば不一致
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() };
}
// プレフィックスの時点で合わない：最初の不一致を報告する
DeviceLogComparison {
divergence: first_divergence(expected, observed),
trailing_flushes: 0,
}
}
一致するだけではまだ安心できない。永遠に緑のゲートは、ゲートがないのと同じだからだ。そこで全部で六つのシナリオを走らせる。そのうち二つは、わざと壊した対照群だ：
| シナリオ | やること | 期待 |
|---|---|---|
direct |
プールを新規作成し、最初のファイルを書く。ページキャッシュを通さず直接ディスクへ | 緑 |
file-overwrite |
上に加えて、もう一度上書きする | 緑 |
second-instance |
さらに、再起動、書き込み可能マウント、もう一度コミット | 緑 |
raise-rollback-floor |
さらにもう一度コミットし、「どこまで巻き戻せるか」の下限を引き上げる | 緑 |
skip-new-pool-file-creation-barrier |
書き込みバリアをわざと一つ抜く | 赤でなければならない。しかも一枚目のディスクだけが赤 |
page-cache |
わざとシステムのページキャッシュを通す | 赤でなければならない（32K と 16K の二つの書き込みが、48K の一つにまとめられる） |
さらに三つ目の独立した道もある。仮想マシン内の /sys/block の統計に出る FLUSH の回数は、プログラムが出したバリアの数と FUA（強制永続化）書き込みの数の和に等しくなければならない。
二つの対照群の意味は、バリアが抜けたり書き込みがまとめられたりしたら、この突き合わせがそれを見分けられると証明することにある。バリアが抜けても緑と判定するなら、「一致した」ことは何も証明していない。
ついでに QEMU のバグを一つ。この書き込みログフィルタは、一回の書き込みのデータセグメント数が 1023 以上になると、システムの一回の I/O あたり最大 1024 セグメントという上限を超えてしまう。ホスト側で引数エラーが返り、仮想マシン内には I/O エラーが届き、フォーマット（mkfs）がそこで壁にぶつかる。QEMU にパッチを当てた：上限を超えるときは、まずデータを連続したバッファにコピーしてから記録する。QEMU をビルドするスクリプトは、すべてのステップで sha256 を照合している。
これで証明できる：プログラムが出したすべての書き込み、バリア、強制永続化、discard は、本物の仮想ブロックデバイスにそのまま、同じ順序で届く。書き込みがまとめられたこともバリアが抜けたことも、赤と緑の対照で見分けられる。
証明できないこと：この関門には電源断のシミュレーションがない。さらに仮想ディスクの FLUSH は、最終的にホストでの一回の同期呼び出しに落ちるだけで、ホストの物理ディスク自身のキャッシュまでは届かない。だから検証しているのは仮想ブロックデバイスの層であって、本物のディスクの永続化セマンティクスではない。
二、メモリ順序：順序は成り立つか
書き込みに問題がないことは証明した。次の問いは、順序は正しいか、だ。
COW ファイルシステムのアトミックなコミットは、突き詰めれば一つの順序の上に建っている：先に内容を書き、それから内容を指すポインタを書く。読み手が新しいポインタを見たなら、新しい内容も見えていなければならない。
CPU もコンパイラも、性能のために読み書きを並べ替える。この順序が CPU のメモリモデルの下で成り立つかどうかは herd7 に判定させる。herd7 はメモリモデル検査器で、我々は Linux カーネルのメモリモデル（LKMM）を使う。テストは litmus と呼ばれる小さなプログラムとして書き、litmus/ に置く。全部で 8 本、4 組：
| テスト | 起きてはならない悪い結果 |
|---|---|
commit-publish |
読み手が新しいバージョン番号を見たのに、古いブロック内容を読む |
…-journal-implies-units |
読み手がジャーナルのレコードを見たのに、レコードが名指ししたデータブロックを読めない |
…-root-implies-units |
読み手が新しいルートポインタを見たのに、ルートの下のデータブロックを読めない |
publish-returns-after-the-rotation-barrier |
コミットはもう成功を返したのに、読み手にはまだそのコミットが見えない |
いちばん単純な一本（litmus/commit-publish.litmus）：
P0(int *blk, int *gen) // 書き手：トランザクションをコミット
{
WRITE_ONCE(*blk, 1); // 先にブロック内容を書く
smp_wmb(); // 書き込みバリア
WRITE_ONCE(*gen, 1); // それから内容を指すバージョン番号を書く
}
P1(int *blk, int *gen) // 読み手：マウントまたは並行読み出し
{
int r0;
int r1;
r0 = READ_ONCE(*gen);
smp_rmb(); // 読み込みバリア
r1 = READ_ONCE(*blk);
}
exists (1:r0=1 /\ 1:r1=0) // 悪い結果：新しいバージョン番号を見たのに、古いブロックを読む
これは Never を宣言している。herd7 は、この悪い結果がどんな並べ替えの下でも起きないと判定しなければならない。
これ一本では足りない。ルールがさらに二つある。
一つ目、すべての「起きない」に対照群を一つずつ付ける。 commit-publish-nofence.litmus は同じコードから二つのバリアを外したもので、「起きることがある」と判定されなければならない。スクリプトは一文ずつ照合し、対照群がちょうど元のものからバリアを外した形になっていることを確かめる。理由は対照群のファイルヘッダに書いてある：
もしこちらも Never と判定されたら、このパターンはそもそも起こり得ないということであり、commit-publish が Never と判定されても何も証明していない。
このルールは痛い目に遭って生まれた。以前、互いに無関係な 10 本の「起きない」が、たった 1 本の「起きることがある」だけで、まとめてゲートを通っていたのだ。
二つ目、本物のコードに結びつける。 各 litmus のファイルヘッダには、それがどの関数をモデル化しているかが書いてある：
* singlefs-expect: Never
* singlefs-models: crates/singlefs-core/src/transaction.rs :: publish_first_file 書き手（P0）
* singlefs-models: crates/singlefs-core/src/recovery.rs :: choose_root 読み手（P1：先にルートを選び、それからツリーをたどってユニットを読む）
書かれた関数名は、そのファイルの中でちょうど一つ見つからなければならない。さらに別のテストが litmus の書き手の手順を解析し、プログラムが実際に記録したコミットの順序と一項目ずつ突き合わせる。コードを変えれば、この判定はやり直しになる。
これで証明できた：CPU のメモリモデルの層では、COW のコミット順序は成り立つ。読み手がポインタを見たのに内容を読めない、ということは起きない。
証明できないこと：herd7 が扱うのは CPU とメモリの間の並べ替えであって、ディスクに永続化される順序ではない。「ポインタはもう永続化したが、データはまだ」という問題は FLUSH と強制永続化の担当で、それは前の実デバイス突き合わせと、次のクラッシュポイント再生の仕事だ。また、コードとの結びつけで比べているのは書き手側の手順だけで、読み手側は関数が存在するかどうかしか確かめていない。
三、クラッシュポイント再生：電源断のあらゆる瞬間で一太刀
順序も問題ない。では、電源断のあと正しく復旧できるか。
理屈は単純だ。ブロックデバイスへのすべての書き込み要求を記録し、電源が落ち得るあらゆる瞬間で打ち切る。それから再マウントして復旧し、復旧したディスクが正当か、履歴と辻褄が合うかを調べる。
地味に聞こえるが、ここがプロジェクト全体でいちばん恐ろしいところだ。
記録する：書き込みパスを最後まで一度走らせ、すべての書き込み、バリア、強制永続化を記録する。
切る：バリアや強制永続化が来るたびに、書き込みの流れを区間に切る。電源断の瞬間のディスクの状態 = それより前の区間はすべて永続化済み + 現在の区間の各書き込みがそれぞれ「落ちた / 落ちていない」の任意の組み合わせ。ある書き込みを「守る」のは、同じディスク上でそれより後ろにあるバリアだけだ。まだ通していないディスクが一枚でもあれば、その区間は閉じない。インプレース上書きには、通常の書き込みより一つ多い結果がある——書きかけで、新旧どちらも読めない。これがティアリングだ。
組み合わせの数はどう数えるか。コードのコメントにあけすけに書いてある（crates/singlefs-checker-tier/src/crash.rs）：
/// 区間内の各書き込みはそれぞれ取り得る状態を任意に組み合わせ、区間全体が永続化した一通りを除く：
/// n 個の書き込みのうち m 個がインプレース上書きのとき 3^m · 2^(n−m) − 1 通り。m = 0 なら任意の真部分集合で 2^n − 1 通り。
EveryProperSubset,
3^m · 2^(n−m) − 1
インプレース上書きは一つあたり「落ちていない・落ちた・ティアリング」の三通り、通常の書き込みは二通り。掛け合わせて「全部落ちた」一通りを引く。指数爆発だ。
判定する：電源断の各状態ごとに、四つを順に走らせる：
- 復旧を二回：一回はジャーナルを見て、一回は見ずに。
- 結果判定：復旧した内容が、この履歴で現れてよいどれかの版か。
- プールレベル checker：ディスク上の構造が正当か（七つ目で詳しく）。
- レコード照合器：ルートポインタとジャーナルレコードの書き込みが本当にディスク上にあるか、データブロックが欠けていないか。
レコード照合器は特筆に値する。復旧コードを通らず、ツリーも解析しない。「電源断前のディスク、記録した書き込みの流れ、電源断後のディスク、どの書き込みが永続化済みか」の四つだけを取ってバイトを比べる。この道は必須だ。実測で、ルートポインタの手前のバリアをわざと一つ外したところ、結果判定は一つの状態も赤にしなかった。赤を出したのはレコード照合器だけで、1 状態だった。
規模：
- 2026-09-30 のフルラン一回：7 項目、マシン 2 台、GPU 5 枚、全数探索：
CRASH_AMPLIFICATION_TOTAL items=7 failed=0 states=2563727926 red=0 seconds=27288
25.6 億の電源断状態、赤 0、所要 7 時間 35 分。
- 今日登録されているクラッシュケースは 47 本、さらに規模を増幅した項目が 25 ある。
- 2026-10-25 のコミット前フルラン：38 本のケースのうち先頭 6 本を走り切り、累計 45 億状態、違反 0。そのうち 30 億は過去の判定をそのまま再利用した。その後に止めたので、残り 31 本は走っていない。
これが、マイルストーン三でこの部分をほぼ全部壊して書き直し、枝刈りと再利用に切り替えた理由だ。そうしなければ、何台ホストがあっても足りない。かっこよく言えば、GPU ヘテロジニアスと判定ライブラリの再利用だ。
GPU ヘテロジニアス：CPU と GPU で分業する。CPU は効率よく記録し、GPU が判定する。実測で、CPU が一つの状態を完全に判定する（書き込み可能マウント + プールレベル checker）のに約 19.5 ミリ秒、GPU は約 4 マイクロ秒。五千倍近い差だ。そこで、復旧、結果判定、レコード照合器、そしてプールレベル checker の 109 のルールを、別の言語、別のアルゴリズムでもう一度書いた。六本の GPU シェーダ（WGSL）、合計約 2.3 万行。GPU 版は CPU 版と状態ごと・ビットごとに一致しなければならず、専用の突き合わせテストがある。VRAM のテーブルに収まらなければ「判定不能」を報告し、その回は丸ごと止まる。こっそり CPU に戻ることは絶対にしない。
判定ライブラリの再利用：ブロックごとの判定は、キーを付けて長期保存のライブラリに入れる。キーのレイアウト（crates/singlefs-checker-tier/src/verdict_store.rs）：
ブロックのキー（72 バイト）= この区間の書き込みと開始時ディスク状態のダイジェスト（32）‖ 計画のダイジェスト（32）‖ ブロックの始点（8）
判定のキー = ブロックのキー ‖ 判定法の指紋（32）
「判定法の指紋」はこう計算する。このブロックの判定に使う関数それぞれについて、コメントを取り除いてから指紋を取り、そこにコンパイルスイッチ、ツールチェーンのバージョン、使う依存のバージョンを加えてダイジェストをとる。ファイルパス、関数名、行番号、コミット番号は一切キーに入れない。だから関数を一つ変えれば、それを使う判定だけをやり直し、それ以外はそのまま再利用できる。以前は楽をして、ライブラリ全体のダイジェストをキーにしていた。判定法を一文字変えるとすべてが無効になり、合計で 39 億状態も余計に判定し直した——関数単位の指紋は、こうして追い込まれて生まれた。
さらに毎回、ライブラリから判定済みのものをいくつかランダムに抜いて番兵にし、もう一つを強制的に判定し直す。番兵が判定し直されたり、強制再判定の結果がライブラリの記録と食い違ったりしたら、再利用の仕組みそのものが壊れているということで、この関門は即座に赤になる。
これで証明できる：テストでカバーした書き込みパスは、モデルの層では、どの瞬間に電源が落ちても正しく復旧できる。ただ量があまりに多いので、フルランはマイルストーンごとにまとめて追いかけるか、マシンが空いているときに少しずつ足していくしかない。
証明できないこと：切っているのはプログラム自身が記録した書き込みの流れで、その記録が本物だという前提に立っている——そこは一つ目の実デバイス突き合わせが支えている。本物のディスクの FLUSH が本当に効くかどうかは射程外だ。普段走らせている高速版は時間を節約するため、データブロックを「丸ごと落ちた」か「丸ごと落ちていない」かの二択にしていて、「データブロックが半分だけ落ちた」類は見えない。だからコミット時には相変わらずフルランが要る。そしてフルランは、今日の時点でまだ走り切れていない。
四、モデルとの突き合わせ：正解がないなら、自分で作る
ここまでで証明できるのは、プログラムが自分の理解どおりに動いている、ということだけだ。では、その理解そのものは正しいのか。
メモリ上に、セマンティクスだけを扱い、性能も、クラッシュも扱わない理想のファイルシステムを書いた：crates/singlefs-harness/src/model.rs、13535 行。メモリの中に住んでいるので、動きは安定し、答えは明確だ。
そして同じランダム操作列で、理想モデルと本物の実装を同時に動かす（実装はテスト用のメモリディスクの上で動く）。実装を呼ぶ前に、毎ステップ、モデルに聞く：このステップは「成功すべき」か「拒否すべき」か、それとも「ある範囲内ならどれでもよい」か。モデルの答えはこういう形をしている：
/// 一ステップの操作に対するモデルの答え。
pub struct ModelAnswer {
pub operation: ModelOperationKind,
/// 拒否しなければならない理由：空でなければ必ず拒否
pub required_refusals: BTreeSet<ModelRefusalReason>,
/// 成功したときに書き出されるべきルート、順番どおり
pub expected_roots: Vec<ModelRoot>,
/// コールドスタートの後に読み戻されるべきもの
pub expected_read_back: Option<ModelReadBack>,
/// 巻き戻し下限を引き上げるときの上限値
pub rollback_floor_ceiling: Option<ModelCheckpointTxg>,
// ……
}
実装が走り終えたら、結果を翻訳してモデルの答えと一項目ずつ比べる。食い違いは全部で 28 種類に分けている：成功すべきなのに拒否した、拒否すべきなのに成功した、拒否の理由が違う、拒否する前にこっそりディスクに書いていた、書き出したルートが違う、ファイルの内容が違う、コールドスタートで読み戻したものが違う……モデルが知らないエラーはすべて「説明不能」として記録し、見逃さない。
ランダム操作は現在 20 種類で、16 組の異なる配分がある。いちばんよく使う配分は、「マウント済み、ファイルあり」のとき：上書き 52、巻き戻し下限の引き上げ 16、巻き戻し 10、マウント 6、ファイル削除 3、最新版を捨てるクラッシュ復旧 3。
設計で触れておきたい点が二つある：
- 生成と実行を分ける：生成時の各ステップは「何をするか」と一つのセレクタだけを持ち、具体的な引数は実行の瞬間にディスクの状態から計算する。だから失敗した後で前のステップを削っても後ろのステップは意味を保ち、最短の再現まで縮められる。
-
シードは二度と引き直さない：乱数シードの起点は定数
7_463_871_032_432_355_113に固定してある。もっと試したければ後ろに新しい区間を足していく。古いシードは永遠に再現できる。
モデルと実装が一歩ずつ一致して初めて、我々のセマンティクス——つまり操作の意図——が実装によって忠実に実行されたと言える。
もう一つ、もっと小さな RefFS（参照ファイルシステム、crates/singlefs-reference-filesystem）がある。外部依存は一つもなく、Rust の標準ライブラリだけを使い、メモリ上で POSIX 操作どおりに動く。答える問いは一つだけ：電源断の後に読み出した内容は、許される範囲に入っているか。
/// 一回のクラッシュの後、復旧が読み出してよい状態：{S_j : j = lo、または j がちょうど明示的な発行か巻き戻しの末尾、lo ≤ j ≤ hi}、添字の昇順。
pub struct AllowedSet {
pub lower_bound: StateIndex,
pub upper_bound: StateIndex,
pub allowed: Vec<AllowedState>,
}
人の言葉に直すと：「最後に永続化が確定した版」から「電源断の瞬間」までの間で、明示的なコミットそれぞれの直後の版なら、どれが復旧結果になってもよい。それ以外は一切だめ。理想モデルは「電源断がないときどうあるべきか」を、RefFS は「電源断の後に何が見えてよいか」を担当する。分業だ。
証明できないこと：モデルも、実装も、我々が書いた。両方とも同じ設計文書に沿ってセマンティクスを理解している。両方が一緒に誤解すれば、一緒に緑になる。さらに、今は突き合わせが「走った」ことしか確かめておらず、操作の種類ごとに突き合わせが「届いた」かは確かめていない。新しく足した書き込みパスが、一歩も突き合わされていない可能性がある。
五、形式検証：数学は嘘をつかない
だが、実装の中のいちばん重要な判断が、ランダム操作では決して当たらない入力でだけ間違っていたら？
テストが試せる入力は有限個だ。形式検証は違う：まず、このコードが満たすべき性質（spec）を数学で書き下し、次に証明器に証明させる——あり得るすべての入力について、コードはそれを満たす、と。証明できなければ、そのコードは受け入れない。
我々は Verus で Rust のコードを証明している。たとえば、電源断からの復旧で「ジャーナルから再生してよい区間を取り出す」中核の関数 replay_core（crates/singlefs-replay-prefix/src/lib.rs）は、シグネチャの後ろに前提（requires）と結論（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@), // 前提：ジャーナルのレコードが順に並んでいる
every_counter_has_a_successor(records@),
ensures
replay_follows_the_prefix_rules(...), // どの区間を取るかはルールどおり
replaying_an_applied_record_twice_leaves_the_root_as_once(...), // 同じレコードを二回再生しても一回と同じ
replaying_from_the_landed_root_is_a_fixed_point(...), // 結果からもう一度再生しても結果は変わらない
// もう一つ：再生の結果が出発点より古くなることはない
もっと短いものを二つ：
// レコードを回収してよいかの判断は、この一つの比較だけ。一文字多くても少なくてもいけない
pub fn released_record_can_be_reclaimed(released: bool, generation: u64, floor: u64) -> (answer: bool)
ensures answer == (released && generation <= floor)
// ガベージコレクションの途中で二回電源が落ちても、一回落ちたのと結果は同じ
run_ring_next(run_ring_next(state, RunRingStep::Crash), RunRingStep::Crash)
== run_ring_next(state, RunRingStep::Crash)
肝心なのは、証明しているのが実際に動いているそのコードだということだ。別に書いたモデルではない。復旧パスはこれらの関数を直接呼ぶ。普段のビルドでは Verus の spec と証明の部分が消され、残ったコードがそのまま製品に入る。「証明した版」と「動いている版」がこっそり別れないよう、二通りのビルドが出力する中間コードを一項目ずつ比べ、一字一句同じであることを要求している。
証明されているコードは一つの crate にまとまっている：crates/singlefs-replay-prefix。依存は Verus の標準ライブラリだけで、ファイルは四つ：
| ファイル | 行数 | 証明関数 | 何を証明しているか |
|---|---|---|---|
lib.rs |
4342 | 25 | 電源断からの復旧の三段階：ジャーナルから再生できる区間を取る、いくつかの候補ルートから一つを選ぶ、ジャーナルリングを走査して表を作る |
compaction_plan_proofs.rs |
1588 | 16 | 空間を整理するとき、どの区間を選び、どう移すか |
gc_ring_interval_proofs.rs |
1762 | 20 | ガベージコレクションの移動手順のプロトコルモデル |
gc_crash_proofs.rs |
167 | 2 | 回収前のあの比較 |
証明義務は全部で 113 個。四つのファイルに「成り立つと仮定する」「証明を飛ばす」といった裏口の書き方は 0 箇所だ。
だが形式検証は万能ではない。いちばん陰険な失敗は「証明できない」ことではなく、証明できたのに、何も証明していないことだ。だから、さらに四つを守っている：
一、空虚な真の検査。 前提がそもそも成り立ち得ないなら、そこからは何でも「証明」できてしまう。だから前提ごとに、関数の先頭に assert(false)（偽の表明）を一行差し込み、一箇所ごとに別のコピーを作って、証明が通らないことを要求する。通ってしまえば前提が自己矛盾しているということで、その証明は赤になる。
二、必ず赤になる世界。 わざと壊した箇所を 231 箇所登録してある。一箇所壊すたびに Verus はエラーを出さなければならず、しかもエラーは指定した関数で出なければならない。たとえばこの一箇所：
壊し方：結論を反転する
元： is_last_record == is_last_record_of_its_publish(*record),
変更後：is_last_record == !is_last_record_of_its_publish(*record),
期待： 証明エラー 7 箇所
自分が赤になれることを示せて、初めて証明と呼べる。
三、ツールチェーンの固定。 Verus のバージョン、それが依存する六つのパッケージのバージョンと内容の指紋、Rust コンパイラのバージョン。一つでも合わなければ即座に真っ赤になる。
四、全数探索の反例固定表。 別に一つ実験をして、有限の規模の中で本物のジャーナル再生関数を全数探索した：正当な入力が約 4975 万通り、悪意のある入力が約 6451 万通り。反例が一つ出るたびに、そのまま一つの表に釘付けする。今は 360 行。コミットのたびに、今のコードでこれを一行ずつ再生する。
正直に言うと、形式検証は高くつく。今日の時点でも、覆っているのはいちばん中核の判断がいくつかだけだ：ジャーナルからどの区間を取るか、どのルートを選ぶか、ジャーナルリングの走査、整理の計画、回収のしきい値。ディスク上のバイトがどうやってこれらの関数の入力に解析されるか、ディスクのバリア、エンコードとデコード、チェックサム、複数ディスク、整数オーバーフロー——どれも証明の外だ。コードディレクトリの説明ファイル自身がこう書いている：「ファイルシステム全体の完全なクラッシュ復旧の証明とは呼べない」。
もう一つ、はっきり言っておかなければならない：Verus が証明するのは「コードが spec に合っている」ことであって、「spec そのものが正しい」ことは証明できない。spec を書き間違えても、証明は普通に通る。spec が正しいかどうかは、設計文書での論証と、ここまでの関門との相互の裏付けにかかっている。
六、ミューテーション：審判を審判する
では、検証そのものが偽物だということはないか。テストが届いていない、アサーションが逆向きに書かれている、サンプリング点がたまたま二つの書き方で同じ結果になる場所に選ばれている——こういうとき、テストは普通にオールグリーンだが、何も判定していない。
理屈は単純だ：コードをわざと壊して、検証が赤になるかを見る。赤になれば、その検証にはこの種の誤りを見分ける力がある。壊しても緑のままなら、その検証は飾りだ。
具体的には二つある。
一、バグを一つ直すたびに、地雷を一つ埋める。 crates/mutations.tsv は全部で 5981 行。各行に、どのファイルを、どの原文から何に書き換え、どのテストを走らせ、どのテストが赤にならなければならないかが書いてある。たとえば：
名前 ：割り当て後に空き数が減らない（空間の帳簿の検査が赤にならなければならない）
ファイル ：crates/singlefs-core/src/allocator.rs
原文 ：self.free_slots -= span;
変更後 ：// 変異：空きを減らさない
必ず赤 ：cold_start_reads_the_second_content_and_the_pool_checker_stays_green
表のヘッダには由来が書いてある：敵対的レビューで問題が見つかって直すたびに、「元に戻せば赤になる」変異を一つ残す。直し方がこっそり取り消されたとき、ここが先に鳴る。いつか誰か（たいていはどこかの agent）が直し方をこっそり元に戻しても、地雷が先に鳴るわけだ。原文はファイルの中でちょうど一箇所見つからなければならない。コードが変わって原文が見つからなくなれば、その行は「アンカー失効」として記録され、やはり赤になる。
二、広域ミューテーション。 地雷は人間が埋めるものだから、思いつかない場所が必ずある。そこで、ミューテーションを自動生成するツールがもう一つある（scripts/mutation/broad-mutation.py、中では cargo-mutants を使っている）：比較演算子をひっくり返す、定数に一を足す・引く、文を一行消す……2026-09-30 に一度数えたところ、checker から 1765 個、コアのコードから 3326 個生成できた。一つ残らず結論が出ていなければならず、赤にならないものが一つでもあればコミットできない。細かい点をいくつか：
- タイムアウトやメモリ上限への到達は捕まえたことにならない。条件を引き上げてもう一度走らせ、二回ともタイムアウトし、しかも証拠が揃っている場合に限る。
- 結論は関数の指紋で再利用する：それを捕まえたテストが変わっておらず、それが入っている関数も変わっていなければ、走らせ直さない。
- 結論ライブラリの各行には、リポジトリの外にある鍵で計算した署名が付いている。防いでいるのはハッカーではなく、agent がついでに結論を一行書き換えることだ。
前の関門の「必ず赤になる世界」も、実は同じ考え方だ：証明を壊したら、証明器はエラーを出さなければならない。
ミューテーションが赤にならなかったとき、いちばん楽なのは「この二つの書き方はもともと等価だ」と一言書いて立ち去ることだ。プロジェクトのルールはそれを許さず、「赤にならなかった」を八つに分類している。いちばんよく濫用されるのはこれだ：自分が選んだいくつかのテスト入力でたまたま同じ結果になっただけで、入力を変えれば違う。この場合は入力を一つ足さなければならず、等価だとしてごまかしてはいけない。判断基準は一文だけ：
ミューテーションが捕まらなかったら、一度問え：サンプリング点を変えても、まだ同じ値か？
証明できないこと：ミューテーションが証明するのは「アサーションは赤になれる」ことであって、「カバレッジが完全だ」ことではない。表に書かれていない壊し方は永遠に試されないし、自動生成できる変異の種類にも限りがある。
七、プールレベル checker：どのディスクでも拾い上げる
最後に、どんなディスクでも拾い上げたとき、それが正当な singlefs のディスクかどうかをどう判定するか。
それがプールレベル checker だ。先に一つはっきりさせておく：これはマウント時に走るものではない。マウントはコア自身の復旧と検証のコードを通る。checker は独立した監査役で、テスト、クラッシュポイント再生、GPU との突き合わせの中で呼ばれる。マウントと監査は同じことをそれぞれ一回ずつ判定し、使っているコードは別々だ。
入口は関数一つだけ（crates/singlefs-checker/src/walk.rs）：
pub fn check_pool_image(reader: &dyn ImageReader) -> Vec<(&'static str, InvariantVerdict)>
入力はバイトだけだ。ImageReader が渡すのは「ディスクが何枚あるか、それぞれの大きさ、あるディスクのある位置から何バイトか読む」だけで、実行時のメモリ状態には一切触れない。出力はルールごとに一つの判定：
/// 一つのイメージ上での一つの不変条件の判定。「適用外」には理由が必須で、黙って成立扱いにしてはならない。
pub enum InvariantVerdict {
Holds, // 成立
Violated(String), // 違反、どこかを書く
NotApplicable(&'static str), // 適用外、理由が必須
PartiallyJudged(String), // 判定できた部分はすべて正しく、判定できない部分が別にある：赤でもなく、成立でもない
}
まずディスクごとにシステム構成を読み、最新の有効なルートを選び、ジャーナルを走査してその版を再生する。それから二つの方向でそれぞれ一回歩く：
- 参照をたどる：ルートから出発し、inode ツリー、削除記録、スナップショットの系譜など、すべてのツリーを末端までたどる。
- ブロックごとに走査する：誰が誰を参照しているかは気にせず、ディスク上の全ブロックの自己記述ヘッダを一つずつ読み、インデックス全体を組み直す。
二つの方向で組み上がったインデックスは、完全に同じでなければならない。最後に、走査で得た空間の使用量を、ディスク上に記録された帳簿とディスクごとに突き合わせる。
checker が判定するルールの一覧は crates/singlefs-checker/invariants/ にあり、実装済みは 109 本。コードの IMPLEMENTED_INVARIANTS: [&str; 109] と一対一に対応している。いくつか挙げる：
- 各ブロックのヘッダに記録された身元は、そのブロックを参照している場所と一致しなければならない。 冒頭で言った「どのブロックも単体で拾い上げれば、私は誰か、誰に属しているか、何世代目かに答えられる」が、コードになったものだ。
- 有効なルートは、最新のもの以外に、少なくとももう一つ古いものがなければならない。 なければ赤。それは「次に書き損じたら、もう退路がない」ことを意味するからだ。
- 帳簿上の「割り当て済み」の空間は、実際に参照をたどって計算した空間と等しくなければならない。
- ディスクごとの「割り当て済み − 解放待ち」は、最新版が実際に占めているブロック数と等しくなければならない。 読むのはディスク上の帳簿で、メモリ上のアロケータは読まない。
実装済みのルールには、どれも「わざと壊して、ちょうどそれを引き起こす」壊れたディスクが一枚ずつ付いている。
プールレベル checker は、コアのコードとロジックを一行も共有してはならない。共有するのはフォーマット定数のモジュール一つだけだ。その Cargo.toml の依存は一行しかない：
[dependencies]
singlefs-format = { path = "../singlefs-format" }
このフォーマットモジュールには if、match、for すら書いてはならず、定数だけを置く。設計規律にこういう一文がある：
禁止されているのは「走査」ではなく、二つのことだ：「答えが必要なその瞬間にまだ答えがない」こと、そして「監査する側とされる側が同じコードを使う」こと。実行時と checker は異なるアルゴリズムを使わなければならない。
両者が解析コードを共有していれば、そのコードが一度間違えば両方が同じように間違え、突き合わせは相変わらずオールグリーンになる。だからゲートが厳しく押さえている：二つのモジュールの依存は、フォーマット定数を除いて一切交わってはならない。「参照をたどる」方向と「ブロックごとに走査する」方向が呼ぶ関数も、共通部分はフォーマットの解析と定数だけに限られる。
同時に、checker は一つの仕様でもある。「このフォーマットとは結局何なのか」を定義している。singlefs のフォーマット全体は checker のソースを正とし、文書もそれ以外の場所もこれを基準にする。
証明できないこと：見ているのは静的なディスク一枚だけだ。暗号化に関するルールはまだ一本も実装していない。「正方向の参照と逆引きインデックスが互いに一致する」というルールも、まだ補うべき一覧に入ったままだ。ルールにはこう書いてある：「checker が何も報告しなかった」ことは「ディスクが健全だ」ことを意味しない。一覧に書かれていない誤りは、checker には見えない。
最後に
どの関門にも足りないところと欠点があり、どれも単独ではコードの正しさを保証できない。だが互いに支え合っている：
- 形式検証は最も中核の判断を証明したが、周りのグルーコードは見ない → クラッシュポイント再生とプールレベル checker がグルーを支える。
- クラッシュポイント再生は、記録した書き込みの流れが本物だと前提している → 実デバイス突き合わせが門の外でもう一本記録する。
- herd7 は CPU の並べ替えを見るが、ディスクの永続化順序は見ない → 実デバイス突き合わせとクラッシュポイント再生が検出できる。
- バリアが一つ抜けても、結果判定には見えない → レコード照合器には見える。
- 理想モデルと実装が一緒に誤解しているかもしれない → RefFS がもう一枚の新しい鏡になる。
- どの関門も永遠に緑のままかもしれない → 対照群、必ず赤になる世界、空虚な真の検査、ミューテーション表が、一つずつ自分が赤になれることを証明する。
これらの関門が組み上げたシステムは、ベルリンの壁のようなものだ。高くはない。越えたい？ ビッグ・ブラザーが見ているぞ。
この壁が堅固だと、どう証明するのかね。ゴルバチョフ同志。