スマートコントラクトなどの高保証が求められるソフトウェアにおいて、数学的な手法を用いてプログラムの仕様と実装が一致していることを厳密に証明する技術はどれか。

形式検証は、コードの正当性を数学的に証明する手法であり、ブロックチェーンのスマートコントラクトや航空宇宙など、バグが許されない分野で用いられる。