「仕様書は存在しない」——形式手法の限界と可能性

Specifications Don't Exist (2025)

形式手法の成功例は、コンパイラや暗号ライブラリ、マイクロカーネルなど、自然に形式化できるシステムに限られています。しかし、WebブラウザやPDFのような複雑なシステムには、正確で一貫性のある形式的仕様を書くことはほぼ不可能です。本記事では、Galoisの経験から、仕様書が存在しない理由と、形式手法の適用範囲について考察します。