---
title: "スマート・コントラクトの形式的検証"
description: "イーサリアムのスマート・コントラクトにおける形式的検証の概要"
lang: ja
---

[スマート・コントラクト](/developers/docs/smart-contracts/)により、分散型でトラストレスかつ堅牢なアプリケーションの作成が可能になり、新しいユースケースが導入され、ユーザーに価値をもたらしています。スマート・コントラクトは大量の価値を扱うため、開発者にとってセキュリティは極めて重要な考慮事項です。

形式的検証は、[スマート・コントラクトのセキュリティ](/developers/docs/smart-contracts/security/)を向上させるために推奨される手法の1つです。プログラムの仕様策定、設計、検証に[形式手法](https://www.brookings.edu/techstream/formal-methods-as-a-path-toward-better-cybersecurity/)を用いる形式的検証は、重要なハードウェアおよびソフトウェアシステムの正確性を保証するために長年使用されてきました。

スマート・コントラクトに実装された場合、形式的検証はコントラクトのビジネスロジックが事前に定義された仕様を満たしていることを証明できます。テストなど、コントラクトコードの正確性を評価する他の手法と比較して、形式的検証はスマート・コントラクトが機能的に正しいことをより強力に保証します。

## 形式的検証とは？ {#what-is-formal-verification}

形式的検証とは、形式仕様に照らしてシステムの正確性を評価するプロセスを指します。簡単に言えば、形式的検証により、システムの動作が特定の要件を満たしているか（つまり、意図した通りに動作するか）を確認できます。

システム（この場合はスマート・コントラクト）の期待される動作は形式モデリングを使用して記述され、仕様記述言語によって形式的プロパティの作成が可能になります。その後、形式的検証手法により、コントラクトの実装がその仕様に準拠していることを検証し、実装の正確性の数学的証明を導き出すことができます。コントラクトが仕様を満たしている場合、それは「機能的に正しい（functionally correct）」、「設計上正しい（correct by design）」、または「構築上正しい（correct by construction）」と表現されます。

### 形式モデルとは？ {#what-is-a-formal-model}

コンピューターサイエンスにおいて、[形式モデル](https://en.wikipedia.org/wiki/Model_of_computation)とは計算プロセスの数学的記述です。プログラムは数学的関数（方程式）に抽象化され、モデルは入力が与えられたときに関数の出力がどのように計算されるかを記述します。

形式モデルは、プログラムの動作の分析を評価できる抽象化レベルを提供します。形式モデルの存在により、対象となるモデルの望ましいプロパティを記述する「形式仕様（formal specification）」の作成が可能になります。

形式的検証のためにスマート・コントラクトをモデリングするには、さまざまな手法が使用されます。たとえば、一部のモデルはスマート・コントラクトの高レベルな動作を推論するために使用されます。これらのモデリング手法は、スマート・コントラクトにブラックボックスの視点を適用し、入力を受け取り、その入力に基づいて計算を実行するシステムとして捉えます。

高レベルモデルは、スマート・コントラクトと外部エージェント（外部所有アカウント（EOA）、コントラクトアカウント、ブロックチェーン環境など）との関係に焦点を当てています。このようなモデルは、特定のユーザーインタラクションに対してコントラクトがどのように動作すべきかを指定するプロパティを定義するのに役立ちます。

逆に、スマート・コントラクトの低レベルな動作に焦点を当てた形式モデルもあります。高レベルモデルはコントラクトの機能についての推論に役立ちますが、実装の内部動作に関する詳細を捉えきれない場合があります。低レベルモデルはプログラム分析にホワイトボックスの視点を適用し、プログラムトレースや[制御フローグラフ](https://en.wikipedia.org/wiki/Control-flow_graph)など、スマート・コントラクトアプリケーションのより低レベルな表現に依存して、コントラクトの実行に関連するプロパティを推論します。

低レベルモデルは、イーサリアムの実行環境（つまり[EVM](/developers/docs/evm/)）におけるスマート・コントラクトの実際の実行を表現するため、理想的であると考えられています。低レベルのモデリング手法は、スマート・コントラクトにおける重要な安全性プロパティを確立し、潜在的な脆弱性を検出するのに特に役立ちます。

### 形式仕様とは？ {#what-is-a-formal-specification}

仕様とは、特定のシステムが満たさなければならない技術的要件のことです。プログラミングにおいて、仕様はプログラムの実行に関する一般的なアイデア（つまり、プログラムが何をすべきか）を表します。

スマート・コントラクトのコンテキストにおいて、形式仕様とは「プロパティ（properties）」、つまりコントラクトが満たすべき要件の形式的な記述を指します。このようなプロパティは「不変条件（invariants）」として記述され、例外なくあらゆる可能な状況下で真であり続けなければならない、コントラクトの実行に関する論理的アサートを表します。

したがって、形式仕様は、スマート・コントラクトの意図された実行を記述する、形式言語で書かれたステートメントの集合と考えることができます。仕様はコントラクトのプロパティを網羅し、さまざまな状況下でコントラクトがどのように動作すべきかを定義します。形式的検証の目的は、スマート・コントラクトがこれらのプロパティ（不変条件）を備えているか、そして実行中にこれらのプロパティが違反されないかを判断することです。

形式仕様は、スマート・コントラクトの安全な実装を開発する上で極めて重要です。不変条件の実装に失敗したり、実行中にプロパティが違反されたりするコントラクトは、機能を損なったり悪意のあるエクスプロイトを引き起こしたりする脆弱性を抱えやすくなります。

## スマート・コントラクトの形式仕様の種類 {#formal-specifications-for-smart-contracts}

形式仕様により、プログラム実行の正確性に関する数学的推論が可能になります。形式モデルと同様に、形式仕様は高レベルのプロパティ、またはコントラクト実装の低レベルな動作のいずれかを捉えることができます。

形式仕様は、プログラムのプロパティに関する形式的推論を可能にする[プログラム論理](https://en.wikipedia.org/wiki/Logic_programming)の要素を使用して導き出されます。プログラム論理には、プログラムの期待される動作を（数学的言語で）表現する形式的なルールがあります。形式仕様の作成には、[到達可能性論理](https://en.wikipedia.org/wiki/Reachability_problem)、[時相論理](https://en.wikipedia.org/wiki/Temporal_logic)、[ホーア論理](https://en.wikipedia.org/wiki/Hoare_logic)など、さまざまなプログラム論理が使用されます。

スマート・コントラクトの形式仕様は、大きく分けて**高レベル**仕様と**低レベル**仕様に分類できます。仕様がどのカテゴリに属するかに関わらず、分析対象のシステムのプロパティを適切かつ明確に記述する必要があります。

### 高レベル仕様 {#high-level-specifications}

その名の通り、高レベル仕様（「モデル指向仕様」とも呼ばれます）はプログラムの高レベルな動作を記述します。高レベル仕様は、スマート・コントラクトを[有限状態機械](https://en.wikipedia.org/wiki/Finite-state_machine)（FSM）としてモデル化します。FSMは操作を実行することで状態間を遷移でき、FSMモデルの形式的プロパティを定義するために時相論理が使用されます。

[時相論理](https://en.wikipedia.org/wiki/Temporal_logic)とは、「時間に関して修飾された命題（例：「私は_常に_お腹が空いている」や「私は_最終的に_お腹が空く」など）を推論するためのルール」です。形式的検証に適用される場合、時相論理は状態機械としてモデル化されたシステムの正しい動作に関するアサートを述べるために使用されます。具体的には、時相論理はスマート・コントラクトが将来なり得る状態と、状態間をどのように遷移するかを記述します。

高レベル仕様は一般に、スマート・コントラクトの2つの重要な時相プロパティ、すなわち**安全性（safety）**と**活性（liveness）**を捉えます。安全性プロパティは「悪いことは決して起こらない」という考えを表し、通常は不変性を表現します。安全性プロパティは、[デッドロック](https://www.techtarget.com/whatis/definition/deadlock)がないことなどの一般的なソフトウェア要件を定義したり、コントラクトのドメイン固有のプロパティ（例：関数のアクセス制御に関する不変条件、状態変数の許容値、トークン送金の条件など）を表現したりします。

たとえば、ERC-20トークンコントラクトで`transfer()`または`transferFrom()`を使用するための条件をカバーする次の安全性要件を考えてみましょう。「_送信者の残高が、送信を要求されたトークンの量を下回ることは決してない。_」このコントラクトの不変条件の自然言語による記述は、形式的（数学的）仕様に変換でき、その後、その妥当性を厳密にチェックできます。

活性プロパティは「最終的に良いことが起こる」とアサートし、コントラクトがさまざまな状態を経て進行する能力に関係します。活性プロパティの例としては「流動性」があり、これは要求に応じてコントラクトがその残高をユーザーに送金する能力を指します。このプロパティが違反された場合、[Parityウォレットのインシデント](https://www.cnbc.com/2017/11/08/accidental-bug-may-have-frozen-280-worth-of-ether-on-parity-wallet.html)で起こったように、ユーザーはコントラクトに保存されている資産を引き出すことができなくなります。

### 低レベル仕様 {#low-level-specifications}

高レベル仕様は、コントラクトの有限状態モデルを出発点とし、このモデルの望ましいプロパティを定義します。対照的に、低レベル仕様（「プロパティ指向仕様」とも呼ばれます）は、プログラム（スマート・コントラクト）を数学的関数の集合からなるシステムとしてモデル化し、そのようなシステムの正しい動作を記述することがよくあります。

簡単に言えば、低レベル仕様は「プログラムトレース」を分析し、これらのトレース上でスマート・コントラクトのプロパティを定義しようと試みます。トレースとは、スマート・コントラクトの状態を変更する関数実行のシーケンスを指します。したがって、低レベル仕様はコントラクトの内部実行に関する要件を指定するのに役立ちます。

低レベルの形式仕様は、ホーアスタイルのプロパティ、または実行パス上の不変条件のいずれかとして与えることができます。

### ホーアスタイルのプロパティ {#hoare-style-properties}

[ホーア論理](https://en.wikipedia.org/wiki/Hoare_logic)は、スマート・コントラクトを含むプログラムの正確性を推論するための一連の形式的ルールを提供します。ホーアスタイルのプロパティはホーアの三つ組`{P}c{Q}`で表されます。ここで、`c`はプログラムであり、`P`と`Q`は`c`（つまりプログラム）の状態に関する述語で、それぞれ「事前条件（preconditions）」および「事後条件（postconditions）」として形式的に記述されます。

事前条件は、関数の正しい実行に必要な条件を記述する述語です。コントラクトを呼び出すユーザーはこの要件を満たす必要があります。事後条件は、関数が正しく実行された場合に確立される条件を記述する述語です。ユーザーは関数を呼び出した後、この条件が真になることを期待できます。ホーア論理における「不変条件」は、関数の実行によって保持される（つまり変化しない）述語です。

ホーアスタイルの仕様は、「部分正当性（partial correctness）」または「完全正当性（total correctness）」のいずれかを保証できます。コントラクト関数の実装は、関数の実行前に事前条件が真であり、実行が終了した場合に事後条件も真であれば「部分的に正しい」とされます。完全正当性の証明は、関数の実行前に事前条件が真であり、実行が必ず終了し、終了したときに事後条件が真である場合に得られます。

一部の実行は終了するまでに遅延したり、まったく終了しなかったりする可能性があるため、完全正当性の証明を得ることは困難です。とはいえ、イーサリアムのガスメカニズムは無限のプログラムループを防ぐため（実行は正常に終了するか、「ガス不足（out-of-gas）」エラーにより終了するかのいずれかです）、実行が終了するかどうかという問題は事実上無意味であると言えます。

ホーア論理を使用して作成されたスマート・コントラクトの仕様には、コントラクト内の関数やループの実行に対して定義された事前条件、事後条件、および不変条件が含まれます。事前条件には関数への誤った入力の可能性が含まれることが多く、事後条件はそのような入力に対する期待される応答（特定の例外をスローするなど）を記述します。このように、ホーアスタイルのプロパティはコントラクト実装の正確性を保証するのに効果的です。

多くの形式的検証フレームワークは、関数の意味論的な正確性を証明するためにホーアスタイルの仕様を使用します。また、Solidityの`require`ステートメントと`assert`ステートメントを使用して、ホーアスタイルのプロパティを（アサートとして）コントラクトコードに直接追加することも可能です。

`require`ステートメントは事前条件または不変条件を表現し、ユーザー入力の検証によく使用されます。一方、`assert`は安全性に必要な事後条件を捉えます。たとえば、関数の適切なアクセス制御（安全性プロパティの一例）は、呼び出し元アカウントのIDに対する事前条件チェックとして`require`を使用することで実現できます。同様に、コントラクト内の状態変数の許容値（流通しているトークンの総数など）に関する不変条件は、関数実行後にコントラクトの状態を確認するために`assert`を使用することで、違反から保護できます。

### トレースレベルのプロパティ {#trace-level-properties}

トレースベースの仕様は、コントラクトを異なる状態間で遷移させる操作と、これらの操作間の関係を記述します。前述のように、トレースとは特定の方法でコントラクトの状態を変更する操作のシーケンスです。

このアプローチは、スマート・コントラクトを、いくつかの事前定義された状態（状態変数によって記述される）と、事前定義された遷移のセット（コントラクト関数によって記述される）を持つ状態遷移システムとしてモデル化することに依存しています。さらに、プログラムの実行フローをグラフィカルに表現した[制御フローグラフ](https://www.geeksforgeeks.org/software-engineering-control-flow-graph-cfg/)（CFG）が、コントラクトの操作的意味論を記述するためによく使用されます。ここでは、各トレースは制御フローグラフ上のパスとして表されます。

主に、トレースレベルの仕様はスマート・コントラクトの内部実行パターンを推論するために使用されます。トレースレベルの仕様を作成することで、スマート・コントラクトの許容される実行パス（つまり状態遷移）をアサートします。シンボリック実行などの手法を使用することで、実行が形式モデルで定義されていないパスをたどらないことを形式的に検証できます。

トレースレベルのプロパティを説明するために、パブリックにアクセス可能な関数をいくつか持つ[DAO](/dao/)コントラクトの例を使用しましょう。ここでは、DAOコントラクトがユーザーに以下の操作を許可していると仮定します。

- 資金の預け入れ

- 資金を預け入れた後、提案に投票する

- 提案に投票しない場合、返金を請求する

トレースレベルのプロパティの例としては、「_資金を預け入れていないユーザーは提案に投票できない_」や「_提案に投票しないユーザーは常に返金を請求できるべきである_」などが考えられます。どちらのプロパティも、望ましい実行シーケンスをアサートしています（資金を預け入れる_前_に投票することはできず、提案に投票した_後_に返金を請求することはできません）。

## スマート・コントラクトの形式的検証手法 {#formal-verification-techniques}

### モデル検査 {#model-checking}

モデル検査は、アルゴリズムがスマート・コントラクトの形式モデルをその仕様と照らし合わせてチェックする形式的検証手法です。モデル検査において、スマート・コントラクトは状態遷移システムとして表現されることが多く、許容されるコントラクト状態に関するプロパティは時相論理を使用して定義されます。

モデル検査では、システム（つまりコントラクト）の抽象的な数学的表現を作成し、[命題論理](https://www.baeldung.com/cs/propositional-logic)に基づく数式を使用してこのシステムのプロパティを表現する必要があります。これにより、数学的モデルが与えられた論理式を満たすことを証明するという、モデル検査アルゴリズムのタスクが簡素化されます。

形式的検証におけるモデル検査は、主に時間の経過に伴うコントラクトの動作を記述する時相プロパティを評価するために使用されます。スマート・コントラクトの時相プロパティには、前述した「安全性」と「活性」が含まれます。

たとえば、アクセス制御に関連するセキュリティプロパティ（例：_コントラクトの所有者のみが`selfdestruct`を呼び出すことができる_）は、形式論理で記述できます。その後、モデル検査アルゴリズムは、コントラクトがこの形式仕様を満たしているかどうかを検証できます。

モデル検査は状態空間探索を使用します。これには、スマート・コントラクトのすべての可能な状態を構築し、プロパティ違反を引き起こす到達可能な状態を見つけようとするプロセスが含まれます。しかし、これは無限の数の状態につながる可能性があり（「状態爆発問題」として知られています）、そのためモデルチェッカーはスマート・コントラクトの効率的な分析を可能にするために抽象化手法に依存しています。

### 定理証明 {#theorem-proving}

定理証明は、スマート・コントラクトを含むプログラムの正確性について数学的に推論する手法です。これには、コントラクトのシステムのモデルとその仕様を数式（論理ステートメント）に変換することが含まれます。

定理証明の目的は、これらのステートメント間の論理的同値性を検証することです。「論理的同値性」（「論理的相互含意」とも呼ばれます）とは、2つのステートメント間の関係の一種であり、2番目のステートメントが真である_場合にのみ_、1番目のステートメントが真になるというものです。

コントラクトのモデルとそのプロパティに関するステートメント間の必要な関係（論理的同値性）は、証明可能なステートメント（定理と呼ばれます）として定式化されます。形式的な推論システムを使用することで、自動定理プルーバーは定理の妥当性を検証できます。言い換えれば、定理プルーバーは、スマート・コントラクトのモデルがその仕様と正確に一致することを決定的に証明できます。

モデル検査がコントラクトを有限状態の遷移システムとしてモデル化するのに対し、定理証明は無限状態システムの分析を処理できます。しかし、これは自動定理プルーバーが論理問題が「決定可能」であるかどうかを常に知ることができるわけではないことを意味します。

結果として、定理プルーバーが正確性の証明を導き出すのを導くために、人間の支援が必要になることがよくあります。定理証明に人間の労力を使用するため、完全に自動化されているモデル検査よりも使用コストが高くなります。

### シンボリック実行 {#symbolic-execution}

シンボリック実行は、「具体的な値」（例：`x == 5`）の代わりに「シンボリックな値」（例：`x > 5`）を使用して関数を実行することにより、スマート・コントラクトを分析する手法です。形式的検証手法として、シンボリック実行はコントラクトコード内のトレースレベルのプロパティについて形式的に推論するために使用されます。

シンボリック実行は、実行トレースをシンボリックな入力値に対する数式として表現します。これは「パス述語（path predicate）」とも呼ばれます。[SMTソルバー](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories)は、パス述語が「充足可能」であるか（つまり、数式を満たす値が存在するか）をチェックするために使用されます。脆弱なパスが充足可能である場合、SMTソルバーはそのパスに向けて実行を誘導する具体的な値を生成します。

スマート・コントラクトの関数が入力として`uint`値（`x`）を受け取り、`x`が`5`より大きく、かつ`10`より小さい場合にリバートするとします。通常のテスト手順を使用してエラーを引き起こす`x`の値を見つけるには、エラーを引き起こす入力を実際に見つけられるという保証なしに、数十（またはそれ以上）のテストケースを実行する必要があります。

逆に、シンボリック実行ツールはシンボリックな値`X > 5 ∧ X < 10`（つまり、`x`は5より大きく、かつ`x`は10より小さい）を使用して関数を実行します。関連するパス述語`x = X > 5 ∧ X < 10`は、解決のためにSMTソルバーに渡されます。特定の値が数式`x = X > 5 ∧ X < 10`を満たす場合、SMTソルバーはそれを計算します。たとえば、ソルバーは`x`の値として`7`を生成するかもしれません。

シンボリック実行はプログラムへの入力に依存しており、すべての到達可能な状態を探索するための入力のセットは潜在的に無限であるため、依然としてテストの一形態です。しかし、例に示されているように、シンボリック実行はプロパティ違反を引き起こす入力を見つける上で、通常のテストよりも効率的です。

さらに、シンボリック実行は、関数への入力をランダムに生成する他のプロパティベースの手法（ファジングなど）よりも誤検知が少なくなります。シンボリック実行中にエラー状態がトリガーされた場合、エラーを引き起こす具体的な値を生成し、問題を再現することが可能です。

シンボリック実行は、ある程度の数学的な正確性の証明を提供することもできます。オーバーフロー保護を備えたコントラクト関数の次の例を考えてみましょう。

```
function safe_add(uint x, uint y) returns(uint z){

  z = x + y;
  require(z>=x);
  require(z>=y);

  return z;
}
```

整数オーバーフローを引き起こす実行トレースは、次の数式を満たす必要があります。`z = x + y AND (z >= x) AND (z >= y) AND (z < x OR z < y)` このような数式が解かれる可能性は低いため、関数`safe_add`が絶対にオーバーフローしないという数学的証明として機能します。

### なぜスマート・コントラクトに形式的検証を使用するのか？ {#benefits-of-formal-verification}

#### 信頼性の必要性 {#need-for-reliability}

形式的検証は、その障害が死亡、負傷、または経済的破綻などの壊滅的な結果をもたらす可能性のある、安全性重視のシステムの正確性を評価するために使用されます。スマート・コントラクトは莫大な価値を制御する価値の高いアプリケーションであり、設計上の単純なエラーが[ユーザーにとって回復不能な損失](https://www.freecodecamp.org/news/a-hacker-stole-31m-of-ether-how-it-happened-and-what-it-means-for-ethereum-9e5dc29e33ce/amp/)につながる可能性があります。しかし、デプロイ前にコントラクトを形式的に検証することで、ブロックチェーン上で実行された際に期待通りに機能するという保証を高めることができます。

信頼性はあらゆるスマート・コントラクトにおいて非常に望まれる品質です。特に、[イーサリアム](/)仮想マシン（EVM）にデプロイされたコードは通常イミュータブルであるためです。ローンチ後のアップグレードが容易に利用できないため、コントラクトの信頼性を保証する必要性から形式的検証が不可欠になります。形式的検証は、監査人やテスターが見逃す可能性のある、整数のアンダーフローやオーバーフロー、リエントランシー、不十分なガス最適化などの厄介な問題を検出できます。

#### 機能的正確性の証明 {#prove-functional-correctness}

プログラムテストは、スマート・コントラクトが特定の要件を満たしていることを証明する最も一般的な方法です。これには、コントラクトが処理すると予想されるデータのサンプルを使用してコントラクトを実行し、その動作を分析することが含まれます。コントラクトがサンプルデータに対して期待される結果を返す場合、開発者はその正確性の客観的な証明を得たことになります。

しかし、このアプローチでは、サンプルに含まれない入力値に対する正しい実行を証明することはできません。したがって、コントラクトのテストはバグの検出（つまり、実行中に一部のコードパスが望ましい結果を返さない場合）には役立つかもしれませんが、**バグがないことを決定的に証明することはできません**。

逆に、形式的検証は、コントラクトをまったく実行する_ことなく_、無限の範囲の実行に対してスマート・コントラクトが要件を満たしていることを形式的に証明できます。これには、正しいコントラクトの動作を正確に記述する形式仕様を作成し、コントラクトのシステムの形式的（数学的）モデルを開発する必要があります。その後、形式的な証明手順に従って、コントラクトのモデルとその仕様の間の一貫性をチェックできます。

形式的検証を用いると、コントラクトのビジネスロジックが要件を満たしているかどうかを検証するという問題は、証明または反証可能な数学的命題になります。命題を形式的に証明することで、有限のステップ数で無限のテストケースを検証できます。このように、形式的検証は仕様に関してコントラクトが機能的に正しいことを証明する上で、より優れた見込みを持っています。

#### 理想的な検証対象 {#ideal-verification-targets}

検証対象とは、形式的に検証されるシステムを記述したものです。形式的検証は、「組み込みシステム」（より大きなシステムの一部を形成する、小さくシンプルなソフトウェア）で使用するのが最適です。また、ルールが少ない専門的なドメインにも理想的です。これにより、ドメイン固有のプロパティを検証するためのツールの変更が容易になるためです。

スマート・コントラクトは、少なくともある程度は両方の要件を満たしています。たとえば、イーサリアムのコントラクトはサイズが小さいため、形式的検証に適しています。同様に、EVMはシンプルなルールに従っているため、EVMで実行されるプログラムの意味論的プロパティの指定と検証が容易になります。

### 開発サイクルの高速化 {#faster-development-cycle}

モデル検査やシンボリック実行などの形式的検証手法は、一般に（テストや監査中に実行される）スマート・コントラクトコードの通常の分析よりも効率的です。これは、具体的な値を使用するテスト（「ユーザーが5イーサを引き出そうとしたらどうなるか？」）とは異なり、形式的検証がアサートをテストするためにシンボリックな値に依存しているためです（「ユーザーが_n_イーサを引き出そうとしたらどうなるか？」）。

シンボリックな入力変数は複数のクラスの具体的な値をカバーできるため、形式的検証アプローチはより短時間でより多くのコードカバレッジを約束します。効果的に使用すれば、形式的検証は開発者の開発サイクルを加速させることができます。

形式的検証はまた、コストのかかる設計エラーを減らすことで、分散型アプリケーション (dapp) の構築プロセスを改善します。脆弱性を修正するためにコントラクトをアップグレードする（可能な場合）には、コードベースの大規模な書き換えと、開発に費やすさらなる労力が必要になります。形式的検証は、テスターや監査人が見逃す可能性のあるコントラクト実装の多くのエラーを検出し、コントラクトをデプロイする前にそれらの問題を修正する十分な機会を提供します。

## 形式的検証の欠点 {#drawbacks-of-formal-verification}

### 手作業のコスト {#cost-of-manual-labor}

形式的検証、特に人間がプルーバーを導いて正確性の証明を導き出す半自動検証は、かなりの手作業を必要とします。さらに、形式仕様の作成は高度なスキルを要求される複雑な作業です。

これらの要因（労力とスキル）により、形式的検証は、テストや監査など、コントラクトの正確性を評価する通常の方法と比較して、より要求が厳しく高価になります。それにもかかわらず、スマート・コントラクト実装におけるエラーのコストを考慮すると、完全な検証監査のコストを支払うことは実用的です。

### 偽陰性（見逃し） {#false-negatives}

形式的検証は、スマート・コントラクトの実行が形式仕様と一致するかどうかのみをチェックできます。そのため、仕様がスマート・コントラクトの期待される動作を適切に記述していることを確認することが重要です。

仕様の記述が不十分な場合、脆弱な実行を示すプロパティの違反は、形式的検証監査では検出できません。この場合、開発者はコントラクトにバグがないと誤って思い込んでしまう可能性があります。

### パフォーマンスの問題 {#performance-issues}

形式的検証は、いくつかのパフォーマンスの問題に直面します。たとえば、モデル検査やシンボリック検査中にそれぞれ遭遇する状態爆発やパス爆発の問題は、検証手順に影響を与える可能性があります。また、形式的検証ツールは基盤となるレイヤーでSMTソルバーやその他の制約ソルバーを使用することが多く、これらのソルバーは計算集約的な手順に依存しています。

また、プログラムが終了しない可能性があるため、プログラム検証ツールがプロパティ（論理式として記述される）を満たすことができるかどうかを常に判断できるとは限りません（「[決定問題](https://en.wikipedia.org/wiki/Decision_problem)」）。そのため、コントラクトが適切に指定されていたとしても、一部のプロパティを証明することが不可能な場合があります。

## イーサリアムのスマート・コントラクト向け形式的検証ツール {#formal-verification-tools}

### 形式仕様を作成するための仕様記述言語 {#specification-languages}

**Act**: _*Actは、ストレージの更新、事前/事後条件、およびコントラクトの不変条件の指定を可能にします。そのツールスイートには、Coq、SMTソルバー、またはhevmを介して多くのプロパティを証明できる証明バックエンドも備わっています。*_

- [GitHub](https://github.com/ethereum/act)
- [ドキュメント](https://github.com/argotorg/act)

**Scribble** - _*Scribbleは、Scribble仕様記述言語のコードアノテーションを、仕様をチェックする具体的なアサートに変換します。*_

- [ドキュメント](https://docs.scribble.codes/)

**Dafny** - _*Dafnyは、コードの正確性を推論し証明するために高レベルのアノテーションに依存する、検証対応のプログラミング言語です。*_

- [GitHub](https://github.com/dafny-lang/dafny)

### 正確性をチェックするためのプログラム検証ツール {#program-verifiers}

**Certora Prover** - _Certora Proverは、スマート・コントラクトのコードの正確性をチェックするための自動形式的検証ツールです。仕様はCVL（Certora Verification Language）で記述され、静的解析と制約解決の組み合わせを使用してプロパティ違反が検出されます。_

- [ウェブサイト](https://www.certora.com/)
- [ドキュメント](https://docs.certora.com/en/latest/index.html)

**Solidity SMTChecker** - _*SolidityのSMTCheckerは、SMT（Satisfiability Modulo Theories）とホーン解決に基づく組み込みのモデルチェッカーです。コンパイル時にコントラクトのソースコードが仕様と一致するかどうかを確認し、安全性プロパティの違反を静的にチェックします。*_

- [GitHub](https://github.com/ethereum/solidity)

**solc-verify** - _*solc-verifyは、アノテーションとモジュール式プログラム検証を使用してSolidityコードの自動形式的検証を実行できる、Solidityコンパイラの拡張バージョンです。*_

- [GitHub](https://github.com/SRI-CSL/solidity)

**KEVM** - _*KEVMは、Kフレームワークで記述されたイーサリアム仮想マシン（EVM）の形式的意味論です。KEVMは実行可能であり、到達可能性論理を使用して特定のプロパティ関連のアサートを証明できます。*_

- [GitHub](https://github.com/runtimeverification/evm-semantics)
- [ドキュメント](https://jellopaper.org/)

### 定理証明のための論理フレームワーク {#theorem-provers}

**Isabelle** - _Isabelle/HOLは、数式を形式言語で表現できるようにし、それらの数式を証明するためのツールを提供する証明支援システムです。主な用途は数学的証明の形式化であり、特にコンピューターのハードウェアやソフトウェアの正確性の証明、コンピューター言語やプロトコルのプロパティの証明を含む形式的検証です。_

- [GitHub](https://github.com/isabelle-prover)
- [ドキュメント](https://isabelle.in.tum.de/documentation.html)

**Rocq** - _Rocqは、定理を使用してプログラムを定義し、機械的にチェックされた正確性の証明をインタラクティブに生成できる対話型定理プルーバーです。_

- [GitHub](https://github.com/rocq-prover/rocq)
- [ドキュメント](https://rocq-prover.org/docs)

### スマート・コントラクトの脆弱なパターンを検出するためのシンボリック実行ベースのツール {#symbolic-execution-tools}

**マンティコア** - _*シンボリック実行に基づくEVMバイトコード分析ツール*。_

- [GitHub](https://github.com/trailofbits/manticore)
- [ドキュメント](https://github.com/trailofbits/manticore/wiki)

**hevm** - _*hevmは、EVMバイトコード用のシンボリック実行エンジンおよび等価性チェッカーです。*_

- [GitHub](https://github.com/dapphub/dapptools/tree/master/src/hevm)

**Mythril** - _イーサリアムのスマート・コントラクトの脆弱性を検出するためのシンボリック実行ツール_

- [GitHub](https://github.com/ConsenSysDiligence/mythril)
- [ドキュメント](https://github.com/ConsenSysDiligence/mythril/tree/develop/docs/source)

## 参考文献 {#further-reading}

- [スマート・コントラクトの形式的検証の仕組み](https://runtimeverification.com/blog/how-formal-verification-of-smart-contracts-works/)
- [イーサリアムエコシステムにおける形式的検証プロジェクトの概要](https://github.com/leonardoalt/ethereum_formal_verification_overview)
- [イーサリアム2.0デポジットスマート・コントラクトのエンドツーエンドの形式的検証](https://runtimeverification.com/blog/end-to-end-formal-verification-of-ethereum-2-0-deposit-smart-contract/)
- [世界で最も人気のあるスマート・コントラクトの形式的検証](https://www.zellic.io/blog/formal-verification-weth)
- [SMTCheckerと形式的検証](https://docs.soliditylang.org/en/v0.8.15/smtchecker.html)