形式検証とは

通常のテストは、入力をいくつか用意して結果を確かめます。この方法では、試していない入力で起きる問題は見つかりません。形式検証は発想が違い、「この関数を実行しても総供給量は変化しない」といった性質を仕様として書き、それが成り立たない入力が存在しないことを示します。

スマートコントラクトは、公開後の修正が難しく、扱う金額が大きく、コードが比較的短いという特徴があります。この条件は形式検証と相性がよく、トークンの会計処理、担保と負債の関係、権限の遷移といった中核部分に適用されることが増えています。持分証明の設計や合意形成の証明にも使われます。

限界も明確です。証明されるのは記述した性質だけなので、そもそも仕様として書かれていない前提が崩れる場合は検出できません。また、外部のプロトコルと組み合わせたときの挙動や、運営者の権限行使そのものは、検証の対象外に置かれることが一般的です。

利用者にとっての意味は、「形式検証済み」という言葉を無条件の安全と読まないことです。どの部分について、どんな性質が証明されたのかが公開されているかを見ます。検証範囲が明記され、監査と報奨金制度と併用されている状態が、現実的に最も検証の厚い形になります。