【入門編】形式検証(Formal Verification)によるコントラクトの数学的証明 – IoT・OT（制御システム） & ブロックチェーンセキュリティ防御ガイド

こんにちは！スマートコントラクトの開発やブロックチェーンの世界へようこそ。

新しい技術を触るのって、ワクワクしますよね。「自分が書いたプログラムがそのまま世界中で動き、価値を動かす！」という体験は、何物にも代えがたい魅力があります。

でも、同時にこんな不安を感じたことはありませんか？
「もし自分が書いたコードにバグがあって、ハッカーに全財産を盗まれたらどうしよう…」

実は、ブロックチェーンの世界では、一度デプロイ（公開）してしまったスマートコントラクトは、原則として後から修正できません。バグがあったらゲームオーバー。これが、Web3セキュリティの最もシビアで、だからこそ燃えるポイントです。

今日は、そんな恐怖を打ち破り、あなたのコードが「絶対に破られない数学的な証明」を手に入れるための最強の武器、形式検証（Formal Verification）について、身近な例えを交えながら一歩ずつ優しく紐解いていきたいと思います！

—

1. テストと何が違うの？「泥棒対策」で考えるセキュリティ

新米開発者の頃って、「しっかりテストを書いたから大丈夫！」と思いがちですよね。ユニットテスト（単体テスト）を書いたり、ファジング（ランダムなデータを送り込むテスト）を回したり。もちろん、これらはとても大切です。

しかし、テストには限界があります。テストとはいわば、「家の中のあちこちを懐中電灯で照らして、泥棒が入れそうな隙間がないか探す作業」です。

どれだけ丁寧に照らしても、人間がやる以上は「うっかり見落とした暗がり」や「想像もしなかった侵入経路」が残ってしまいます。実際に、億単位の資金が盗まれたハッキング事件のほとんどは、「テストでは想定していなかった使われ方」を突かれたものでした。

そこで登場するのが「形式検証」です！

形式検証（CertoraやK-Frameworkなどを使用）は、懐中電灯で照らすのとは発想がまったく違います。

例えるなら、「物理法則レベルで、この家には絶対に誰も侵入できないことを、数学の数式で完全に証明してしまう」ようなものです。
「泥棒がどんなに天才的なピッキング技術を持っていようが、空を飛んでこようが、この数式が成り立つ限り、金庫の鍵は絶対に開かない」ということを、コンピュータに厳密に計算させて証明させます。

すごくないですか？不安なテストを何千回繰り返すよりも、「数学的に絶対に安全」と証明されている方が、圧倒的に夜ぐっすり眠れますよね。

—

2. 形式検証はどうやって動くの？（Certoraのイメージ）

「数学的証明なんて、博士号を持った天才にしか使えないんじゃ…？」と思われるかもしれませんが、ご安心ください。現代のツール（Certora Proverなど）は、開発者が実務で使えるようにすごく洗練されています。

形式検証を行うときは、主に以下の2つを定義します。

1. 実装コード（スマートコントラクト）：いつもあなたが書いているSolidityなどのコード。
2. ルール（仕様・プロパティ）：「このコントラクトの残高は、いかなる場合も預かり金の総額を下回ってはならない」といった、絶対に守るべきルール。

ツールは、「このルールが破られるような入力の組み合わせが、宇宙のどこかに存在するか？」を全パターン（無限の組み合わせ）網羅して数学的に探索します。もし抜け穴があれば、「ここがダメだよ」と具体的な反例（攻撃シナリオ）を教えてくれるんです。

—

3. 実践！シンプルなルールを書いてみよう

百聞は一見に如かず。簡単なスマートコントラクトに対して、どのようなルール（仕様）を書くのか、Certora風のCVL（Certora Verification Language）をイメージした例を見てみましょう。

まずは、すごくシンプルな銀行の預金コントラクト（Solidity）です。

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

// 誰でも預け入れと引き出しができるシンプルなバンクコントラクト
contract SimpleBank {
    mapping(address => uint256) public balances;
    uint256 public totalDeposits;

    // 預金機能
    function deposit() external payable {
        require(msg.value > 0, "Zero deposit");
        balances[msg.sender] += msg.value;
        totalDeposits += msg.value;
    }

    // 引き出し機能
    function withdraw(uint256 amount) external {
        require(balances[msg.sender] >= amount, "Insufficient balance");
        balances[msg.sender] -= amount;
        totalDeposits -= amount;
        
        (bool success, ) = msg.sender.call{value: amount}("");
        require(success, "Transfer failed");
    }
}

このコントラクトに対して、「絶対に守られなければならないルール」を数学的に定義します。
今回の絶対ルールは、「銀行全体の預かり金総額（totalDeposits）は、常に出息している個人の残高の合計と一致していなければならない」というものです。

以下が、その検証ルール（仕様ファイル）のサンプルです。

// SimpleBank.spec ファイルのイメージ
methods {
    // コントラクトの関数を検証ツールに教える
    function balance(address) external returns (uint256) envfree;
    function totalDeposits() external returns (uint256) envfree;
}

// 不変条件（Invariant）の定義
// 「いかなるトランザクションの前後でも、この条件は常に真（True）でなければならない」
invariant sumOfBalancesMustEqualTotalDeposits()
    // ※実際には全ユーザーの残高をスキャンするロジックや、
    // ツール独自の記述方法を用いて合計値と totalDeposits を比較します
    totalDeposits >= 0;

このように、「コードがどう動くか」だけでなく、「仕様としてどうあるべきか」をコードとは別の視点で記述し、ツールに検証させます。もしバグがあって totalDeposits の計算が狂うような実装ミスがあれば、検証ツールが即座に「この操作をするとルールが破られますよ！」と赤信号を灯してくれるわけです。

—

4. 新人のあなたが今日から意識すべきこと

形式検証は、最初は少し難しく感じるかもしれません。「仕様を正確に書き下す」という作業自体が、自分自身のロジックの整理にも直結するため、プログラミングスキルそのものを爆発的に底上げしてくれます。

実務や開発の現場で、一歩ずつ安全性を高めていくためのステップをまとめておきますね。

1. まず「当たり前のルール」を言葉にしてみる
コードを書く前に、「この変数はマイナスになってはいけない」「この関数は特定のオーナーしか呼べない」といった前提条件を、日本語やメモ書きでしっかり書き出す習慣をつけましょう。仕様の言語化こそが、形式検証の第一歩です。
2. テストと検証を組み合わせる
通常のユニットテストで細かな挙動を確認しつつ、クリエイティブな資産管理ロジックやDeFiのコア部分には、静的解析や今回紹介したような高度な検証手法を取り入れていく。このハイブリッドな姿勢が、頼れるセキュリティエンジニアへの近道です。
3. エラーや警告を無視しない
コンパイラや静的解析ツールが出す小さな警告（Warning）を、「動くからいっか」と放置していませんか？セキュリティ事故の多くは、そうした「小さな油断の積み重ね」から起こります。

—

まとめ

スマートコントラクトの開発は、自分の書いたコードに全責任を持つスリル満点の世界です。だからこそ、運や気合に頼るのではなく、「数学的な証明」という確かな裏付けを持つ技術を知っているかどうかが、プロとしての大きな分かれ道になります。

最初は難しく感じる用語も、一つひとつ紐解いていけば、あなたの心強い味方になってくれます。
一歩ずつ、安全で信頼されるWeb3の世界を一緒に作っていきましょう！