スマートコントラクトの形式的検証
最終更新： 2026年2月23日
スマートコントラクトは、分散型でトラストレス、かつ堅牢なアプリケーションの作成を可能にし、ユーザーに新しいユースケースを導入し、価値を解き放ちます。 スマートコントラクトが取り扱うものには巨額の価値があるため、デベロッパーにとってセキュリティは極めて重要です。
形式的検証は、スマートコントラクトのセキュリティを向上させるために推奨される手法の1つです。 プログラムの仕様記述、設計、検証に形式手法 (opens in a new tab)を用いる形式的検証は、クリティカルなハードウェアやソフトウェアシステムの正当性を保証するために、長年用いられてきました。
スマートコントラクトに形式的検証を実施することで、スマートコントラクトの挙動があらかじめ規定された仕様を満たすことが証明できます。 スマートコントラクトのコードの正しさを査定する他の手法(テスト技法など)と比べて、形式的検証はスマートコントラクトが機能的に正しいことをより強力に保証します。
形式的検証とは何か
形式的検証というのは、形式仕様記述に対してシステムの正しさを評価するための一連の作業のことです。 簡単に言うと、形式的検証によってシステムの挙動が求められている要件を満たしているかどうかを確かめることができます。
システム(この場合はスマートコントラクト)の期待される挙動は形式的な表現によって記述され、形式的プロパティは仕様記述言語で書かれます。 そして、形式的検証の技法により、スマートコントラクトの実装が仕様に準拠していることを検証でき、さらにその実装の正しさの数学的証明を導くことができます。 スマートコントラクトが仕様を満たすことを、「機能的に正しい」、「設計により正しい」または「構成により正しい」といいます。
形式モデルとは何か
コンピューターサイエンスでは、形式モデル (opens in a new tab)は、計算プロセスを数学的に記述したものです。 プログラムは数学的な関数(方程式)によって抽象化され、関数の入力に対して出力をどう計算するかが形式モデルによって記述されます。
形式モデルは、プログラムの挙動の分析を評価できる水準での抽象化を可能とします。 形式モデルがあることで_形式仕様_を作成でき、それによって、対象のモデルの持つべき望ましいプロパティが記述されます。
形式的検証のためのスマートコントラクトのモデル化には、さまざまな技法が用いられます。 たとえば、スマートコントラクトの高水準な挙動を論証するために用いられるモデルがあります。 そのようなモデル化技法では、スマートコントラクトを与えられた入力に基いて計算を実行するブラックボックスとみなします。
高水準なモデルでは、スマートコントラクトと外部エージェント(外部所有アカウント(EOA)、コントラクトアカウントもしくはブロックチェーン環境)との関係に重点が置かれます。 このようなモデルは、スマートコントラクトが特定のユーザーインタラクションにどう応じるべきかを記述するのに有用です。
逆に、スマートコントラクトの低水準な挙動に重点を置く形式モデルもあります。 高水準なモデルはスマートコントラクトの機能について論証するのに役立ちますが、その反面、実装の内部動作の詳細が上手く掴めないこともあります。 低レベルモデルはプログラム分析にホワイトボックスビューを適用し、プログラムトレースや制御フローグラフ (opens in a new tab)といったスマートコントラクトアプリケーションの低レベルな表現を利用して、コントラクトの実行に関連するプロパティを推論します。
低レベルモデルは、イーサリアムの実行環境(すなわちEVM)におけるスマートコントラクトの実際の実行を表すため、理想的であると考えられています。 低水準なモデリング技法は、スマートコントラクトの重要な安全性の確立と潜在的な脆弱性の検出に特に有用です。
形式仕様記述とは何か
仕様とは、特定のシステムが満たすべき技術的要件のことです。 プログラミングにおいては、仕様はプログラムの実行についてのおおまかな狙い(すなわち、プログラムが何をすべきか)を表します。
スマートコントラクトの文脈において、形式仕様とは、コントラクトが満たさなければならない要件を形式的に記述した_プロパティ_を指します。 プロパティはスマートコントラクトの実行を通しての「不変条件」として記述され、例外なしにあらゆる状況下で真であるべき論理アサーションを表現するものです。
したがって、形式仕様記述はスマートコントラクトのしかるべき挙動を形式言語で記述したものの集まりである、と考えることができます。 仕様が対象とするのはスマートコントラクトのプロパティで、スマートコントラクトがさまざまな状況下でどのように動作すべきかを表します。 スマートコントラクトがそれらのプロパティ(不変条件) を実行中に破らないことを見極めるのが、 形式的検証の目的です。
形式仕様記述は、スマートコントラクトのセキュアな実装をする上で極めて重要です。 求められた不変条件を満たさなかったり、実行中にプロパティを破るスマートコントラクトには、その機能を害したり悪用を許してしまう脆弱性があるおそれがあります。
スマートコントラクトの形式仕様の種類
形式的仕様記述により、プログラム実行の正しさを数学的に論証することが可能となります。 形式モデルと同様、形式仕様記述は高水準のプロパティもしくはスマートコントラクトの実装の低水準の挙動をとらえることができます。
形式仕様は、プログラム論理 (opens in a new tab)の要素を用いて導出され、プログラムのプロパティについて形式的に推論することを可能にします。 プログラム論理が備えている形式規則により、プログラムのしかるべき挙動が(数学的に)表現されます。 形式仕様の作成には、到達可能性論理 (opens in a new tab)、時相論理 (opens in a new tab)、ホーア論理 (opens in a new tab)など、さまざまなプログラム論理が使用されます。
スマートコントラクトの形式仕様は、高水準仕様と低水準仕様に大別できます。 いずれの場合でも、分析対象のシステムのプロパティを適切かつ一義的に記述できなければなりません。
高水準仕様
その名のとおり、高水準な仕様記述(「モデル指向仕様記述」とも呼ばれます) はプログラムの高水準な挙動を記述するためのものです。 高水準仕様では、スマートコントラクトを有限状態機械 (opens in a new tab)(FSM)としてモデル化します。FSMは操作を実行することで状態間を遷移し、そのFSMモデルの形式的プロパティの定義には時相論理が用いられます。
時相論理 (opens in a new tab)とは、「時間という観点から修飾された命題(例：「私は_いつも_空腹である」または「私は_いずれ_空腹になる」)について推論するためのルール」です。 形式的検証での時相論理は、状態遷移機械でモデル化されたシステムの正しい挙動に関するアサーションを記述するために使われます。 具体的には、スマートコントラクトがある将来の時点でモデルのどの状態にあるのか、そしてどのように状態間で遷移するのかを時相論理で記述できます。
高水準仕様は一般に、スマートコントラクトの2つの重要な時相プロパティ、すなわち安全性と活性を捉えます。 安全性とはすなわち「何も悪いことが起こらない」ということで、通常は不変条件によって表されます。 安全性プロパティは、デッドロック (opens in a new tab)フリーなどの一般的なソフトウェア要件を定義することもあれば、コントラクトのドメイン固有のプロパティ(例：関数のアクセス制御の不変量、状態変数の許容値、トークン送金の条件)を表現することもあります。
ERC-20トークンコントラクトでtransfer()またはtransferFrom()を使用する条件をカバーする、この安全性要件を例にとってみましょう：「送信者の残高は、送信要求されたトークンの量を下回ってはならない」。 この自然言語で書かれたスマートコントラクトの不変条件は数学的な形式仕様記述に翻訳され、その妥当性が厳密に検査されます。
活性は「何らかの良いことがいずれは起こる」ということを意味し、スマートコントラクトに関しては、するべき処理を滞りなく進められることを示します。 活性の一例として「流動性」が挙げられ、これは、要求に応じてスマートコントラクトが残高を他ユーザーに譲渡できることを意味します。 このプロパティに違反した場合、Parityウォレット事件 (opens in a new tab)で起こったように、ユーザーはコントラクトに保管されている資産を引き出すことができなくなります。
低水準仕様
高水準な仕様記述では、有限状態モデルから出発してモデルの望ましいプロパティを記述しました。 一方で、低水準な仕様記述(プロパティ指向仕様記述とも呼ばれます)では、プログラム(すなわちスマートコントラクト)を数学的な関数の集まりからなるシステムとしてモデル化し、そのシステムの正しい挙動を記述します。
簡単に言うと、低水準仕様ではプログラムの_トレース_を解析し、それに基づいてスマートコントラクトのプロパティを定義しようと試みます。 トレースとは、スマートコントラクトの状態変化を伴った関数の実行シーケンスを指します。したがって、低水準な仕様記述ではスマートコントラクト内部の実行の様子についての要求仕様まで記述できます。
低水準な仕様記述は、ホーア型のプロパティもしくはプログラムの実行フローによって与えられます。
ホーア式プロパティ
ホーア論理 (opens in a new tab)は、スマートコントラクトなどのプログラムの正当性を論証するための形式規則のセットを提供します。 ホーア式プロパティは、ホーアトリプル{P}c{Q}で表されます。cはプログラムで、PとQはc(つまりプログラム)の状態に関する述語であり、それぞれ_事前条件_と_事後条件_として正式に記述されます。
事前条件は関数を正しく実行するために求められる条件を表しています。スマートコントラクトを呼び出す際には、この事前条件が満たされている必要があります。 事後条件は、関数が正しく実行された場合に成立する条件を表しています。関数呼び出しの後はこの事後条件が真となることが期待されます。 ホーア論理の_不変条件_は、関数の実行によって維持される(つまり変化しない)述語です。
ホーア式の仕様では、_部分的正当性_または_完全な正当性_のいずれかが保証されます。 事前条件が関数実行前に真であり、実行が停止した場合には事後条件も真であるとき、スマートコントラクト関数の実装は「部分正当性を満たし」ます。 完全正当性を証明するには、関数の実行前に事前条件が真であること、実行が終了すること、その際に事後条件が真であることの三つが必要です。
プログラムによっては実行が終わるのに時間がかかったり、そもそも終わらなかったりするので、完全正当性の証明は困難となります。 とはいえ、イーサリアムのガスメカニズムが無限ループを防ぐので、実行が終了するかどうかは議論の余地はあれども理論上の問題点です(実行は正常に終了するか、'ガス不足'のエラーで打ち切られます)。
ホーア論理で作成されたスマートコントラクトの仕様記述は、スマートコントラクト内部の関数やループを実行するために述べられた事前条件、事後条件、不変条件を含みます。 事前条件が関数への誤った入力を許容する場合もあり、その際は事後条件でそのような誤った入力があった場合の応答(例外を発生させるなど)が記述されます。 このようにして、ホーア型のプロパティはスマートコントラクト実装の正当性を保証する際に効果を発揮します。
多くの形式的検証のフレームワークで、関数の意味的正当性を証明するためにホーア型の仕様記述が使われています。 また、Solidity の require および assert 文を使用することで、ホーア式プロパティを(アサーションとして)コントラクトコードに直接追加することも可能です。
require文は事前条件または不変条件を表現し、多くの場合ユーザー入力の検証に使用されます。一方、assertは安全性に必要な事後条件を捕捉します。 例えば、関数の適切なアクセス制御(安全性プロパティの一例)は、呼び出しアカウントのIDに対する事前条件チェックとして require を使用することで実現できます。 同様に、コントラクト内の状態変数の許容値に関する不変条件(例：流通しているトークンの総数)は、関数実行後に assert を使用してコントラクトの状態を確認することで、違反から保護することができます。
トレースレベルのプロパティ
トレースベースの仕様記述では、スマートコントラクトの状態を遷移する操作や、操作間にある関係を定義します。 前述したように、トレースは特定の方法でスマートコントラクトの状態を変化させる操作シーケンスです。
このアプローチは、スマートコントラクトのモデルがいくつかの定義済みの状態(状態変数で表されます) および遷移(スマートコントラクトの関数で表されます) を備えた状態遷移系で与えられていることを前提としています。 さらに、プログラムの実行フローをグラフで表現した制御フローグラフ (opens in a new tab)(CFG)が、コントラクトの操作的意味論を記述するためによく使用されます。 ここで、各トレースは制御フローグラフ上のパスで表されます。
主に、トレースレベルの仕様記述は、スマートコントラクトの内部の実行のパターンを論じる際に用いられます。 トレースレベルでの仕様記述を作成することで、スマートコントラクトに許容される実行パス(すなわち、状態遷移)をアサートできます。 シンボリック実行などの手法を用いれば、形式的モデルで定義されていないパスには実行が進まないことを形式的に検証することができます。
トレースレベルのプロパティを説明するために、パブリックにアクセス可能な関数を持つDAOコントラクトの例を使用してみましょう。 ここでは、DAOコントラクトによってユーザーが以下の操作を実行できることとします。
-
入金
-
入金後に、ある提案に対し投票をする
-
提案への投票をしなかった者は返金を要求する
トレースレベルのプロパティの例としては、_「資金を入金しないユーザーは、提案に投票できない」または「提案に投票しないユーザーは、いつでも返金を要求できる」_などが考えられます。 どちらのプロパティも望ましい実行シーケンスを表明します(入金する_前_に投票することはできず、提案に投票した_後_に払い戻しを要求することはできません)。
スマートコントラクトの形式的検証の手法
モデル検査
モデル検査は、仕様記述に対し、アルゴリズムによってスマートコントラクトの形式的モデルの検査を行う形式的検証の技法です。 モデル検査では通常、スマートコントラクトは状態遷移システムとして表され、許容されるコントラクトの状態のプロパティは時相論理を用いて定義されます。
モデル検査では、システム(すなわちコントラクト)の抽象的な数学的表現を作成し、そのシステムのプロパティを命題論理 (opens in a new tab)に根差した式を用いて表現する必要があります。 これにより、モデル検査アルゴリズムの目的は、数学的モデルが与えられた論理式を充足することの証明、と単純化されます。
形式的検証におけるモデル検査は主として、スマートコントラクトの挙動を時間経過を加味して記述する時間的プロパティの評価に用いられます。 スマートコントラクトの時相プロパティには、先に説明した_安全性_と_活性_が含まれます。
例えば、アクセス制御に関連するセキュリティプロパティ(例：コントラクトの所有者のみが selfdestruct を呼び出せる)は、形式論理で記述できます。 その後、モデル検査のアルゴリズムはスマートコントラクトがこの形式的仕様を満たしているかどうかを検証することができます。
モデル検査では、スマートコントラクトのすべての起こりうる状態を正確に描き、そのうちの到達可能な状態を見つけだそうと試みることで、状態空間の探索をします。 しかし、これは無限の状態数につながる可能性があります(「状態爆発問題」として知られています)。そのため、モデル検査器は抽象化技法によってスマートコントラクトの分析を効率化します。
定理証明
定理証明は、スマートコントラクトなどのプログラムの正しさを数学的に論証する手法です。 スマートコントラクトのシステムとその仕様記述を数式(論理式)で書き下す必要があります。
定理証明で目指すのは、それらの数式が論理的に等価であると検証することです。 「論理的同値」(「論理的双含意」とも呼ばれます)は、2つの文間の関係の一種で、第1の文が真である場合_に限り_、第2の文も真となります。
スマートコントラクトのモデルに関するステートメントとそのプロパティのステートメントとの間に要求された関係性(論理的等価性)は、証明可能なステートメント(定理と呼ばれます)として定式化されます。 形式的な推論システムにより、自動定理証明器は定理の妥当性を検証することができます。 言い換えれば、定理証明器はスマートコントラクトのモデルが仕様記述に正確に適合していることを、疑いの余地のない形で証明することができます。
モデル検査でスマートコントラクトが有限状態の遷移システムでモデル化されていたのに対し、定理証明では無限に状態を持つシステムの分析が可能となります。 しかし、 自動証明器があらゆる問題について「決定可能」かどうかを判断できるわけではないことをも意味します。
結果、定理証明器が正しさの証明を導出するためには、多くの場合、人による作業も必要となります。 モデル検査が完全に自動化されているのに対し、人手が必要となる定理証明にはより高いコストがかかります。
シンボリック実行
シンボリック実行は、具体的値(例：x == 5)の代わりに_シンボリック値_(例：x > 5)を用いて関数を実行することで、スマートコントラクトを分析する手法です。 形式的検証の手法として、シンボリック実行によってスマートコントラクトのコード中のトレースレベルのプロパティを形式的に論証することができます。
シンボリック実行では、実行トレースをシンボリック入力値に関する数式、別名_パス述語_として表現します。 SMTソルバー (opens in a new tab)は、パス述語が「充足可能」(すなわち、式を満たす値が存在する)かどうかを検査するために用いられます。 脆弱性のあるパスが充足可能であれば、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 を生成するかもしれません。
シンボリック実行はプログラムへの入力によって行うもので、到達可能なあらゆる状態を探索するための入力集合は潜在的に無限となるため、これは依然としてテスト技法の一形態です。 ただし、例に示すように、プロパティに反する入力を見付けることについては、シンボリック実行は通常のテスト技法より効果的です。
さらに、シンボリック実行は、関数への入力をランダム生成するようなプロパティベースの技法(ファジングなど)よりも偽陽性が少なくなります。 シンボリック実行でエラー状態に到達した場合は、そのエラーを引き起こす具体的な入力値を生成して問題を再現することができます。
シンボリック実行により、正しさに関するある程度の数学的証明を作成することもできます。 次のような、オーバーフローが防止されたスマートコントラクトの関数を例に考えます。
1function safe_add(uint x, uint y) returns(uint z){23 z = x + y;4 require(z>=x);5 require(z>=y);67 return z;8}整数オーバーフローを発生させる実行トレースは、z = x + y AND (z >= x) AND (z >= y) AND (z < x OR z < y)という式を満たす必要があります。このような式は解ける可能性が低いため、safe_add関数がオーバーフローしないことの数学的証明となります。
なぜスマートコントラクトを形式的に検証するのか
信頼性の必要性
形式的検証は、システム障害によって死傷者を出したり金融破綻を引きおこすなどの破滅的な結果となりうる、セーフティークリティカル・システムの正しさを評価するのに使用されます。 スマートコントラクトは膨大な価値を管理する高価値アプリケーションであり、設計上の単純なミスがユーザーにとって回復不能な損失 (opens in a new tab)につながる可能性があります。 デプロイする前にスマートコントラクトの形式的検証をすることで、ブロックチェーン上で期待通りに動作する保証が高まります。
特にイーサリアム仮想マシン(EVM)にデプロイされたコードは通常は変更不能であるため、あらゆるスマートコントラクトにおいて信頼性は非常に望ましいことです。 スマートコントラクトは起動後は容易にアップグレードできないので、信頼性の保証の需要により形式的検証が必要とされています。 整数のアンダーフローやオーバーフロー、リエントランスや不十分なガス最適化など、過去に監査担当者やテスターを躓かせてきた扱いにくい問題であっても、形式的検証で検出することができます。
機能的正当性の証明
プログラムテスト技法は、スマートコントラクトがある要求を満たしていることを証明する最も一般的な方法です。 プログラムテストでは、スマートコントラクトに正常に動作することが期待されるサンプルデータを与えて実行し、そのときの挙動を分析します。 期待通りの結果であれば、それが正しさの客観的な証明となります。
しかし、このアプローチではサンプルに含まれない入力値に関しては正しさを証明することができません。 したがって、コントラクトのテストはバグの検出に役立ちますが(すなわち、一部のコードパスが実行中に期待される結果を返さない場合)、バグが存在しないことを決定的に証明することはできません。
逆に、形式的検証は、コントラクトを一切実行すること_なく_、スマートコントラクトが無限の実行範囲に対する要件を満たすことを形式的に証明できます。 そのためには、スマートコントラクトの正しい挙動の詳細な形式仕様記述を作成し、スマートコントラクトのシステムの形式的(数学的)モデルを開発する必要があります。 そうすれば、形式的な証明手続きによって、スマートコントラクトのモデルとその仕様記述の間に矛盾がないことを確認することができます。
形式的検証により、スマートコントラクトのビジネスロジックが要件を満たしているかどうかを検証するという問題は、証明もしくは反証できる数学的命題となります。 形式的に命題を証明することで、無限にあるテストケースが有限の手順で検証できるようになります。 形式的検証には、スマートコントラクトが仕様記述に対して機能的に正しいこと証明することの、より良い将来性が見込まれます。
理想的な検証対象
検証の対象は、形式的に検証すべきシステムを記述します。 形式的検証は、「組み込みシステム」(大きなシステムの一部を形成する小さく単純なソフトウェア)で最もよく使用されます。 また、少数の規則のみを扱うドメインであれば、ドメイン固有のプロパティを検証するためにツールを変更することも容易であるため、形式的検証が適しています。
スマートコントラクトは、少なくともある程度は両方の要件を満たしています。 たとえば、イーサリアムのスマートコントラクトはサイズが小さいため、形式的検証が適しています。 同様に、EVMは単純なルールに従っているため、EVMで実行されるプログラムの意味論的なプロパティの仕様記述とその検証も容易になります。
開発サイクルの高速化
モデル検査やシンボリック実行などの形式的検証の技法は、一般的にスマートコントラクトのコードの定期的な分析よりも効率的です(テストや監査中に実行されます)。 これは、形式的検証がアサーションのテストにシンボリックな値(「ユーザーが n etherを引き出そうとした場合はどうなりますか？」)を用いるためです。 具体的な値を用いる場合(「ユーザーが5 ethを引き出そうとした場合はどうでしょう？」)とは異なります。
シンボリックな入力変数は複数クラスの具体的値をカバーできるため、形式的検証のアプローチでは、より短い時間でより多くのコードカバレッジが期待されます。 形式的検証を効果的に使用することで、開発サイクルを加速させることができます。
形式的検証は、コストのかかる設計エラーを減らすことで、分散型アプリケーション(dapps)を構築するプロセスも改善します。 脆弱性を修正するためにスマートコントラクトをアップグレードするには、コードベースの広範な書き換えと多くの労力が必要です。 形式的検証は、過去にテスターや監査担当者をつまずかせてきたスマートコントラクト実装のエラーを検出することができ、スマートコントラクトのデプロイ前に問題を修正する十分な機会を用意します。
形式的検証の欠点
手作業のコスト
形式的検証、特に半自動検証のように人が証明ツールを操作して正しさの証明を得るものは、かなりの手作業を要します。 さらに、形式仕様記述の作成は複雑な作業であり、高度なスキルが要求されます。
そのような要因(労力とスキル)により、形式的検証はテスト技法や監査など、スマートコントラクトの正しさを査定するための通常の手法に比べて多大な努力を要し、高コストとなります。 それにもかかわらず、スマートコントラクトの実装にエラーがあった場合の損害を考慮し、完全な検証監査のため実際にコストがかけられています。
偽陰性
形式仕様検証で確認できるのは、スマートコントラクトの実行が形式仕様記述に一致するかどうかのみです。 そのため、スマートコントラクトに求められる挙動が正しく仕様記述されていることが重要です。
もし仕様記述に不備があれば、形式的検証監査ではプロパティが破られることを検出できず、これはすなわち脆弱性のもととなります。 この場合、デベロッパーにスマートコントラクトにバグがないと勘違いさせてしまうことになります。
パフォーマンスの問題
形式的検証はパフォーマンス上の問題になります。 例えば、モデル検査とシンボル検査中に発生する状態爆発問題とパス爆発問題により、検証手順に悪影響がありえます。 また、形式的検証ツールは多くの場合にSMTソルバーやその他の制約ソルバーを内部的に使用しており、多量の計算処理を要します。
また、プログラムが決して停止しない可能性があるため、プログラム検証者がプロパティ(論理式として記述される)が満たされるかどうかを判断することが常に可能であるとは限りません(「決定可能性問題 (opens in a new tab)」)。 スマートコントラクトのプロパティが正しく記述されていたとしても、証明することが不可能なことがあります。
イーサリアムスマートコントラクトのための形式的検証ツール
形式仕様を作成するための仕様言語
Act: Actは、ストレージの更新、事前/事後条件、コントラクトの不変量の仕様を可能にします。 そのツールスイートには、Coq、SMTソルバー、またはhevmを介して多くのプロパティを証明できる証明バックエンドもあります。
Scribble - Scribbleは、Scribble仕様言語のコードアノテーションを、仕様をチェックする具体的なアサーションに変換します。
Dafny - Dafnyは検証対応のプログラミング言語で、高レベルのアノテーションに依存してコードの正当性について推論し、証明します。
正当性をチェックするためのプログラム検証器
Certora Prover - Certora Proverは、スマートコントラクトのコードの正当性をチェックするための自動形式的検証ツールです。 仕様はCVL(Certora Verification Language)で記述され、静的解析と制約解消を組み合わせてプロパティ違反が検出されます。
Solidity SMTChecker - SolidityのSMTCheckerは、SMT (Satisfiability Modulo Theories) とホーン解決に基づく組み込みのモデルチェッカーです。 コンパイル中にコントラクトのソースコードが仕様と一致するかどうかを確認し、安全性プロパティの違反を静的にチェックします。
solc-verify - solc-verifyはSolidityコンパイラの拡張版で、アノテーションとモジュラープログラム検証を使用してSolidityコードの自動形式的検証を実行できます。
KEVM - KEVMは、Kフレームワークで書かれたイーサリアム仮想マシン(EVM)の形式的意味論です。 KEVMは実行可能であり、到達可能性論理を用いて特定のプロパティ関連のアサーションを証明できます。
定理証明のための論理フレームワーク
Isabelle - Isabelle/HOLは、数式を形式言語で表現し、それらの式を証明するためのツールを提供する証明支援ツールです。 主な応用分野は、数学的証明の形式化、特に形式的検証であり、これにはコンピュータのハードウェアやソフトウェアの正当性の証明、コンピュータ言語やプロトコルのプロパティの証明が含まれます。
Rocq - Rocqは対話型の定理証明器で、定理を用いてプログラムを定義し、機械チェックされた正当性の証明を対話的に生成できます。
スマートコントラクトの脆弱なパターンを検出するためのシンボリック実行ベースのツール
Manticore - シンボリック実行に基づくEVMバイトコード分析ツール。
hevm - hevmは、EVMバイトコード用のシンボリック実行エンジン兼等価性チェッカーです。
Mythril - イーサリアムスマートコントラクトの脆弱性を検出するためのシンボリック実行ツール