IOG のロマン・スラ氏とジャン＝フレデリック・エティエンヌ氏が、日本時間 10 月 9 日（金）17 時からの Cardano の開発者向けオンライン会「Developers Office Hours #82」で、検証ツール Blaster を実演します。Blaster は、Cardano のスマートコントラクトが仕様どおりに動くことを自動で証明するか、仕様を破る具体的な反例を返すツールです。
監査人が読んで「問題は見つからなかった」と言うのと、数学的に「この性質は必ず守られる」と示すのとでは、保証の強さが違います。後者を開発者の手元で回せるようにするのが Blaster の狙いで、Cardano のトレジャリーに資金を求めた取り組みの柱の一つでもあります。この記事では、実演の前に、Blaster が何をする道具で、どこまで公開されているのかを整理します。
金曜の実演で扱う 6 つの話題
Cardano の公式 X は、会の告知を次のように書いています。
Romain Soulat and Jean-Frédéric Etienne from IOG demo Blaster: it proves a Cardano contract meets its spec, or hands back the concrete counterexample that breaks it.
— Cardano 公式 X（2026 年 10 月 6 日 UTC）
参加登録のページによると、会のテーマは「スマートコントラクトが正しいと証明できるか」で、Google Meet で開かれます。予定されている話題は次の 6 つです。
- Lean 4 と自動証明
- UPLC と CEK マシン、台帳の形式化
- コントラクトの仕様の書き方
- 実演: 証明と反例
- Blaster のこれから
- 質疑応答
Blaster は何をするのか: 証明か、反例か
IOG が 5 月 12 日に公開した解説によると、Blaster は定理証明支援系 Lean 4 のための自動証明の仕組みです。開発者が「このコントラクトは、こういう条件では必ずこう振る舞う」という性質を書くと、Blaster はその性質が成り立つことを示すか、成り立たない場合には、どこで破れるかを示す具体的なスクリプトの文脈（取引の中身）を返します。
流れは 3 段です。まず、Plinth・Aiken・Plutarch といった言語で書いたバリデーター（取引を認めるかどうかを決めるスクリプト）を、Cardano が実際に実行する形式である UPLC（型なし Plutus Core）に変換します。次に、それを Lean 4 に取り込みます。最後に、Blaster が証明を試みます。言語を問わず、最終的に台帳で動く形に対して検証する点がこの設計の要です。
取り込み先の土台として、IOG は UPLC の完全なモデルと、2 種類の CEK マシン（UPLC を実行する仮想機械）を Lean 4 で書いています。1 つは実行の歩数を数えるもの、もう 1 つは実行コストの計算（コストモデル）まで組み込んだものです。
解説は実例として、Invariant0 が公開しているセキュリティ課題（CTF）の練習用コントラクト「nft_sell」を挙げています。Blaster はこのコントラクトに対して、台帳のルールに沿った完全な取引の文脈を自動で組み立て、「二重充足（double satisfaction）」と呼ばれる型の攻撃が通ることを示しました。1 つの支払いで 2 つの条件を同時に満たしたことにされてしまう、Cardano のコントラクトで知られた落とし穴です。
公開されている部品と、資金の出どころ
Blaster の部品は GitHub で公開されています。UPLC と CEK マシンを Lean 4 で書いた PlutusCoreBlaster（Apache-2.0）、証明に必要な台帳の型と述語をまとめた CardanoLedgerApiBlaster、そして SMT ソルバー（条件を満たす値があるかを機械的に探す道具）を使って推論する中核の Lean-blaster です。PlutusCoreBlaster と CardanoLedgerApiBlaster は、実演を前にした 10 月 6 日にも更新が入っています。
開発は、2026 年の「Cardano High Assurance」の取り組みのもとで続いていると IOG は説明しています。IO を含む 7 組織がこの取り組みのために出したトレジャリー引き出し案は、申請額 13,078,578 ADA のうち 10,112,037 ADA を Blaster の作業に充てる計画で、SIPO は DRep として 5 月に賛成の理由を公開しました（5 月 9 日の記事）。今回の実演は、その計画で作られているものが、開発者の手で使える段階にどこまで来ているかを見る機会でもあります。
SIPO 視点: 委任者や利用者にとっての意味
Cardano の DeFi に資金を預ける人の多くは、コントラクトを自分で読めません。頼りにしているのは監査報告で、監査はふつう、限られた期間に専門家がコードを読み、見つかった問題を報告するものです。見つからなかった問題が無いことまでは保証しません。
形式検証は、書かれた性質については「破れる取引は存在しない」と言い切れる点で、別の層の保証になります。限界もはっきりしていて、守るべき性質を書き漏らせば、その部分は何も保証されません。登録ページが「仕様の書き方」を独立した話題に立てているのは、そこが実務の難所だからでしょう。DeFi の利用者が今後、監査報告と並べて「どの性質が証明済みか」を問えるようになるかどうかは、開発者がこの道具をどれだけ日常に取り込むかにかかっています。
確かめられる次の一点は、10 月 9 日（金）17 時からの実演そのものと、その録画です。Developers Office Hours の過去回は録画が公開されており、登録ページからたどれます。実演で示される「証明」と「反例」が、練習用の課題を超えて実際に稼働しているコントラクトにどこまで当てられているかを見ます。
ことば
- Lean 4 — 数学の証明やプログラムの正しさを、機械が一歩ずつ確かめられる形で書くための言語と証明支援系。Blaster はその上で、証明を自動で探す役を担います。
- UPLC — Untyped Plutus Core の略。Aiken や Plinth で書いたコントラクトが最終的に変換され、Cardano の台帳で実際に実行される形式です。ここを検証の対象にすると、言語の違いを越えて同じ物差しが使えます。
- 二重充足（double satisfaction） — 1 つの出力が、複数のスクリプトの支払い条件を同時に満たしたことにされてしまう攻撃の型。EUTXO のコントラクトで繰り返し指摘されてきた落とし穴です。
一次ソース / 関連リンク
- Cardano 公式 X の告知（2026 年 10 月 6 日 UTC）
https://x.com/Cardano/status/2107507453063508091
GitHub
GitHub