あとがき

『形式的手法の基礎と応用』を最後まで読んでいただき、ありがとうございました。

本書の狙い

本書は、仕様記述・模型検査・定理証明といった形式的手法を「実務のガードレール」として運用するために、基礎概念から導入戦略までを整理しました。安全性やセキュリティの要求が高まる一方、システムの複雑性は増し続けています。そうした状況で「なぜ正しいと言えるのか」を説明できる状態をつくることが、本書の到達目標です。

AI支援時代の位置づけ

AIによる生成や改修が高速化するほど、最終判断は検証器に寄せる必要があります。本書で示した「仕様→検証→実装」の流れは、AIが提案した内容であっても同じ基準で評価できる運用を目指しています。人が理解できる仕様と、機械が判定できる検証の両輪が揃ってはじめて、再現性ある品質保証が成立します。

AI支援執筆と検証方針

本書の改訂では、AI（LLM）を下書き・校正・整理の補助として利用する場合があります。ただし、AIの出力は「未信頼入力」であり、次の方針で取り扱います。

一次情報優先：仕様・ツール仕様・事例は、公式ドキュメント/公式リポジトリ/論文等の一次・準一次情報に寄せる（付録Eを索引として使用する）。
再現性の確保：付録Bの手順（devcontainer/CI）で、最小限のモデルチェックや検証が再現できることを優先する。
レビュー可能性：AIが生成した説明や手順は、前提・境界・例示（仮）を明記し、読者/チームがレビューできる形に整形する。

段階的な導入

形式的手法は、最初から全面適用する必要はありません。リスクの高い部分から小さく始め、スコープと深さを調整しながら適用範囲を広げることが現実的です。本書の手順やテンプレートを、現場の状況に合わせて小さく試し、効果が確認できたところから拡張してください。

継続的な改善

形式的手法は完成形ではなく、運用の中で磨かれていくものです。読者の皆様からのフィードバックや実践例は、今後の改訂に反映していきます。疑問点や改善提案はGitHubのIssue等で共有いただけると助かります。