このウェブサイトは機械検証されています
このサイトは定理証明器 Lean 4 で構築されています。ページ構成、各テキストフィールドに日本語と英語の値が存在すること、出力パスの一意性は型と定理で保証されます。監査プロファイル（--audit）では、内部リンクの参照先、アセット、CSP を検査します。検査に失敗すると、出力ディレクトリは更新されず、失敗したビルドは隔離されます。型や定理による保証 25 件のうち 25 件は、それを保証する Lean の型・定義・定理の名前を示しており、その名前が削除・改名されるとビルドが失敗します。
13コンテンツのスラッグ
26コンテンツのルート（スラッグ × 言語）
4レポートのルート
25このサイトに関する保証（型・定理）
24合格したビルド時の検査
プロファイル「full-audit」: 要求されたすべての検査が実行されました。
主な保証（根拠となる Lean の宣言名付き）
- i18n completeness —
NoGoals.Bridge.i18nComplete - No file collisions in build plan —
NoGoals.Bridge.plan_unique_paths - Canonical, hreflang and sitemap from one route set —
NoGoals.Meta.hreflang_symmetric - XML injection impossible (sitemap/feeds) —
NoGoals.Meta.xmlEscape_no_specials - Chrome structure well-formed (slots trusted) —
NoGoals.Render.Tree.render_wf_mod - Structural invariants proven for this build —
NoGoals.refine - No duplicate page paths —
NoGoals.Bridge.uniquePages
ビルドコマンドとソースの識別情報
./scripts/build.sh --audit
- consumer.commit: 7d08bbc814627b7f70003a97434c656f24336700
- consumer.dirty: false
- nogoals.commit: 05d4a231e03e74f7062f4fd3f8f8d60081166344
- nogoals.dirty: false
概要レポートと詳細レポートは、ほかのページと同じパス関数を使う予約済みルートに配置されます。内容はゲート実行後の検証結果であるため、サイトのページ集合に関する証明の対象外です。ビルド時には、出力パスがほかのファイルと衝突しないようにし、監査プロファイルでは最終検査でほかのページと同じゲートを実行します。
生成日時: 2026-10-08 05:22:24