安全臨界ソフトウェア認証と Almide のギャップ

人命に関わるソフトウェア(航空・自動車・医療)を正式投入するために要求される認証基準と、Almide の現在地の差分。要点は「機械証明されたメモリ安全な言語」は射程内だが、「安全臨界認証をそのまま満たす完全性」は別プロジェクト規模、という見立て。

3つの主要基準

DO-178C には形式手法を認証エビデンスに使える補遺 DO-333、ツール認定の DO-330 があり、機械証明を正面から評価に組み込める枠組みは既に存在する。

「正しいコード」を超えて要求されるもの

認証は「動く」「正しい」だけでは通らない。質的に別のものが要る。

1. エンドツーエンドの証明連鎖 — ソース→中間表現→バイナリまで、証明が途切れず繋がっていること。一部だけ証明されても安全臨界では意味を持たない。
2. 検証範囲の網羅 — メモリ安全だけでなく、終了性・数値オーバーフロー・配列境界・並行性・機能仕様との一致(functional correctness)まで。
3. ランタイム/ホストの認証 — コンパイラが完璧でも、実行系(WASM ランタイム等)が未認証なら全体は通らない。
4. プロセスとツール認定 — tool qualification、要件トレーサビリティ、独立検証。これは技術というより認証の世界(重い形式プロセス)。

Almide の資産(本物)

• Perceus の RC を Lean 4 で 23 定理 + proptest 検証済み — メモリ安全性に機械証明がある。業界でも稀。
• スタック効果の構築時検証(verify_func_stack)。
• LayoutRegistry による単一真実源(メモリレイアウトの一貫性)。
• 抽象オペの正直な拒否 — 未対応を panic でなく BuildError で返す(フォールバック設計とも一貫)。

これらは「完全性を志向する設計」としては正しい土台。

認証基準とのギャップ

ギャップ 1 は 差分ゲートの思想(出力照合で正しさを担保)を証明レベルに引き上げる延長線上にある。

結論: 2つのゴールを分ける

見立て(2026-05 時点の評価)。前者は今の延長で十分到達可能、後者は今の延長だけでは届かない。混同しないことが現実的なロードマップの鍵。

関連

• accepted-safety-in-systems — 3基準を横断して読んだ「業界が許容する安全性」の8原則(本ノートの上位概念)
• safety-critical-certification-bodies — 標準化団体・第三者評価機関・規制当局の3層分業(誰が認証するのか)
• perceus — Lean 4 で機械証明された RC。Almide の保証の核
• theorem-proving — 機械証明。DO-333 で認証エビデンスにできる
• formal-methods — 検証範囲を終了性・並行性等へ広げる手立ての出自
• almide — 言語本体。Pipeline Verification Chain がギャップ1を閉じる土台
• almide-differential-gate — 出力照合による正しさ担保。証明連鎖へ引き上げる起点
• rust-safety-critical — Rust の認定路(Ferrocene)との対比。Almide コンパイラ自体が Rust 製