カルダノに訪れる新時代：スマートコントラクト検証の完全自動化へ

Lean4とZ3が切り拓く、開発者フレンドリーなフォーマル・ベリフィケーション

2025年7月17日、IOG（Input Output Global）は、カルダノにおけるスマートコントラクトの安全性と信頼性を飛躍的に高める新ツールの開発を公表しました。このツールは、開発者の手を煩わせることなく、スマートコントラクトの「形式的検証（formal verification）」を完全自動で実行できる画期的なものです。

なぜ形式的検証が必要なのか？

カルダノのスマートコントラクトは、Plinth、Aiken、Plu-tsなどの高水準言語で記述され、実際の資産を直接制御しています。つまり、コントラクトにバグがあれば、資金が盗まれたり、永久にロックされるリスクがあります。

従来のテストでは、想定したシナリオしか検証できず、実際に起こりうるすべての挙動を網羅するのは不可能です。これに対して形式的検証は、「この性質は常に成り立つ」という命題を数学的に証明し、あらゆる状況で正しく動作することを保証します。

ゲームチェンジャー：Lean4＋Z3による完全自動化

IOGの新ツールの最大の特長は、開発者が証明を書く必要が一切ない完全自動化です。Lean4という証明言語と、Z3やCVC5といったSMTソルバーを組み合わせることで、次のようなプロセスを実現します。

コントラクトを内部でLean4表現に自動変換
Universal Annotation Languageでプロパティ（性質）を指定
SMTクエリに変換し、定理を証明 or 反例を提示
問題があればリプレイ可能な具体的な反例を返却

つまり、ボタン一つで、CI/CDパイプラインに組み込んだ形式的検証が可能になります。しかも、開発者が使い慣れた言語や機能を制限しません。

検証例：ベスティングコントラクトの落とし穴

記事では、VacuumLabsのCTFからベスティング（権利確定）コントラクトの例を紹介。本来は「指定された時刻以降に、受益者本人が署名すれば資金を引き出せる」という仕様ですが、実装に潜むロジックの甘さをツールが見抜きました。

例として、validity_rangeの上限を非常に大きく設定すると、まだ時間が経っていないのに資金が引き出せてしまうという重大なバグが検出されました。

これは、形式的検証なしでは発見が困難な境界ケースであり、このような盲点をSMTソルバーが自動的に反例として提示してくれるのは強力です。

開発状況と今後の展望

このツールは現在、Lean4の推論コアとSMTバックエンドの接続まで完成しており、今後は以下を目指します：

UPLCコード（低レベル言語）への対応
Plutus CoreとCEKマシンの再実装による低層検証の自動化
最適化コードに対する形式的証明の支援

次回記事では、UPLCレベルの自動検証の具体例が紹介される予定です。

まとめ：スマートコントラクトの未来は「証明可能な安全性」へ

この自動検証ツールは、カルダノのスマートコントラクトに対して次のような未来をもたらします：

誰でも簡単にセキュアなコントラクトを開発可能
意図しない動作を事前に排除
ガバナンス提案やDeFi契約の透明性・信頼性を担保
Cardano上でのエンタープライズ利用や規制対応にも大きな前進

まさに、カルダノのスマートコントラクトに「自動で安全を証明する」という新しいパラダイムが到来したといえるでしょう。

以下はIOGブログ記事「A new era of smart contract verification on Cardano」を翻訳したものです。

IOGブログ「カルダノにおけるスマートコントラクト検証の新時代」：翻訳

セキュリティは重要です。カルダノのコントラクトの形式的検証（フォーマル・ベリフィケーション）をこれまで以上に簡単に、迅速に、そして手軽に行える新ツールの登場についてご紹介します。

2025年7月17日　著者：Romain Soulat

スマートコントラクト検証の新時代がカルダノに到来

カルダノ上では、スマートコントラクトは Plinth、Aiken、Plu-ts といった強力な高水準言語で記述されます。これらのコントラクトは実際の価値ある資産を制御しています。そのため、もしバグがあれば、資金が盗まれたり、永久にロックされる恐れがあります。

Input Output（IO）は、カルダノのスマートコントラクトに形式的検証を導入するための新しいツールを開発中です。エコシステム内には Agda や Rocq（旧 Coq）などの証明支援ツールをベースとした既存ツールがあり、高い保証を提供していますが、これらの使用には専門知識が必要です。

今回の新ツールは、Lean4という証明システムと、Z3のようなSMTソルバー（定理自動証明器）の力を組み合わせ、スマートコントラクトが意図通りに動作することを自動的にチェックします。目標は、開発者が自ら証明を書く必要をなくすことです。

以下は続きのセクションの翻訳です。

なぜこのツールがゲームチェンジャーなのか？

このツールが画期的なのは、完全自動化されている点にあります。

手動での証明作成や専門家による介入は一切不要です。ボタンをクリックするだけで、形式的検証が完了します。

つまり、このツールはCI/CDパイプラインに直接統合でき、コミットのたびにスマートコントラクトの形式的検証を即座に、継続的に、そして手頃なコストで行えるのです。現在も開発中であり、今後提供が予定されています。

なぜ形式的検証が必要なのか？

テストでは、開発者が思いついたケースやシナリオしか検証できません。プロパティベースのテスト（特性ベーステスト）はこれを補完しますが、それでも大部分のテスト空間は未検証のままです。

加えて、包括的なテストスイートを構築するには、多くのシナリオと攻撃パターンを網羅する必要があり、開発に多大な労力がかかります。テスト対象が多く複雑であるほど、保守も困難になります。

形式的検証では、コントラクトの特性（プロパティ）を明示的に記述し、それが常に成り立つことを数学的に証明できます。一部の形式的検証技術では、特性が成り立たない場合に反例（カウンターエグザンプル）を生成できます。

既存の形式的検証ツールは、高度なセキュリティ保証を提供する一方で、別の言語でモデルを開発しなければならない上に、特殊な専門知識が必要です。その複雑さ、自動化の欠如、再利用可能な反例が生成できないという点から、ほとんどの開発者にとっては敷居が高いのが現状です。

私たちの目指すもの

IOが開発中の自動形式検証ツールは、スマートコントラクトを以下の手順で検証することを目指しています：

表層のプログラミング言語（Plinth、Aiken、Plu-ts、UPLCなど）から、Lean4での内部表現に自動で変換し、意味的に忠実なモデルを構築。
コントラクトの特性を、Leanの定理として記述。特性は「Universal Annotation Language（汎用アノテーション言語）」で指定し、言語間を超えて利用可能に。
Lean表現と定理を、等価だがSMTソルバーで扱える形に変換・簡略化。
これらをZ3やCVC5といった強力なSMTソルバーに渡す。
結果として以下のいずれかを返す：
- 特性が成り立つというリプレイ可能な証明
- 問題を引き起こす具体的な実行トレースを含んだリプレイ可能な反例
- ソルバーが判定できなかった場合は、専門家による手動解決用の証明課題（proof obligation）

このツールは、内部に高度な最適化・単純化処理とCardano特有の知見を組み込むことで、専門家の介入を極力減らす設計になっています。

以下は続きのセクション「開発状況」の日本語訳です。

開発状況

現在、このツールの「推論コア（reasoning core）」は強力なバージョンが完成しています。

非常に専門的な最適化・簡略化・正規化の書き換えルールが多数実装されており、現実的なCardanoスマートコントラクト関数にもスケーラブルに対応できることが実証されています。

また、PlinthやAikenなどの表層言語が提供する高水準な機能の多くを考慮しているため、開発者がこれらの言語で使い慣れた機能を制限されることなく、当ツールを活用できるように設計されています。

Lean4の定理（ゴール）をSMTクエリへと変換するSMTバックエンドへのトランスレーションも構築済みで、さらに生成された反例をLeanに戻す仕組みも備えています。

シンプルな使用例

現在、まだどのプログラミング言語からLean4への完全なトランスパイラ（自動変換器）は存在していませんが、Lean4の例を使って当ツールの動作を実演できます。

ここでは、VacuumLabsの「キャプチャ・ザ・フラッグ（CTF）」チャレンジにおける「ベスティング（権利確定）コントラクト」の例を手動でLean4に翻訳したものを使用します。

以下のバリデータ（validator）は、以下の条件を満たすときのみベスティング・コントラクトにロックされた資金を使用可能とします：

トランザクションに、想定された受益者の署名が含まれている
ベスティング期間がすでに経過している

def validator : Demo -> VestingDatum -> VestingRedeemer -> ScriptContext -> Bool :=
    fun demo datum _ sc =>
        let transaction := sc.transaction;
        let purpose := sc.purpose;
        let signatories := transaction.signatories;
        let v_range := transaction.validity_range
        (purpose == Purpose.Spending) && (containsKey signatories datum.beneficiary demo) && (timeHasElapsed v_range datum.lock_until)

ここでは2つのヘルパー関数が使用されています。

1. containsKey

この関数は、与えられた署名リストに受益者の鍵が含まれているかどうかを確認します。

def containsKey : List VerificationKeyHash -> VerificationKeyHash -> Bool :=
   fun keys key =>
   match keys with
   | [] => false
   | k :: ks => if k == key then true else containsKey ks key

2. timeHasElapsed

この関数は、指定されたベスティング時間が経過しているかどうかをチェックします。

def timeHasElapsed : ValidityRange -> POSIXTime -> Bool :=
    fun range time =>
        range.upper_bound >= time.time

このコードは、開発者がPlu-tsやAikenといったCardanoの任意のスマートコントラクト言語を使って記述したであろう内容と非常に近いものです。

以下は続きのセクションの翻訳です。

期待される動作の検証

通常、こうしたコードが要件を満たしているかどうかを確認するには、テスター（あるいは開発者自身）が名目ケースや境界ケースを含む複数のシナリオを手動で書く必要があります。

しかし私たちのアプローチでは、期待される動作、つまり「満たすべき特性（プロパティ）」だけを記述すれば十分です。

期待される動作はLean4における定理（theorem）として表現できます。現段階では、この言語はあまりユーザーフレンドリーとは言えませんが（今後改善予定です！）、以下のように記述できます：

theorem only_accept_if_signatory_and_time_elapsed :
    ∀ (datum: VestingDatum) (redeemer: VestingRedeemer) (scriptContext : ScriptContext) (time: POSIXTime),
    
    (isValidCtx scriptContext time) →  
    (validator datum redeemer scriptContext) →

    (scriptContext.transaction.signatories.contains datum.beneficiary
     &&
     time.time ≥ datum.lock_until.time)

この定理が意味するのは以下の通りです：

datum（データ）、redeemer（リディーマー）、scriptContext（スクリプトコンテキスト）がどのようなものであっても、
time（現在時刻）がその有効範囲内にあり、
バリデータが true を返した場合には、

以下の条件が必ず成立していなければならない：

トランザクションの署名者リストに、データ内で指定された受益者が含まれている
現在の時刻が、データ内で指定されたロック解除時間（lock_until）よりも大きい

私たちのツールはこの定理を自動的にSMTクエリに変換し（これは開発者が直接読むものではありません）、SMTソルバーに送信します。

SMTソルバーの結果：定理は偽！

SMTソルバーはこの定理が偽（Falsified）であると報告しました。ツールは以下のような反例（テストケース）を出力しました（可読性のために一部整理済み）：

❌ 偽（Falsified）

反例：

datum：

{
  lock_until: 1,
  beneficiary: 0
}

time：

scriptContext：

{
  purpose: Spending,
  signatories: [0],
  validity_range: [0, 11798],
  ...
}

redeemer: 8335

この反例から明らかになるのは、timeHasElapsed 関数の検査ロジックに誤りがあるということです。実際、validity_range の上限が十分高ければ（この例では11798。ソルバーがやや過剰に設定）、実際の時間がまだ経過していなくても（現在時刻は0、ロックは1まで）、受益者が資金を引き出せてしまいます。

このシナリオは、VacuumLabsのCTFチャレンジの中でも、上限を非常に高く設定することで再現・検証できます。

今後の展望

これは、今後続くシリーズ記事の第一弾です。

次回の記事ではさらに深く掘り下げ、UPLCコード（Cardanoの低レベルスマートコントラクト言語）を、Lean4で再実装したCEKマシンおよびPlutus Coreの仕組みを用いて、どのように自動的に形式的証明できるかを紹介します。

この仕組みを実際のプロダクションコード上で実演し、さらにこのツールが、コードレベルで施された最適化の正式な証明にも活用できることを示していきます。

SITION Stake Pool & DReps Cardano ADA

IOGブログ, ニュース, ...

カルダノに訪れる新時代：スマートコントラクト検証の完全自動化へ