エビデンスファースト文書
ドキュメントはシステムについての物語ではありません。それは主張台帳です。表明された実質的な記述はすべて、メカニズムとエビデンスにトレース可能であり、その限界は主張と同じ場所に記載されなければなりません。
自信に満ちた文章は安価です。目的は、読者が何が証明され、何がテストされ、何がレビューのみで、何が未解決かを判断できるようにすることです。
基本ルール
すべての実質的な主張には、次の4つの要素が必須です。
- メカニズム — その主張を真にするためにシステム内で機能しているもの。
- エビデンス — 証明成果物: 証明、モデル、テスト、分析レポート、トレース、ベンチマーク、またはレビュー記録。
- スコープ — 主張が適用される範囲と、信頼境界外にあるもの。
- ステータス — エビデンスが裏付ける、最も正直なラベル。
4つのうち1つでも欠けている場合、その主張は準備ができていません。設計意図、計画、または未解決の質問として書き直し、結果として偽装してはいけません。
主張台帳
ドキュメント内、またはリンクされたエビデンスファイルにテーブルを維持します。
| ID | 主張 | メカニズム | エビデンス | スコープ / TCB | ステータス | 制限 | 最終検証日 |
|---|---|---|---|---|---|---|---|
| C-01 | ロールXのみがテーブルTに書き込み可能 | 権限チェック + DBポリシー | 否定テスト T-04..T-11 | PostgreSQL 14–17; ロールY, ロールなしセッション | tested | スーパーユーザーとDBAは脅威モデル外 | 2026-11-02 |
ルール:
- 1行は1つの主張に対してであり、1文書に1行ではない。
- 主張は反証可能でなければならない。「システムは安全です」は主張ではない。「ロールYは、いずれのサポートされるエントリポイントからもテーブルTに書き込めない」は主張である。
- ツール名だけでなく、成果物にリンクすること。「SARIF」はフォーマット名であり、レポートパスとレビューしたルールセットがエビデンスである。
- 成果物が再実行されたら
最終検証日を更新すること。陳腐化したエビデンスは発見事項であり、形式的なものではない。 - 否定的な結果も保持すること。「Xの理由で破れなかった」もエビデンスであり、隠蔽すると誤った安心感を生む。
ステータスラダー
エビデンスが裏付ける最も強いラベルを使用し、それより強いラベルは決して使用してはいけません。
| ステータス | 意味 |
|---|---|
proven | 表明された特性の機械検証による証明。前提条件とTCBが宣言されていること。 |
model-checked | モデルの網羅的または制限付き探索。境界とモデル-コード間ギャップを明記すること。 |
tested | 違反を試みるテストが実行され、環境と結果が記録されていること。 |
static-refinement | 静的解析またはリファインメントチェック。ツール、ルール、未解決の発見事項を明記すること。 |
reviewed | 人間によるレビューのみ。実行可能または形式上のエビデンスはなし。 |
open | 主張は存在するがエビデンスなし。結果ではなくリスクである。 |
低いステータスは失敗ではありません。過大評価されたステータスこそが失敗です。
verified、proven、correct、secure、safe、complete、guaranteed、certified、compliant という単語を、隣接するステータスとスコープなしに使用してはいけません。もし単語がエビデンスなしで成立するなら、その単語は削除すべきです。
エビデンスの強度
正しい理由で失敗できるエビデンスを優先します。
- 明示的な前提条件のもとでの、表明された特性の形式的証明。
- 表明された境界内での網羅的モデルチェック。
- 記録されたコーパスとオラクルを用いたプロパティベーステストまたはファズテスト。
- メカニズムが除去されたときに失敗する、ターゲットを絞った否定テスト。
- レビュー済みルールセットとトリアージ済みの発見事項を伴う静的解析。
- 名前付きレビュアーとチェックリストを伴うコードレビュー。
- アサーションまたは逸話。
この階層は絶対ではありません。ターゲットを絞ったテストは、誤った適用をされた証明よりも強力になりえます。エビデンスを主張に合わせてください。コードをリファインしないモデルの証明は、コードを証明しません。プラットフォームが先に拒否したためにテストがパスしても、あなたのガードを証明するものではありません。
スコープと信頼境界
遠くの付録ではなく、主張の隣に境界を記載します。
- 対象となるバージョンとプラットフォーム。
- 除外される特権アクター: スーパーユーザー、DBA、デプロイ管理者、秘密鍵管理者、ビルドシステム、オペレーター。
- 前提条件: 暗号プリミティブ、クロック、ネットワーク、ストレージ、テナント分離、設定。
- 何が記号的にモデル化され、何が実際に実行されるか。
- 何がスコープ外で、その理由。
修飾されていない主張は、すべてについての主張であり、それはほぼ常に誤りです。「文書化された設定でPostgreSQL 14–17上でロールYに対して安全; DBAはモデル外」は、正直で有用です。
ワークフロー
- 主張を棚卸しする。 テキストを読み、特性、結果、保証、コンプライアンスステータスを主張するすべての文をマークします。
- 各主張を分類する。 設計意図、要件、実装事実、テスト結果、形式的結果、リリース主張のいずれか。
- IDとステータスを割り当てる。 メカニズム、エビデンス、スコープ、制限、
最終検証日を追加します。 - 主張を成果物に対してテストする。 レポートを開き、コマンドを再実行し、不足している成果物を要求します。ファイル名をエビデンスとして受け入れてはいけません。
- 未サポートの主張を書き直す。 「設計意図」、「計画済み」、「未検証」、または未解決の質問に変換します。野心は維持し、誤った確信は取り除きます。
- 否定的事実を確認する。 セキュリティや正確性に関する主張ごとに、それを違反しようとしたテストや分析を明記します。存在しない場合、その主張は
openとマークします。 - 言語をレビューする。 禁止ワード、曖昧な定量表現、修飾されていない絶対表現を削除します。
references/banned-words.mdを参照。 - エビデンスを固定する。 コマンド、コミット、環境、日付、成果物パスを記録し、レビュアーが結果を再現できるようにします。
- リリースをゲートする。 リリースノートは台帳がサポートする主張のみを主張できます。残余リスクと未解決の主張を明示的にリストします。
レビューチェックリスト
- 実質的な主張ごとに、ID、メカニズム、エビデンス、スコープ、ステータス、制限がある。
testedとされた主張は、メカニズムが除去されたときに失敗するテストを明示している。model-checkedとされた主張は、境界とモデル-コード間ギャップを明記している。provenとされた主張は、前提条件とTCBを明記している。- 否定的な結果と既知の失敗が存在し、除外されていない。
- 日付とバージョンが最新であり、陳腐化したエビデンスは陳腐化とマークされている。
- 特権アクターとスコープ外のパスが明記されている。
- 禁止ワードは、隣接するエビデンスとスコープなしには出現しない。
- README、アーキテクチャ文書、API契約書、リリースノートが互いに矛盾していない。
- 読者は文書のみからエビデンスを再現できる。
アンチパターン
- 希望的現在形。 計画であるのに「システムは…を強制する」と書く。
- ファイル名によるエビデンス。 結果、スコープ、日付なしで「report.pdfを参照」と書く。
- ツール名を証明として使う。 ルール、発見事項、トリアージなしで「静的解析で検証済み」と書く。
- スコープのすり替え。 狭いテスト結果を製品全体の保証として提示する。
- 全テスト合格の絶対表現。 どのテストか、どのプラットフォームか、何を違反しようとしたのかを言わずに「すべてのテストが合格」と書く。
- コンプライアンスのごっこ遊び。 標準名を証明書として使う。マッピングは監査ではない。
- 埋め込まれた制限。 注意書きは存在するが、主張から遠く離れている。
- 陳腐化した確信。 古いコミットの結果を最新として提示する。
- 否定的なエビデンスがない。 成功のみが文書化され、失敗や拒否は消える。
出力形式
技術文書の作成やレビューを求められた場合、以下を生成します。
- ステータスごとの件数を含む短い 主張サマリー。
- 主張台帳（インラインまたはリンク）。
- 未解決の主張と残余リスク、結果から明示的に分離。
- スコープと前提条件、それらが制約する主張の隣に。
- エビデンスインデックス、パス、コマンド、日付、バージョンを含む。
台帳とリリースノートの形式には references/evidence-template.md を使用します。公開前には references/banned-words.md を使用します。リポジトリに標準クロスウォークが含まれている場合は references/standards-map.md に配置します。スキル自体は特定の標準に依存しません。
出力は文書に合わせてスケールします。短いリリースノートには、完全な監査パックではなく、コンパクトな主張テーブルと短い残余リスクセクションで十分です。認証エビデンスファイルには、完全な台帳、エビデンスインデックス、スコープが必要です。網羅性と長さを混同しないでください。各行は読者が必要とする情報を伝えなければなりません。