Sui Prover がオープンソース化：形式検証がスマートコントラクト セキュリティの欠けたピースである理由
2025 年、DeFi はスマートコントラクトのエクスプロイトにより 33 億ドルを失いました。攻撃を受けたプロトコルのほとんどが監査済みであり、中には複数回監査を受けたものもあったにもかかわらずです。2 月の 15 億ドルの Bybit 流出、4,200 万ドルの GMX エクスプロイト、そして数え切れないほどのリエントランシー攻撃は、不都合な真実を証明しました。従来のセキュリティ監査は必要ですが、十分ではありません。数学的な精度が求められる場合、エッジケースをテストするだけでは不十分です。それらを「証明」する必要があります。
これこそが、Sui Prover のオープンソース化が単なる GitHub のリリース以上の意味を持つ理由です。Asymptotic によって開発され、現在は Sui 開発者コミュニティに無償で提供されている Sui Prover は、飛行制御システムやプ ロセッサ設計の失敗を防ぐために使用されるのと同じ数学的手法である「形式検証」を、日常のスマートコントラクト開発にもたらします。わずかな見落とされたエッジケースが数億ドルの流出を招く可能性がある現状において、コードが正しく動作することを数学的に証明できる能力は、もはや贅沢品ではなく、必需品となりつつあります。
監査のパラドックス：「安全」が十分ではないとき
2025 年のブロックチェーンセキュリティの状況は、懸念すべきパターンを浮き彫りにしました。Halborn の「Top 100 DeFi Hacks Report」によると、厳格な監査に合格したプロトコルであっても、依然としてエクスプロイトの犠牲になっていました。その理由は、サプライチェーンの脆弱性、アクセス制御の欠陥、経済モデルにおける微妙な数学的誤りなど様々でした。しかし、共通していたのは、手動レビューであれ自動スキャンであれ、従来のコード分析では考えられるすべての失敗モードを捉えきれなかったということです。
Yearn の yETH バグや Balancer の丸め誤差のエクスプロイトを考えてみましょう。これらは素人によるミスではありませんでした。数千もの実行パスにわたって丸め精度を武器に変えた、巧妙な数学的エラーでした。監査人が数週間かけてコードを確認したとしても、壊滅的 な挙動を引き起こすたった一つの入力の組み合わせを見逃す可能性があります。
GMX のエクスプロイトは、問題の別の側面を示しました。その脆弱性はコアの取引ロジックには存在せず、コンポーネント間の境界、つまりオラクルがマージン計算と出会い、清算ロジックがブリッジインフラと相互作用する場所で発生しました。失敗が相互作用から生じる場合、個々のコンポーネントをテストするだけでは不十分でした。
ここで形式検証は、従来のセキュリティアプローチと根本的に異なります。特定のテストケースをチェックする代わりに、形式検証は、考えられるすべての入力と実行パスにおいて特定のプロパティが維持されることを数学的に証明します。どのような状況下でもボールト（金庫）が空にならないことを証明できれば、テストで見逃した不明瞭なエッジケースを心配する必要はありません。
形式検証が実際に行うこと
形式検証は、コードを数学的な記述に変換し、それらの記述が意図した挙動の形式仕様と一致することを証明します。プロセスは以下の通りです：
まず、開発者はコードが何をすべきかを記述する仕様を作成します。これはプログラミング言語ではなく、数学的なプロパティを表現するために設計された特殊な仕様記述言語で行われます。スマートコントラクトの場合、これらの仕様には「ミントまたはバーンが呼び出 されない限り、トークンの総供給量は変化しない」や「ユーザーの残高は、ユーザーの明示的な許可がある場合にのみ減少する」といった記述が含まれます。
次に、プロバー（証明器）ツール（この場合は Boogie 検証エンジンと Z3 SMT ソルバー上に構築された Sui Prover）が、コードが考えられるすべての入力に対してこれらの仕様を満たしているかどうかを網羅的にチェックします。特定の値をチェックするテストとは異なり、プロバーは数学的な推論を通じて、考えられるすべての入力を同時に評価します。
検証に成功すると、指定されたプロパティが保持されているという数学的な証明が得られます。失敗した場合、プロバーは通常、仕様に違反する具体的な入力である「反例」を提示します。これにより、テストでは見逃されていた可能性の高いバグが明らかになることがよくあります。
Sui と Aptos の両方で使用されている Move プログラミング言語は、最初から形式検証を念頭に置いて設計されました。そのリソース指向モデルと強力な静的型付けは、Solidity のような言語よりも形式検証を実用的なものにする基盤を提供します。Move 仕様言語 (MSL) を使用すると、開発者は以下の 3 つのカテゴリのプロパティを表現できます：
- 構造体インバリアント (Struct Invariants)：構造体がその生存期間を通じて維持すべき状態
- 関数仕様 (Function Specifications)：各関数の事前条件、事後条件、および挙動の保証
- グローバル状態仕様 (Global State Specifications)：すべての状態遷移において維持されなければならないシステム全体のプロパテ ィ
Sui Prover：内部ツールからコミュニティのリソースへ
Asymptotic は当初、Sui 上で構築されているプロトコルの監査業務をサポートするために Sui Prover を開発しました。Sui における唯一の形式検証プロバイダーとして、彼らは手動レビューを超えて、クライアントのコードベースの高リスク領域を数学的に検証できるツールを必要としていました。
このツールをオープンソース化するという決定は、形式検証技術の成熟と、セキュリティが公共財であるという認識の両方を反映しています。より多くの開発者が形式検証にアクセスできるようになれば、エコシステム全体がより安全になります。これは、より高レベルな懸念事項に集中できるセキュリティ監査人を含む、すべての人に利益をもたらします。
Sui Prover は GitHub で公開されており、Homebrew (brew install asymptotic-code/sui-prover/sui-prover) 経由でインストールできます。活発な開発が続いており、2026 年 1 月には継続的な改善に向けた最新のイシューが報告されています。
Sui Prover を特に価値のあるものにしているのは、Sui Move の既存の開発ワークフローとの統合です。開発者は、既存のコードに仕様を段階的に追加し、重要な機能を優先的に検証しながら、徐々にカバー範囲を広げていくことができます。仕様は安全性のチェックとドキュメントの両方の役割を果たします。コントラクトをレビューしたり統合したりする人は誰でも、仕様を読んで保証された挙動を理解することができます。
証明可能な実世界のプロパティ
形式検証の力は、証明可能な具体的なプロパティを考慮すると非常に明確になります：
資金流出不可能なヴォルト：ユーザーの資金を保持する DeFi プロトコルにとって、適切な権限なしにどのような操作シーケンスを実行してもヴォルトから資金を流出させることができないと証明することは、攻撃カテゴリ全体を排除することを意味します。これは「多くの攻撃ベクトルをテストした」ということではなく、流出が不可能であるという数学的な確信です。
減少しないシェア価格：イールドヴォルトや流動性プールは、シェア価格が（予想されるスリッページを除いて）予期せず減少TypeValueしないことを保証する必要があることがよくあります。形式検証は、市場の状況やユーザーのアクションに関係なく、このプロパティが保持されることを証明できます。
正確な残高保持：トークンコントラクトは、すべての操作にわたって総供給量が一定であること、転送が指定された正確な量を移動すること、および指定された関数以外でトークンが生成または破棄されないことを証明できます。
アクセス制御の保証：コントラクトの状態や以前の操作シーケンスに関係なく、許可されたアドレスのみが特権関数を呼び出せることを証明します。
経済的インバリアント（不変条件）：複雑な DeFi プロトコルは、その経済モデルに関するプロパティを証明できます。流動性の制約が遵守されていること、担保率が維持されていること、アービトラージループが無限の価値を抽出できないことなどです。
これらは理論的な例ではありません。 Sui エコシステムの開発者は、 AMM やレバレッジイールドファーミングシステムを含む DeFi コントラクトを検証するために、すでに形式仕様を適用しています。これらのプロパティが想定ではなく証明されると、セキュリティポスチャ（セキュリティ体制）は根本的に変化します。
セキュリティ環境はより優れたツールを求めている
2025 年の統計は、形式検証の必要性を説得力のあるものにしています。セキュリティ研究者によると、 2024 年の攻撃の 56.5% 、失われた資金の 80.5% がオフチェーンのインシデントによるものでしたが、スマートコントラクトの脆弱性は、悪用されると依然として壊滅的です。アクセス制御の脆弱性だけで、 2024 年全体で 9 億 5,320 万ドルの文書化さ れた損害が発生しました。
2025 年の OWASP Smart Contract Top 10 では、分散型エコシステム全体で合計 14 億 2,000 万ドル以上の損失が記録されました。従来のセキュリティツール（シンボリック実行の Mythril 、プロパティベースのファジングの Echidna 、 OtterSec 、 Halborn 、 MoveBit などの企業による手動監査）は、問題のさまざまな側面に対処します。しかし、プロトコルがより複雑になり、より多くの価値を扱うようになるにつれて、これらのアプローチ間のギャップはより危険になります。
CertiK は形式検証技術を導入してスマートコントラクトを数学的に検証し、レポートによると 3,000 億ドル以上の資産を保護しています。この規模は、数学的なセキュリティ保証に対する需要と、ブロックチェーンシステムに形式手法を適用することの実現可能性の両方を示しています。
セキュリティ研究者の間で形成されつつあるコンセンサスは、監査、バグバウンティ、モニタリング、段階的なリリース、および形式手法が防御レイヤーとして連携する必要があるということです。高価値のシステムでは、重要な不変条件の形式検証は、例外的な厳格さではなく、標準的な慣行になりつつあります。
なぜ Move は形式検証を実用的なものにするのか
すべてのプログラミング言語が形式検証に等しく適しているわけではありません。 Solidity の柔軟性と EVM の複雑さは、形式検証を困難にします。不可能ではありませんが、多大なツールオーバーヘッドと専門知識が必要です。
Move は異なった設計がなされています。そのリソース指向モデルは、資産が暗黙的に複製されたり破棄されたりできない線形型（ Linear types ）を持つことを意味します。型システムは、他の言語ではランタイムチェックが必要となるカテゴリ全体のバグをコンパイル時にキャッチします。 Move Prover は言語と並行して開発され、言語機能と検証機能の緊密な統合を確実にしました。
この設計の伝統は、 Move 標準ライブラリ自体が形式検証されていることを意味します。 Sui や Aptos で構築する場合、数学的な正しさの証明がある基盤の上に構築することになります。その証明は、独自の検証済みコードをその上に重ねるにつれて複合されていきます。
実用的な意味として、 Move での形式検証は他のプラットフォームよりも専門的な専門知識を必要としません。 Sui Prover のドキュメント、例、および標準的な開発ワークフローとの統合により、形式手法の専門家ではない開発者でもアクセスしやすくなっています。単純な関数のコントラクトから始め、理解が深まるにつれて複雑な不変条件へと、段階的に仕様の書き方を学ぶことができます。
Sui 開発者にとっての意味
Sui で構築する開発者 にとって、オープンソースの Sui Prover は新しい可能性を切り拓きます：
セキュリティによる差別化：競争の激しい DeFi 環境において、セキュリティプロパティを証明することは単なるリスク軽減ではなく、競争上の優位性となります。ユーザーや監査人は、プロトコルの安全性に関する主張を、単なる言明を信頼するのではなく検証できます。
監査コストの削減：重要な関数に形式証明がある場合、監査人はエッジケースを徹底的にテストするのではなく、より高レベルの懸念事項に集中できます。これにより、セキュリティの成果を実際に向上させながら、監査の範囲とコストを削減できます。
ドキュメントの品質：形式仕様は、古くなることのない正確なドキュメントです。仕様が特定の不変条件を保持すると述べている場合、それは証明可能であるか、あるいは Prover が違反をフラグ立てするかのどちらかです。
段階的な導入：すべてを形式検証する必要はありません。引き出し、担保、または特権操作を処理するような、最もリスクの高い関数から始め、時間の経過とともにカバレッジを拡大してください。
Sui エコシステムには、 MoveBit （ Move 形式検証のパイオニア）、 Certora 、 OtterSec 、 Zellic など、複数の経験豊富な監査会社がすでに存在しています。 Sui Prover は、開発者があらゆる検証タスクで必ずしも外部の監査人を雇用することなく、直接使用できるツールを追加します。
より広範な軌道
Sui Prover のオープンソース化は、ブロックチェーン業界全体におけるセキュリティ ツールの成熟という、より広範なパターンに合致しています。形式検証（Formal verification）は、学術研究から本番環境のインフラへと、また専門のコンサルティング会社から開発者が利用可能なツールへと移行しつつあります。
スマート コントラクトによって保護される価値の規模が拡大し続けているため、この軌道は重要です。DeFi プロトコルは総額で数千億ドルの資産を管理しています。主要なプロトコルにおけるたった 1 つのバグが、従来のソフトウェア企業が全存続期間を通じて直面する額を超える損失を引き起こす可能性があります。
従来のソフトウェア業界は、最終的に航空電子機器、医療機器、金融システムなどの安全性に不可欠なシステムに形式手法を採用しました。「コードは法なり（Code is Law）」であり、バグが不可逆的であることが多いブロックチェーン業界には、数学的検証を取り入れるさらに強力な理由があります。
Sui Prover はこの方向性における一歩を象徴しています。つまり、形式検証を誰も読まない形ばかりのセキュリティ ドキュメントとして放置するのではなく、開発者が実際に使用できるほど身近なものにすることです。
はじめに
Sui での形式検証の探索に関心のある開発者向け：
- Sui Prover のインストール:
brew install asymptotic-code/sui-prover/sui-prover - スモール スタート: 1 つの重要な関数に仕様を追加し、それがパスすることを確認します。
- 仕様言語の学習: Move Specification Language には、一般的なプロパティを表現するための優れたドキュメントがあります。
- 反復: 自信を深めるにつれて、より多くの関数やより複雑な不変条件へとカバレッジを拡大します。
形式仕様の学習への投資は、複利的な利益をもたらします。低レベルのモジュールが正しいことを検証できれば、それらの基盤が数学的に証明されていることを確信した上で、高レベルのロジックを構築できます。
2025 年に予防可能なバグによって数十億ドルを失った業界にとって、形式検証に努力を払う価値があるかどうかは問題ではありません。問題は、エコシステムがどれだけ迅速にそれを採用できるかです。Sui Prover のオープンソース リリースは 1 つの障壁を取り除きました。今後は知識と実践がそれに続く必要があります。
Sui で安全なアプリケーションを構築するには、プロトコルのセキュリティ標準に一致する信頼性の高いインフラストラクチャが必要です。BlockEden.xyz は、Sui、Aptos、および 20 以上のチェーンに対して、本番環境のアプリケーションが求める稼働率と信頼性を備えたエンタープライズ グレードの RPC エンドポイントを提供します。当社の API マーケットプレイスを探索して、形式検証済 みのスマート コントラクトを強化しましょう。