Part IV—形式的検証と定量分析

形式的手段の適用

• 自然言語要件→形式仕様(TLA+/Alloy 等) を生成

• 生成コードが仕様を満たすかを シンボリック実行/モデル検査/証明支援 で検証

有効性メトリクス(虚栄を避ける)

カテゴリ	メトリクス	目的
品質	レビュー後欠陥率	もっとも重要なアウトカム
品質	重大問題の検出率	セキュリティ/性能の深刻度を把握
品質	コードチャーン	短期修正率で要件/レビュー品質を診断
ベロシティ	レビューサイクルタイム	ボトルネックの可視化
ベロシティ	最初のレビューまでの時間	応答性
プロセス	偽陰性/偽陽性率, オーバーライド率	AI適合度の学習指標

ダッシュボード出力は CI で収集 → reference/ にスキーマ化して公開すると再現性が増します。