形式検証への反論、50年後の再検証

The Case Against Formal Verification, 50 Years Later

AIコーディングの台頭により形式検証への関心が高まる中、1979年の古典的論文「Social Processes and Proofs of Theorems and Programs」の主張を現代の視点から再検証する。著者は形式検証の限界を指摘するが、その後の技術発展により多くの論点が覆されている。本稿では、仕様の曖昧さ、自動検証の可能性、現実システムへの適用性など、6つの論点を最新の動向と照らし合わせて考察する。形式検証は万能ではないが、AIエージェントがコードを書く時代において、その重要性は増している。