形式検証

形式検証(Formal Verification)とは、プログラムの設計・検証工程において正しさを数学的に解析・証明することで、そのセキュリティを向上させる手法です。

Tezosコアデベロッパーは、純粋な関数型プログラミング言語「Michelson」を開発しました。この言語は主にTezosでのスマートコントラクトに用いられますが、その構造から、形式検証ツールの適用を容易にします。

Michelson
メリット

解析速度向上

コスト削減

不具合の回避

形式検証ツールは、スマートコントラクトによる契約の締結など、重要な局面での不具合を低減し、その機能を支えます。その後の不具合やクレーム対応などで発生するコストも低減するでしょう。