シミュレーション、ゲーム経済、複数期にわたるバッチ処理、あるいは会計の月次・年次締め処理など、状態が期（ステップ）をまたいで累積していくシステムを開発していると、奇妙な現象に突き当たることがあります。単体テストは 100% 通過し、三面等価の保存則テストもすべて緑（パス）で、AI エージェント（Claude Code や自律ワーカー）と協業して整備したプルリクエストの CI やコードレビューを完全にクリアしたはずのコードが、実際に運用環境で時間を進めた途端、ある日突然「状態が完全に静止する」「特定のリソースが一方通行に偏って枯渇する」といったサイレントな破綻を起こす現象です。

シミュレーションにおける 1期の不変条件テスト とは、1ステップ（1期）内の人口保存則や資金保存則など「悪いことが起きないこと（Safety）」を検証する局所テストであり、期をまたいで累積する微小な端数切り捨てや処理順序の偏り（状態のドリフト）を検証する 長期推移テスト（Liveness / DST）と対比されます。

私たちが AI エージェントと協業して個人で開発中の自作ゲーム（非公開。以下、プロジェクトA）のシミュレーションエンジンでも、まったく同じ壁に直面しました。エージェントが作成した関数の実装、単体テスト、PR の自動コードレビューをすべて通過していたにもかかわらず、1年 = 25期として設計された人口・経済シミュレーションにおいて、初期人口 100 人（子供 18 人、成人 36 人、老人 36 人、冒険者 10 人。子供の内訳は男児 9 人、女児 9 人）の都市を動かしたところ、50 年間（1,250期）にわたり人口が初期値の 100 人から 1 人も動かない「人口凍結」が発生しました。さらに、別の修正後に施策を実行しながら 20 年間（500期）進行させたところ、男児が 9 人から 1 人へ激減し、女児が 9 人から 23 人へと激増する「男女比の崩壊」に見舞われたのです。

これらのコードは、1 期ごとの出生数や死亡数、人口保存則を検証する単体テストをすべてクリアしていました。なぜ 1 期の不変条件テストをすり抜けて長期の破綻が起きたのか。本記事では、自作ゲームで露呈した 4 つの失敗パターンをコードと実測ログから解剖し、Safety と Liveness の理論的背景、および時間を早送りして推移を検証する「決定論的シミュレーションテスト（DST）」の実践的な設計論を共有します。

なぜ1期のテストをすり抜けたのか：4つの失敗パターンの解剖

すべての単体テストと保存則テストがパスしていたにもかかわらず、長期実行で露呈した不具合は次の 4 つでした。いずれも「1期の中では完全に正しい計算」が行われていたことが、発見を遅らせた共通の原因でした。

パターン1: 率×人数の端数切り捨てによる人口凍結

最初の不具合は、初期人口 100 人の都市において、50 年間（1,250期）まったく人口が変動しなかった現象です。

シミュレーションエンジンでは、毎期の出生率や死亡率を千分率（‰）として定義し、整数演算（除算による切り捨て）で当期の人数を算定していました。しかし、初期人口 100 人という小規模な都市では、各年齢層の人数が小さいため、率を掛けた結果が毎期 1 未満になっていました。

  • 成人女性からの出生: 11 人 × 5‰ = 0.055 人 → 0 人に切り捨て
  • 老人の自然死亡: 18 人 × 8‰ = 0.14 人 → 0 人に切り捨て
  • 年齢層の加齢推移: 18 人 ÷ 375 期（子供期間15年＝375期） = 0.048 人 → 0 人に切り捨て
  • 冒険者のダンジョン死亡: 10 人 × 10‰ = 0.1 人 → 0 人に切り捨て

この結果、毎期の変動量が全項目で 0 人となり、都市の人口動態が完全に停止しました。数学的には、固定的な切り捨て演算が引き起こす停滞（stagnation）現象として解析されている挙動です1。

以下のコードは、人口凍結を引き起こしていた当時の出生計算ロジックの抜粋です。

引用元: プロジェクトAの population.rs

        // Births from general adult females only
        let births = (u64::from(self.general.adult_female)
            * u64::from(effective_birth_rate_permille)
            / 1000) as u32;
        let male_births =
            (u64::from(births) * u64::from(BIRTH_SEX_RATIO_MALE_PERMILLE) / 1000) as u32;
        let female_births = births.saturating_sub(male_births);

このコードを実行し、50年分（1,250期）進めたときの実測ログが以下です。施策なし（何もしない）だけでなく、住宅やインフラを拡張して収容可能人口（cap）を 1,120 人まで増やした施策環境であっても、人口が 100 人（子18 成36 老36 冒10）のまま 1 人も動いていないことが記録されています。

--- 何もしない
y1 pop=100 (子18 成36 老36 冒10) cap=100 [住100 水100 食100 衛100] wall=50 used=48 国庫=113975
...
y50 pop=100 (子18 成36 老36 冒10) cap=100 [住100 水100 食100 衛100] wall=50 used=48 国庫=798750
--- 人口を増やす
y1 pop=100 (子18 成36 老36 冒10) cap=160 [住170 水160 食160 衛160] wall=80 used=74 国庫=72552
y50 pop=100 (子18 成36 老36 冒10) cap=1120 [住1130 水1130 食1130 衛1120] wall=470 used=463 国庫=34468

1 期の人口保存則テストの視点から見ると、「前期の人口 100人 + 出生 0人 - 死亡 0人 = 今期の人口 100人」という等式は何の破綻もなく成立します。そのため、ユニットテストも CI もこの静止をまったく検知できませんでした。

パターン2: 男女振り分けの端数切り捨てによる男女比崩壊

人口凍結に対処するため、端数を持ち越すバッファを導入したところ、今度は別の端数切り捨てによって男女比が極端に崩壊する不具合が発生しました。

端数バッファの導入により、出生数そのものは 0〜1 人ずつ平滑化されて生まれるようになりました。しかし、生まれた赤子を男児と女児に振り分ける処理において、男児比率（BIRTH_SEX_RATIO_MALE_PERMILLE = 500）を乗じた後に 1,000 で除算する切り捨てが行われていました。

引用元: プロジェクトAの population.rs

        let births = settle(
            &mut self.remainders.births,
            birth_num,
            1_000_000_000_000,
            u32::MAX,
        );
        let male_births =
            (u64::from(births) * u64::from(BIRTH_SEX_RATIO_MALE_PERMILLE) / 1000) as u32;
        let female_births = births.saturating_sub(male_births);

1 期に生まれる赤子が 1 人のとき、1 × 500 ÷ 1000 = 0 となり、男児の出生数は常に 0 人と計算されます。そして残りの全員（1 人）が女児として割り当てられました。この結果、20 年間（500期）シミュレーションを進めた実測ログでは、初期に男児 9 人・女児 9 人だった子供の内訳が次のように歪みました。

男児: 9人 → 1人
女児: 9人 → 23人（20年目）

ここでも、1 期の中では「男児 0人 + 女児 1人 = 出生数 1人」という保存則が 100% 成立しています。定数も 500‰ と公平に設定されており、単体テストは何の警告も出しませんでした。1 人ずつの離散化における丸め方向の偏りが、時間軸で一方通行に累積して初めて顕在化したバグでした。

パターン3: 引退・死亡の処理順序固定による成人女性の一方通行吸収

3 つ目は、処理順序の固定化によって特定属性の人口が別枠へ一方通行に吸い取られ続けた問題です。

初期設計において、世界観の要件から成人男性比率が約 694‰ と高めに設定されていました。その環境下で、冒険者の引退処理およびダンジョンでの死亡処理を実装した際、「リストの先頭（男性）から優先して引退・死亡枠を埋める」という順序固定の実装が行われていました。さらに、一般成人から冒険者へ就業（クラスチェンジ）する処理でも、男性から優先的に採用されていました。

この結果、女性の冒険者がほとんど引退・死亡しなくなり、一般の成人女性枠から冒険者枠へと女性が吸い上げられ続けました。500 期の実走において、修正前は成人が男 234 人に対して女 110 人、冒険者が男 89 人に対して女 50 人という極端な不均衡に固定されました。

1 期の処理としては、「今期引退すべき指定人数が正しく引退したか」「死亡枠の人数が保存されているか」という条件をすべて満たしていました。しかし、選択アルゴリズムの静的な順序バイアスが、長期実行において特定グループの不可逆な流出を引き起こしていました。

パターン4: 施策（移住）の実装漏れによる推移の完全一致

4 つ目の失敗は、仕様として定義されていたロジックがシミュレーションループから呼ばれていなかったという、結合レベルの欠落です。

都市の収容人口を広げる施策を打った際、外部からの「移住」によって人口が流入する仕様が設計されていました。しかし、シミュレーションループの実装から移住の呼び出しが抜け落ちていました。

その結果、施策を一切打たずに放置した都市（収容人口 100 人）と、国庫を投じてインフラを拡張した都市（収容人口 900 人）を 50 年間回したところ、人口推移が 1 年目（93人）から 50 年目（48人）まで、1 人の狂いもなく完全一致（1 年目 93人 → 5 年目 70人 → 50 年目 48人）しました。

インフラ施設の建設処理、費用の引き落とし、収容能力の計算ロジック自体は単体テストで完璧に動作していました。しかし、算定された収容能力が人口動態へとフィードバックされる唯一の結合経路が欠落していたため、50 年間の推移を比較して初めて「施策が一切人口に影響を与えていない」という事実が判明したのです。

なぜ長期推移テスト（DST）を導入したのか：実務での選択理由

これら 4 つの破綻を経験したことで、私たちはテスト設計の前提を根本から見直すことになりました。

Safety（安全性）と Liveness（活性）の二分法

分散システムや並行プログラミングの形式手法において、システムの性質は伝統的に Safety（安全性） と Liveness（活性） の 2 つに分類されます23。

  • Safety（悪いことが起きないこと）: 有限の時間内で不整合や不正な状態が発生しない性質。人口や資金の保存則が守られていること、不正なパラメータによる更新が拒絶されること。何もしないシステム（完全に静止したシステム）も、自明に Safety を満たします。
  • Liveness（望ましいことが起き続けること・前進すること）: 時間が経過するにつれて、望ましい状態へと前進・循環する性質。人口が停滞せず世代交代すること、施策に応じて状態が有意に変化すること、特定の属性が絶滅しないこと。

シミュレーション工学における分類でも、Robert G. Sargent はプログラムが仕様通りに実装されているかを問う「Model verification（検証）」と、動的モデルの振る舞いが意図した目的に対して妥当かを問う「Model validation（妥当性確認 / Operational validity）」を明確に区別しています4。

1 期の不変条件テストは、本質的に Safety の検証（Model verification） です。しかし、私たちが直面した人口凍結や男女比崩壊は、Safety が 100% 守られているにもかかわらず、システムの前進や循環が停止・偏向する Liveness の喪失（Model validation の失敗） でした。

この課題に対し、分散トランザクション DB の TigerBeetle では、決定論的シミュレーションテスト（DST）において Deep Safety 不変条件と Deep Liveness 不変条件を峻別し、長期間のシミュレーションループの中でクラスタが活性を保ち前進しているかを監視する設計を採用しています56。また FoundationDB では、離散イベントシミュレーションによって仮想時間を早送りする Time Dilation を用い、数年分に相当する耐障害性シナリオを短時間で決定論的に再現・検証しています7。

私たちに必要なのも、1 期の Safety テストをいくら厚くすることでもなく、時間を早送りして Liveness と状態推移を検収するテストゲート でした。

乱数に頼らず決定論性を保つ累積剰余バッファ

端数切り捨てによる人口凍結や偏向を解決する際、一般的なアプローチとしては確率的丸め（stochastic rounding）や乱数による振り分けが考えられます。しかし、テストの再現性を最重要視するシミュレーションにおいて、安易に乱数を導入するとテストオラクルの固定が極めて難しくなります。

そこで私たちは、乱数を使わずに決定論性を 100% 維持したまま端数を回収する 累積剰余バッファ（carry-over remainder buffer） を導入しました。毎期の計算で生じた端数（割り算の余り）を状態として保持し、次期以降に加算して繰り上げるアルゴリズムです。

以下は、シミュレーションエンジンで端数を決定論的に処理するために実装された settle 関数の抜粋です。

引用元: プロジェクトAの population.rs

pub(crate) fn settle(remainder: &mut u64, numerator: u64, den: u64, cap: u32) -> u32 {
    let total = *remainder + numerator;
    let whole = u32::try_from(total / den).unwrap_or(u32::MAX).min(cap);
    *remainder = total - u64::from(whole) * den;
    // Do not bank more than one term's worth of fraction when capped by availability.
    *remainder = (*remainder).min(den - 1);
    whole
}

分子に前回の余りを足し合わせ、分母で割った商を当期の確定人数として返し、余りをバッファに残します。これにより、微小な変化量であっても期をまたいで確実に積算され、浮動小数点数を使わずに整数演算だけで長期の期待値を厳密に維持できるようになりました。

50年高速実行で推移と分布を検証する長期テスト

累積剰余バッファを導入した上で、4 つの破綻の再発を構造的に防止するため、初期状態から 50 年間（1,250期）を高速に回す長期シミュレーションテストスイートを配備しました。

引用元: プロジェクトAの long_run_test.rs

#[test]
fn test_population_moves_over_50_years() {
    let run = play(Strategy::None);
    let initial = run.totals[0];
    assert!(
        run.totals.iter().any(|&t| t != initial),
        "population never moved from {initial}"
    );
    assert_ne!(run.totals.last(), Some(&initial));
}

#[test]
fn test_child_sex_ratio_stays_in_range() {
    for strategy in Strategy::ALL {
        let run = play(strategy);
        assert!(!run.child_shares.is_empty(), "{}", strategy.name());
        for share in run.child_shares {
            assert!(
                CHILD_MALE_SHARE_PERMILLE.contains(&share),
                "{}: male share of children {share}‰ (#53)",
                strategy.name()
            );
        }
    }
}

#[test]
fn test_adventurers_never_die_out() {
    for strategy in Strategy::ALL {
        let run = play(strategy);
        assert!(run.min_adventurers > 0, "{}", strategy.name());
    }
}

#[test]
fn test_population_focus_diverges_from_no_policy() {
    // Capacity growth only matters if people can move in (#50): with migration removed, both
    // runs measured the same final total (232).
    let none = play(Strategy::None);
    let focus = play(Strategy::PopulationFocus);
    assert_ne!(none.totals, focus.totals);
    assert!(
        focus.totals.last() > none.totals.last(),
        "population focus ended at {:?}, no policy at {:?}",
        focus.totals.last(),
        none.totals.last()
    );
}

このテストスイートは、以下の 4 点を検証しています。

  1. test_population_moves_over_50_years: 人口が初期値 100 人から動いていること（完全静止の検知）。
  2. test_child_sex_ratio_stays_in_range: 子供の男児比率が健全な帯域（400‰〜600‰）に収まり続けること（男女比崩壊の防止）。
  3. test_adventurers_never_die_out: 冒険者人口が枯渇（0 人）しないこと（循環停止の防止）。
  4. test_population_focus_diverges_from_no_policy: 施策ありと施策なしで推移が有意に分岐（Diverge）すること（施策の結合漏れおよび端数切り捨て停滞の検知）。

システムの健全性を担保するには、1ステップ内の局所的不変条件と、複数ステップにわたる大域的推移の両面からテストを設計する必要があります。両者の役割の違いを整理したのが下表です。

比較軸1期の不変条件テスト（局所検証）長期シミュレーションテスト（DST / 推移検証）
検証の対象（空間）原因の空間（1ステップ内の不変量・保存則）結果の空間（時間累積推移・分布・状態乖離）
形式手法上の分類Safety Property（悪いことが起きない）Liveness Property（良いことが前進・循環する）
検知できる主な不具合資金や人口の即時リーク、不正な入力パラメータ端数切り捨ての累積停滞、順序バイアス、施策の未結合
テストオラクル（期待値）完全一致（三面等価・計算式通りの値）許容帯域（レンジ）・非静止・メタモルフィック関係（施策差分）
実行時間とコスト極めて高速（マイクロ秒単位・数千ケース即時）高速だが一定のループを要する（ミリ秒〜秒単位）

このように、1 期の不変条件テストと長期推移テストは排他ではなく補完関係にあります。1 期の保存則（Safety）を基盤として敷いた上で、長期推移（Liveness）を重ねて検証する二層構造こそが、状態が積み上がるシステムにおける本質的な品質ゲートとなります。

長期テストのトレードオフと適用限界

長期シミュレーションテストは強力ですが、実務に導入する際にはいくつかのトレードオフと設計上の制約が存在します。

実行時間とCI負荷（Time Dilation による解決）

長期テストを導入する際に最も懸念されるのは、CI の実行時間です。「50 年分のシミュレーション」と聞くと長時間の処理を想像しがちですが、FoundationDB の Time Dilation アプローチ7 が示すように、I/O や実時間タイマー、UI レンダリングを完全に分離した純粋ロジックとしてループを設計すれば、実行時間は極めて短く抑えられます。

プロジェクトAにおいても、50 年間（1,250期）のテストは純粋なメモリ上での状態遷移として実行されるため、CI 環境でわずか数ミリ秒から数十ミリ秒で完了します。スリープや非同期待機を排除し、離散ステップを決定論的に回すアーキテクチャを守る限り、CI の高速性を損なうことはありません。

テストオラクル問題（正解の決め方）

長期テストにおける最大の難所は、「何を期待値（テストオラクル）とするか」 という問題です。

複数期にわたるシミュレーションでは、微小な差分が非線形なフィードバックを通じて拡大していくため、「50年後の人口が厳密に232人になる」といった 1 点一致のオラクルを作成すると、わずかなパラメータ調整でテストが頻繁に壊れる脆弱なテスト（脆いテスト）になります。

このオラクル問題に対し、私たちは以下の 3 つのアサーションパターンを組み合わせて対処しました。

  1. 許容レンジ（Range Assertion）: 比率や分布が健全な帯域に収まっているかを検証する（例: 出生男児比率が 400‰〜600‰ に収まること）。
  2. 非静止アサーション（Non-stagnation）: 状態が初期値から一切動かない凍結状態（人口凍結）に陥っていないかを検証する。
  3. メタモルフィック関係（Metamorphic Testing）: 正解の値が事前に分からないアルゴリズムをテストする際、入力を変化させたときに出力がどう相対的に変化すべきかという「変形関係」を検証する手法です8。施策ありと施策なしを並行して走らせたとき、最終結果が一致せず有意に乖離（Diverge）していることをアサーションすることで、施策の実装漏れを確実に検出できます。

長期テストの限界と「書けないこと」の境界

長期テストを導入したからといって、シミュレーションのあらゆる不具合が自動的に防げるわけではありません。

実際のコードコメントにも明記されている通り、私たちが配備した long_run_test.rs は、人口凍結（施策差分経由）、施策未結合、出生男女比の偏向を検知できますが、成人男女の不均衡（パターン3）は検証項目に含めていないため、このテスト単体ではすり抜けます。初期状態の成人は男性比率が約 694‰ と高めに設定されており、テストが明示的に成人の男女比率をアサーションしない限り、長期テストであっても検知はできません。

また、長期テストだけに頼って 1 期の単体テストを疎かにすると、長期テストが失敗した際に「1,250 期のどのステップの、どの計算式で狂いが生じたのか」という原因特定（デバッグ）が困難を極めます。原因を局所化する単体テストと、結果の妥当性を担保する長期推移テストの二層構造が不可欠です。

以前、別の記事「AI が連続で書いたコードをレビューせず放置したら、機能が壊れてテストコードだけが残った」でも触れたように、テストが緑であることそのものを過信してはならず、そのテストが「何を保証し、何を保証していないのか」の境界を常に把握しておく必要があります。

AIエージェント協業時代における品質ゲートの再定義

昨今、Claude Code や自律ワーカーをはじめとする AI エージェントを活用して、コードの実装から単体テストの作成、PR の作成までを自動化する開発スタイルが急速に普及しています。私たちの自作ゲーム開発でも、まさにこのエージェント協業体制によってシミュレーションエンジンを実装していました。この実体験において、今回の教訓は極めて重要な示唆を与えています。

エージェントに渡すテスト計画の範囲

AI エージェントは、与えられた関数のシグネチャや仕様書に基づき、1 ステップの整合性や不変条件（保存則など）を満たすコードと単体テストを極めて迅速かつ高精度に生成します。計算式の型チェックや、三面等価の等式が成り立つことの検証コードを書かせることにおいて、エージェントは非常に強力です。

しかし、1 期の単体テストが緑になったからといって、期をまたぐ振る舞いが健全である保証にはなりません。なお、今回 50 年分の推移を回して原因を突き止める作業そのものは、エージェントに任せています。テストの計画に「1 期の計算だけでなく、長期の計算でも破綻しないこと」と最初から書いておけば、長期のテストも作ってくれたのではないかと考えています。

テスト通過（CI 緑）を過信しない姿勢

「テストが通っている」という事実は、「仕様が完全に守られている」ことと同義ではありません。既存のテストスイートそのものが、1 ステップの局所的で弱い挙動しか前提にしていない可能性があるからです。

テストがすべて成功しているときこそ、「このテストは 1 期の Safety しか見ていないのではないか」「時間経過に伴うドリフトを疑うテストが存在しているか」という批判的な視点を持つことが不可欠です。

テストの計画に長期の範囲を入れる

局所的なテストだけでは足りません。1 期分に限らず、25 期（1 年）や 10 年のように、期をまたいで進めるテストを計画に含めておく必要があります。誰がテストを書くかより、計画の段階で長期の範囲が入っているかのほうが大事だと考えています。

よくある質問（FAQ）

Q. 1期の不変条件テスト（ユニットテストや保存則テスト）だけでシミュレーションの正しさを保証できないのはなぜですか？

A. 1期の不変条件テストは「その 1 ステップの中で悪いことが起きないこと（Safety）」しか検証できず、微小な端数切り捨てや処理順序の偏りが期をまたいで累積するドリフト（累積誤差）を原理的に検出できないためです。例えば、毎期の人口保存則や資金保存則が 100% 満たされていても、端数切り捨てで変化量が毎期ゼロになれば人口は静止し、男女比の計算が毎回一方に丸められれば長期で極端な偏向が生じます。

Q. 長期シミュレーションテストにおいて「期待値（テストオラクル）」はどのように設計すべきですか？

A. 厳密な 1 点の一致ではなく、「許容レンジ（分布幅）」「非静止アサーション」「施策間の乖離（メタモルフィック関係）」という 3 つの判定基準で設計します。長期実行では状態の相互作用によって 1 人単位の厳密解を固定することが困難なため、男女比などの比率が健全な帯域（例: 400‰〜600‰）に収まっていること、状態が初期値から凍結せず推移していること、施策の有無で将来の推移が有意に分岐することをアサーションします。

Q. AIエージェントと協業してシミュレーションやバッチ処理を開発する際、設けるべき品質ゲートは何ですか？

A. 1 ステップのコードレビューや単体テストの合否だけに頼るのではなく、時間を早送りして長期間の推移を観測する「決定論的シミュレーションテスト（DST）」を必須のゲートとして課すことです。1 期の不変条件を満たすテストだけでは、期をまたぐ微小な偏向や施策の結合漏れは捕まりません。「50年〜100年分を瞬時に回して推移と分布を確かめる自動テスト」をゲートに組み込むことが最も確実な防壁となります。

まとめ

本記事で解説した知見と設計判断の基準は、以下の 5 点に集約されます。

  • 1期の不変条件（Safety）は長期の健全性（Liveness）を保証しない: 1 ステップ内の保存則が完全に成立していても、端数切り捨てによる人口凍結や順序固定による偏向吸収は発生する。
  • 決定論性を崩さずに端数を制御するには累積剰余バッファが有効: 乱数に頼らず、余りを状態として期をまたいで持ち越すことで、微小な変化量であっても長期の期待値を厳密に維持できる。
  • 長期テストのオラクルは「レンジ・非静止・施策差分」で設計する: 厳密な 1 点の一致ではなく、分布の健全帯域、状態の推移、施策ごとの分岐（メタモルフィック関係）を検証する。
  • 単体テストと長期テストは両輪である: 原因の特定には局所の単体テストが、結果の妥当性には長期推移テストが必要であり、二層構造で品質を担保する。
  • テストの計画に長期の範囲を入れる: 1 期の計算だけでなく、1 年・10 年と期をまたいで進めても破綻しないことを、最初からテストの計画に含めておく。

状態が期をまたいで積み上がる複雑なシミュレーションやバッチ処理のアーキテクチャ設計、AI エージェントと協業する開発プロセスの品質ゲート設計について、ぜひ コンタクトフォーム よりお気軽にご相談ください。

Footnotes

  1. Stochastic rounding: implementation, error analysis and applications Matteo Croci, Massimiliano Fasi, Nicholas J. Higham, Maryam Mikaitis、Royal Society Open Science, Vol. 9, Issue 3、2022年3月。Section 6: Rounding error analysis with SR (§6.1)。固定的な切り捨てや丸めによる停滞（stagnation）現象の数学的解析。 ↩

  2. Proving the Correctness of Multiprocess Programs Leslie Lamport、IEEE Transactions on Software Engineering, Vol. SE-3, No. 2、1977年3月、pp.125-143。Safety property（悪いことが起きない）と Liveness property（望ましいことが起きる）の二分法の導入。 ↩

  3. Defining Liveness Bowen Alpern, Fred B. Schneider、Information Processing Letters, Vol. 21, Issue 4、1985年10月。すべてのプログラム特性が Safety と Liveness の積集合として表現される定理の証明。 ↩

  4. VERIFICATION AND VALIDATION OF SIMULATION MODELS Robert G. Sargent、Proceedings of the 2010 Winter Simulation Conference、2010年12月、pp.166-183。Model verification（仕様通りの正しさ）と Model validation（動的振る舞いの妥当性）の分離、および operational validity。 ↩

  5. Protocol-Aware Deterministic Simulation Testing TigerBeetle チーム、2026年8月20日、公式技術ブログ。セクション3。プロトコル認識型シミュレーションによるレプリカ単位の Deep Safety / Deep Liveness 不変条件検証、回復停止の検知。 ↩

  6. Simulation Testing For Liveness TigerBeetle チーム、2023年7月6日、公式技術ブログ。セクション3。シミュレータ VOPR による Liveness 検証手法、長期間シミュレーションによる状態遷移の進行監視。 ↩

  7. FoundationDB: A Distributed Unbundled Transactional Key Value Store Jingyu Zhou et al.、Proceedings of the 2021 International Conference on Management of Data (SIGMOD ‘21)、2021年6月。Section 4: Simulation Testing pp.2657-2658。離散イベントシミュレーションによる Time Dilation（時間早送り）、完全決定論的シミュレーションと疑似乱数シード。 ↩ ↩2

  8. 「正解が分からない」アルゴリズムをどうテストするか kam6ri、Hacobell Tech Blog、2025年12月18日。Property-based Testing と Metamorphic Testing による正解が定まらないロジックの検証手法。 ↩