背景 航空宇宙、自動運転、OS カーネルなどの安全性が極めて重要なシステムでは、従来のテストによる網羅は不可能です。形式的検証は、数学的証明を用いてシステムが仕様を満たすことを論理的に保証します。 核心理論 1. …