fizz

Fizz

{SUITE_DIR}（デフォルト：test/fizz/）に、状態を保持する Solidity ファズテストスイートを生成します。メタデータとファザーの実行時ファイルは {META_DIR}（デフォルト：fizz_data/）に生成します。

不変条件キャンペーンには Echidna と Medusa を使用します。コンパイル、スモークテスト、迅速なデバッグには Foundry を使用します。

ワークフロールール

• 手順を順番に実行してください。現在の手順に必要な成果物がまだ存在しない場合は、先に進まないでください。
• 手順が失敗した場合は、そこで停止し、ブロッカーを報告してください。
• ツールが不足している場合は、試した内容と不足しているものを正確に伝えてください。
• ユーザーが別のパスを明示的に指定しない限り、生成する Solidity スイートは test/fizz/ に、メタデータと実行時ファイルは fizz_data/ に分離して配置してください。
• 可能な限り既存のプロジェクト設定とテストロジックを再利用してください。リポジトリにすでにデプロイフローがある場合、新たに作り出さないでください。

パラメーター

• PROJECT_ROOT：ユーザー指定のパス。それ以外の場合は、現在の作業ディレクトリです。
• SKILL_PATH：この SKILL.md を含むディレクトリです。
• SUITE_DIR：PROJECT_ROOT からの相対パスである test/fizz です。スイート生成手順に --suite-dir を渡してください。
• META_DIR：PROJECT_ROOT からの相対パスである fizz_data です。メタデータ手順に --meta-dir を渡してください。
• オプションのコントラクト引数を指定すると、ハンドラー生成の対象を特定のコントラクトに絞り込めます。
• --no-invariants は Step 9 のみをスキップします。
• --max（または --opus、または「max quality」）を指定すると、この実行で使用するすべてのサブエージェントを Sonnet から Opus に切り替えます。詳しくは、以下の「サブエージェントモデル」を参照してください。
• --guided／--automatic で実行モードを選択します。詳しくは、以下の「実行モード」を参照してください。

実行モード

このスキルは、次のいずれかのモードで実行されます。実行開始時に一度だけ決定され、以下の各チェックポイントで共通して使用されます。

• {MODE} = "guided" — 親エージェントは重要なチェックポイントでユーザーの入力を待ちます。対象は Step 3（追加ドキュメント）、Step 4（対話型の関数選択 UI）、Step 4.5（コスト確認）、Step 6（セットアップのレビュー）、Step 8（サイクルごとのカバレッジ判定）、Step 9c（プロパティのレビュー）、Step 10（ファザーの選択）です。
• {MODE} = "automatic" — 親エージェントは一切待機しません。Step 4 は --auto で実行し、Step 8 はカバレッジサイクルを最大 3 回繰り返してから続行し、Step 10 はデフォルトで Medusa を選択します。Step 4.5 のコスト見積もりは表示しますが、ユーザーの確認を条件にしません。

{MODE} の決定

• ユーザーが --guided／「guided mode」／「walk me through」／「let me review」を指定した場合 → {MODE} = "guided"。
• ユーザーが --automatic／--auto／「unguided」／「run the whole thing」／「no prompts」を指定した場合 → {MODE} = "automatic"。
• それ以外の場合は {MODE} を未決定のままにします。Step 0 でバナーを表示した後に、選択プロンプトで確認してください。

以降、{MODE} に言及するすべての指示では、決定済みの値を使用してください。実行中にモードを切り替えないでください。

サブエージェントモデル

このスキルが起動するすべてのサブエージェント（Step 3 の Protocol Analyzer のフォールバック、Step 9b の 5 つの探索エージェント、Step 9c の Synthesizer、Step 9d の 2 つの Implementers、Step 11 の Report Writer）は、コストとレイテンシを抑えるため、デフォルトで Sonnet を使用します。

パイプラインを統括する親エージェントには、ユーザーの Claude Code セッションで実行中のモデルが使用されます（このスキルでは制御しません）。{AGENT_MODEL} が適用されるのは、委譲されるサブエージェントのみです。

{AGENT_MODEL} の決定

実行開始時に一度だけ決定し、以下のすべての起動で共通して使用してください。

• ユーザーが --max／--opus／「max quality」／「run on opus」または同様の指定をした場合 → {AGENT_MODEL} = "opus"。
• ユーザーが --sonnet／「use sonnet」／「default model」を指定した場合 → {AGENT_MODEL} = "sonnet"。
• それ以外の場合は {AGENT_MODEL} を未決定のままにします。Step 0 でバナーを表示した後に、選択プロンプトで確認してください。

以下の起動指示では、すべて {AGENT_MODEL} を参照します。実際のツール呼び出し時には、決定済みの値を使用してください。1 回の実行中にモデルの階層を混在させないでください。

ステップ 0：バナーを表示する

各スキル実行の開始時には、ほかの出力（選択プロンプトを含む）より先に、この ASCII バナーを 1 回だけ表示します。

██████╗  █████╗ ███████╗██╗  ██╗ ██████╗ ██╗   ██╗     ███████╗██╗  ██╗██╗██╗     ██╗     ███████╗
██╔══██╗██╔══██╗██╔════╝██║  ██║██╔═══██╗██║   ██║     ██╔════╝██║ ██╔╝██║██║     ██║     ██╔════╝
██████╔╝███████║███████╗███████║██║   ██║██║   ██║     ███████╗█████╔╝ ██║██║     ██║     ███████╗
██╔═══╝ ██╔══██║╚════██║██╔══██║██║   ██║╚██╗ ██╔╝     ╚════██║██╔═██╗ ██║██║     ██║     ╚════██║
██║     ██║  ██║███████║██║  ██║╚██████╔╝ ╚████╔╝      ███████║██║  ██╗██║███████╗███████╗███████║
╚═╝     ╚═╝  ╚═╝╚══════╝╚═╝  ╚═╝ ╚═════╝   ╚═══╝       ╚══════╝╚═╝  ╚═╝╚═╝╚══════╝╚══════╝╚══════╝
                                

バナーの後、「実行モード」セクションに従って {MODE} を、「サブエージェントモデル」セクションに従って {AGENT_MODEL} を解決します。呼び出しフラグで未解決の値がある場合は、未解決の質問だけを含む単一の AskUserQuestion ツール呼び出しでユーザーに尋ねます（両方ともフラグで解決済みの場合は、呼び出しを完全に省略します）。

出力の規律（必須）：バナーブロックと AskUserQuestion の呼び出しの間には、ユーザー向けのテキストを一切出力しません。「…について尋ねます」や「ツールを読み込み中です…」といった文言も、フラグが不足している旨の確認も出力しません。AskUserQuestion のスキーマを先に ToolSearch で取得する必要がある場合も、同様に何も表示せずに行います。ユーザーに表示されるのは、バナー → 選択 UI → 解決済みの値の行だけで、その間には何も表示されません。この規則は、ツール呼び出しの前に意図を説明するデフォルトの動作に優先します。

• {MODE} に関する質問 — header: "実行モード"、question: "どのように実行しますか？"、選択肢：
  • label: "自動（推奨）"、description: "プロンプトなしで最初から最後まで実行します。"
  • label: "ガイド付き"、description: "7 つのチェックポイントで一時停止します：追加ドキュメント、エントリーポイント選択（ブラウザー UI）、コスト確認、セットアップのレビュー、サイクルごとのカバレッジ判断、プロパティのレビュー、ファザーの選択。"
• {AGENT_MODEL} に関する質問 — header: "サブエージェントモデル"、question: "サブエージェントを動かすモデルはどれですか？"、選択肢：
  • label: "Sonnet（推奨）"、description: "デフォルトです。5 つの探索エージェント、統合担当、2 つの実装担当で、より高速かつ低コストです。"
  • label: "Opus"、description: "品質は高くなりますが、コストは約 10 倍です。--max / --opus を渡すのと同等です。"

ユーザーの選択を {MODE}（automatic / guided）および {AGENT_MODEL}（sonnet / opus）に対応付け、解決済みの値がトランスクリプト上で確認できるよう、次の 2 行を表示します。

• Mode: guided または Mode: automatic — 解決済みの {MODE}。
• Subagent model: sonnet（デフォルト）または Subagent model: opus (--max)（--max / --opus / 「最高品質を使用」/「Opus を使用」/ Opus の選択が要求された場合）。

ステップ 1：ツールと環境を確認する

次の手順を順番に実行します。

1. template-map.md を読みます。
2. forge --version を実行します。
3. forge --version が失敗した場合は、Foundry が見つからないことをユーザーに伝え、公式ドキュメントに従ってインストールするよう案内します。 Foundry のインストールガイド：https://www.getfoundry.sh/introduction/installation
4. forge --version が失敗した場合は、ここで停止します。以降のワークフローを進めるには Foundry が必要です。
5. bash {SKILL_PATH}/scripts/ensure_foundry.sh {PROJECT_ROOT} を実行します。
6. foundry.toml がない場合は、ensure_foundry.sh に作成させます。失敗した場合は停止し、エラーを報告します。
7. medusa --version を実行します。
8. echidna --version を実行します。
9. いずれかのコマンドが失敗した場合は、不足しているツールをユーザーに伝え、公式ドキュメントに従ってインストールするよう案内します。 Medusa のインストールガイド：https://secure-contracts.com/program-analysis/medusa/docs/src/getting_started/installation.html Echidna のインストールガイド：https://secure-contracts.com/program-analysis/echidna/introduction/installation.html
10. medusa --version が失敗した場合は、ここで停止します。以降のワークフローを進めるには Medusa が必要です。
11. echidna --version が失敗しても、Foundry と Medusa がインストールされていれば続行できます。ただし、完全なワークフローでは Echidna も必要なため、ユーザー向けの概要にインストール案内を含めてください。

ステップ 2：コンパイルと抽出

次の手順を順番に実行します。

1. {PROJECT_ROOT}/foundry.toml を読みます。
2. cd {PROJECT_ROOT} && forge build を実行します。
3. node {SKILL_PATH}/scripts/extract_abis.js {PROJECT_ROOT} --meta-dir {META_DIR} を実行します。

ステップ 3：プロトコルを理解する

このステップは、セットアップ、ハンドラーの選択、不変条件の生成品質を向上させるためのものです。

{MODE} = "guided" の場合、分析ソースに触れる前に、まずユーザーに次のように尋ねてください。"確認すべき追加のドキュメント、リンク、ホワイトペーパー、仕様ファイル、または過去の監査メモはありますか？（パスまたは URL を貼り付けるか、「none」と返信してください）"。ユーザーから何か提供された場合は、その生のリストを {PROJECT_ROOT}/{META_DIR}/additional-context.md に書き込んでください（1 行につき 1 項目とし、URL はそのまま記載します）。このステップの後続サブステップとステップ 9a では、このファイルが存在する場合は読み込み、プロトコル理解のコンテキストに組み込む必要があります。

まず {PROJECT_ROOT}/x-ray/ が存在し、x-ray.md が含まれているか確認してください。x-ray.md は必須です。存在しない場合、他のファイルがあるかどうかにかかわらず、x-ray の出力は利用できないものとみなされます。

{PROJECT_ROOT}/x-ray/x-ray.md が存在する場合は、プロジェクト理解の主要な情報源として、最初にこれを読んでください。その後、{PROJECT_ROOT}/x-ray/ に存在する以下の補足ファイルも読み込んでください。

{PROJECT_ROOT}/x-ray/x-ray.md が存在しない場合は、以下の x-ray 取得プロトコル を必ず実行してください。プロトコルアナライザーへのフォールバック（試行 4）は、試行 1〜3 をそれぞれ実行し、その結果を /tmp/x-ray-attempts.md に記録するまで禁止されています。「x-ray は利用できないと思う」は、正当なスキップ理由にはなりません。実際のツール／コマンドの実行結果が記録されている場合に限ります。

x-ray 取得プロトコル

Attempt 1 の前に、/tmp/x-ray-attempts.md が存在する場合は削除してください（rm -f /tmp/x-ray-attempts.md）。前回の実行時の古い記録が残っていると、Attempt 4 の条件を誤って満たしてしまいます。その後、新しい /tmp/x-ray-attempts.md を作成し、試行ごとに1件ずつ記録を追記してください。記録する内容は、タイムスタンプ、試行名、実行したコマンド／ツール、正確な出力（または「出力なし」）、結果（SUCCESS／FAILED: {reason}／SKIPPED: {reason}）です。Attempt 4 を実行するには、ファイルに正確に3件の記録（Attempt 1、2、3 各1件）が必要です。SKIPPED の記録も件数に含めます。

• Attempt 1 — スキルを呼び出す。 Skill ツールを使い、args="{PROJECT_ROOT}" を指定して x-ray スキルを呼び出してください。利用可能かどうかを事前に判断しないでください。実際に呼び出してください。「skill not found」／「unknown skill」という形式のランタイムエラーだけが、利用不可とみなされます。スキルが実行された場合は、完了を待ってから {PROJECT_ROOT}/x-ray/x-ray.md が書き込まれたことを確認してください。書き込まれていれば → SUCCESS として、プロトコルを終了します。

• Attempt 2 — 公式ソースからインストールして再度呼び出す。 次を実行してください。

  git clone --depth 1 https://github.com/pashov/skills.git /tmp/pashov-skills-xray-install \
    && mkdir -p ~/.claude/skills \
    && cp -r /tmp/pashov-skills-xray-install/x-ray ~/.claude/skills/x-ray
  

  その後、Skill('x-ray', args="{PROJECT_ROOT}") を再度呼び出してください。{PROJECT_ROOT}/x-ray/x-ray.md が生成されていれば → SUCCESS として、プロトコルを終了します。再度の呼び出しでも「skill not found」／「unknown skill」が返された場合（そのセッション中に自動検出が新しくインストールされたスキルを認識しなかった場合）は、まだこの試行を失敗と記録しないでください。代わりに ~/.claude/skills/x-ray/SKILL.md（または /tmp/pashov-skills-xray-install/x-ray/SKILL.md）を読み、その手順を {PROJECT_ROOT} に対してインラインで実行してください。その結果 {PROJECT_ROOT}/x-ray/x-ray.md が生成されていれば → SUCCESS とします。Skill の再呼び出しとインライン実行の両方が失敗した場合に限り、この試行を FAILED とします。

• Attempt 3 — ガイドモードでのユーザー確認（ガイドモードのみ）。 {MODE} = "guided" かつ Attempt 1～2 が両方とも失敗した場合は、ユーザーに次のように尋ねてください。"x-ray を自動取得できませんでした（ログ：/tmp/x-ray-attempts.md）。選択肢：(a) x-ray.md のパスを貼り付ける、(b) Protocol Analyzer フォールバックを許可する、(c) 中止する。a／b／c のいずれかを選んでください。" 回答を記録してください。(a) を選び、ファイルが存在する場合は {PROJECT_ROOT}/x-ray/x-ray.md にコピーし、SUCCESS とします。(c) を選んだ場合はスキルを停止します。Attempt 4 を許可するのは、(b) を選んだ場合のみです（ユーザーによる明示的な許可が必要です）。{MODE} = "automatic" の場合は、この試行をスキップし、SKIPPED: automatic mode と記録してください。

• Attempt 4 — Protocol Analyzer フォールバック。 /tmp/x-ray-attempts.md に Attempt 1～3 の記録（ステータスは FAILED、SKIPPED、または Attempt 3 の場合は (b) authorized）がある場合に限り、実行できます。起動する前に、ファイルの存在と記録が3件あることを確認してください。満たされていない場合は、不足している試行に戻ってください。先に進まないでください。

  フォールバック：{SKILL_PATH}/agents/protocol-analyzer.md を読み、{SKILL_PATH} を実際の {SKILL_PATH} に、{PROJECT_ROOT} を実際の {PROJECT_ROOT} に、{META_DIR} を実際の {META_DIR} に置き換えた後、model: "{AGENT_MODEL}" を指定して general-purpose エージェントとして起動してください。エージェントはソースファイルを読み取り、分析結果を {PROJECT_ROOT}/{META_DIR}/protocol-understanding.md に書き込みます。これにより、後続の手順では会話のコンテキストに頼らず、書き戻された分析結果を参照できます。

x-ray のドキュメントまたは protocol-understanding.md から、次の事項を推測して要約してください。

• デプロイの順序
• コンストラクター引数の意味
• デプロイ後に必要な初期化処理
• アクターの役割と、権限が必要な操作
• ハンドラーを有用にするために必要な承認、流動性、その他の状態
• 実際のファジング対象となる外部関数と、プロトコル内部の配線にすぎない関数
• Step 9 に引き継ぐ候補となる不変条件

読み取り後も不明点が残る場合は、保守的な前提を置いて進め、広範囲に推測するのではなく、後で対象を絞った TODO を残してください。

ここでは、ゴースト変数の配置、スナップショット構造体、最終的な実装の詳細を計画しないでください。代わりに、不変条件の候補を明確に記録してください。Step 9 では、{PROJECT_ROOT}/x-ray/ または {PROJECT_ROOT}/{META_DIR}/protocol-understanding.md からそれらを参照し、作業の出発点として再利用できます。

ステップ 4：エントリーポイントを選択する

selection-policy.md を読みます。

{PROJECT_ROOT}/{META_DIR}/entry-point-selection.json を作成します。これは {PROJECT_ROOT}/{META_DIR}/contracts.json をフィルタリングしたコピーで、有用な状態遷移を生成する可能性が最も高い関数を残します。

ステップ 3 で得たプロトコルの理解に基づいて事前選択を行います。主に、利用可能であればエントリーポイントの X 線マップと、ソースレベルで確認したアクセス制御に関する所見を使用します。ステップ 3 で呼び出し元またはアクセスに関する注釈付きのエントリーポイントマップが作成されている場合は、それを主要なフィルターとして使用します。内部呼び出し元のみの関数、またはコントラクト間の連携処理としてマークされた関数は除外します。{PROJECT_ROOT}/{META_DIR}/contracts.json は出力 JSON 形式の構造的なテンプレートとしてのみ使用し、含める関数の決定には使用しません。

次を実行します。

• {MODE} = "automatic" の場合： node {SKILL_PATH}/scripts/select_functions.js {PROJECT_ROOT} --contracts {PROJECT_ROOT}/{META_DIR}/contracts.json --selection {PROJECT_ROOT}/{META_DIR}/entry-point-selection.json --meta-dir {META_DIR} --auto
• {MODE} = "guided" の場合： node {SKILL_PATH}/scripts/select_functions.js {PROJECT_ROOT} --contracts {PROJECT_ROOT}/{META_DIR}/contracts.json --selection {PROJECT_ROOT}/{META_DIR}/entry-point-selection.json --meta-dir {META_DIR}

--auto フラグを指定すると、推定された選択がそのまま受け入れられ、即座に終了します。指定しない場合、スクリプトは推定された選択項目にあらかじめチェックを入れた状態でブラウザー UI を開き、ユーザーが調整して確定できます。どちらの場合も、entry-point-selection.json が書き込まれます。

スクリプトの完了後、{PROJECT_ROOT}/{META_DIR}/entry-point-selection.json を読みます。

entry-point-selection.json が書き込まれる前にスクリプトが終了した場合は、処理を停止し、その失敗を報告します。

次の内容を簡潔にまとめて表示します。

• 選択されたコントラクト
• コントラクトごとに選択された関数
• 特に注目すべき除外された関数

呼び出し頻度の低い関数用ディスパッチャー

選択内容を読み込んだ後、選択された関数を次の 2 つの階層に分類します。

• プライマリー：ファザーが頻繁に呼び出すべき主要なユーザーフロー（deposit、withdraw、mint、redeem、borrow、repay、swap、stake、unstake、claim、liquidate など）
• セカンダリー：有用ではあるものの、呼び出し頻度を下げるべき関数（管理者用のセッター、設定変更、pause/unpause、ロール付与、パラメーター調整など）

各関数エントリーに "tier": "primary" または "tier": "secondary" フィールドを追加して、この分類を {PROJECT_ROOT}/{META_DIR}/entry-point-selection.json に書き込みます。

ステップ 7 では、セカンダリー階層の関数を、列挙型セレクターを使って単一のエントリーポイントにまとめたディスパッチャーハンドラーでラップします。これにより、関数を完全に除外することなく呼び出し頻度を自然に下げられます。ファザーはランダムなセレクター値を選ぶため、セカンダリー関数も時折実行されますが、呼び出しシーケンスを支配することはありません。

選択時にユーザーがすでに関数を除外している場合、その関数は除外されたままです。ディスパッチャーは、ユーザーが残すことを選択したものの、優先度を下げるべき関数にのみ使用します。

{PROJECT_ROOT}/{META_DIR}/entry-point-selection.json が制限するのはハンドラーの生成のみです。セットアップの依存関係グラフは制限しません。

ステップ 4.5：コストの見積もり

次を実行します。

node {SKILL_PATH}/scripts/estimate_cost.js {PROJECT_ROOT} --meta-dir {META_DIR} --model {AGENT_MODEL} --mode {MODE}

スクリプトは entry-point-selection.json を読み込み、選択された関数の数に基づいてサイズ区分を適用し、ステージごとの内訳、合計、および予想範囲を記載した {PROJECT_ROOT}/{META_DIR}/cost-estimate.md を書き込みます。金額は Anthropic の定価に基づく概算であり、実際のコストはカバレッジサイクル、再実行、プロンプトキャッシュのヒット率によって変わります。

コスト見積もり表をユーザーに表示します。その後、次のように進めます。

• {MODE} = "automatic" の場合：一時停止せずにステップ 5 に進みます。
• {MODE} = "guided" の場合：ユーザーに 「この見積もりで続行しますか、それとも中止しますか？」 と尋ね、続行する前に確認を待ちます。ユーザーが中止した場合は実行を停止し、ここまでの成果物が書き込まれた場所を報告します。

ステップ 5：スキャフォールドの生成

次を実行します。

node {SKILL_PATH}/scripts/generate_suite.js {PROJECT_ROOT} --suite-dir {SUITE_DIR} --meta-dir {META_DIR}

これにより、コアハーネスファイルや utils/MockERC20.sol などのユーティリティファイルを含むテンプレート一式が {PROJECT_ROOT}/{SUITE_DIR}/ にコピーされます。また、ファザーの設定ファイル（echidna.yaml、medusa.json）が {PROJECT_ROOT}/ に書き込まれます。

さらに、{PROJECT_ROOT}/{META_DIR}/entry-point-selection.json を読み込み、選択されたコントラクトごとにスタブのハンドラーファイルを生成して {PROJECT_ROOT}/{SUITE_DIR}/handlers/ に配置します。これらのスタブには、上限ありと上限なしのセクション見出しが含まれますが、サンプルのハンドラー関数は含まれません。Handlers.sol は、生成されたすべてのハンドラースタブをインポートして継承するように用意されます。

コピーされたファイルはあくまで出発点として扱ってください。以降のステップでは、対象プロトコルに合わせて変更する必要があります。

ステップ 6：コアファイルの変更とセットアップの接続

setup-playbook.md と template-map.md を読んでください。

{PROJECT_ROOT}/{SUITE_DIR}/ にあるスキャフォールド済みのコアファイルを変更します。継承チェーン、各ファイルの役割、このステップで調整する想定のスキャフォールド済みファイルと後続のステップで調整するファイルについては、template-map.md を正としてください。

以下については、setup-playbook.md を正としてください。

• プロキシとアップグレード可能性の検出
• セットアップ要件と適切なデフォルト値
• モックと実依存関係の選択
• 署名に依存するセットアップのガイダンス
• Base.sol の統合ポイントと TODO/FIXME の方針

対象プロトコルが、対象範囲内のデプロイメントグラフに含まれない単純な外部 ERC20 に依存する場合、プロジェクトにすでにより忠実なトークンモックが含まれていない限り、スキャフォールド済みの utils/MockERC20.sol ヘルパーを優先してください。

このステップの主な成果物は、現実的な Base.sol::setup() 関数を備え、ほかのコアスキャフォールドもそれに合わせて調整された、コンパイル可能なスキャフォールドです。

{MODE} = "guided" の場合は、Base.sol の編集が完了した後、forge build の実行前に、接続した内容をまとめた セットアップレビュー ブロックを表示してください。

• setup() でデプロイされるコントラクト（名前 + アドレス変数 + コンストラクター引数の情報源）
• 検出されたプロキシと、それぞれがラップする実装
• 使用したモックと実依存関係、および各モックを選択した理由
• 設定したアクター（アドレス + ロール）と、ハンドラーの呼び出し元選択を通じてファザーが偽装するアクター
• 初期残高（トークン、受取人、数量）
• ロール／アクセス制御の付与（ロール、付与対象）
• 承認（トークン、所有者、使用者、数量）

次に、ユーザーに 「セットアップは問題ありませんか？ビルドするには「proceed」と返信するか、調整内容をお知らせください。」 と尋ねてください。ユーザーが調整を求めた場合は、それを適用してレビュー ブロックを再表示し、承認されるまで繰り返してください。{MODE} = "automatic" の場合は、レビュー ブロックを省略してそのまま続行します。

先に進む前に、cd {PROJECT_ROOT} && forge build を実行してください。

ステップ 7：ハンドラーを生成する

handler-patterns.md を読んでください。

まず、ハンドラー生成スクリプトを実行して、正しい関数シグネチャと型マッピングを含む、値があらかじめ設定されたスタブを生成します。

node {SKILL_PATH}/scripts/generate_handlers.js {PROJECT_ROOT} --suite-dir {SUITE_DIR} --meta-dir {META_DIR}

次に、以下を並行して読みます。

• {PROJECT_ROOT}/{SUITE_DIR}/handlers/Handlers.sol
• 生成された各 {PROJECT_ROOT}/{SUITE_DIR}/handlers/<Contract>Handler.sol
• 選択した各コントラクトのソースファイル

次に、選択したコントラクト用に生成された {PROJECT_ROOT}/{SUITE_DIR}/handlers/<Contract>Handler.sol を調整します。スタブには正しいシグネチャとクランプ処理のヒントがすでに含まれているため、実際のプロトコル呼び出しの接続、セマンティックなクランプ処理の追加、境界値ストレステスト用バリアントの実装に注力してください。

以下の内容の信頼できる情報源として handler-patterns.md を使用します。

• クランプ処理あり／なしのハンドラー構造
• ハンドラーの構成とセマンティックなアクションの選択
• 呼び出し元のコンテキスト
• クランプ戦略
• エッジケースおよびシグネチャに応じたハンドラーのガイダンス

Handlers.sol を更新して、生成されたすべてのハンドラーをインポートし、継承させます。

cd {PROJECT_ROOT} && forge build を実行し、次に進む前にコンパイルエラーを修正してください。

ステップ 8：Medusa でカバレッジを確保する

インバリアントを生成する前に、生成されたハーネスで Medusa のプロトコルカバレッジを十分に確保できることを確認してください。

Via-IR によるカバレッジ低下への対処

foundry.toml で via_ir = true が設定されている場合、Yul IR オプティマイザーは分岐を積極的に統合・削除します。これにより Medusa のカバレッジ数値が低下します。ソースカバレッジが 85% でも、Medusa のレポートが 65% になることがあります。最初の Medusa 実行前に対処する必要があります。

ステップ 8.0：ファズプロファイルを検出して設定する。

1. {PROJECT_ROOT}/foundry.toml を読み、[profile.default] 内またはトップレベルに via_ir = true が設定されているか確認します。
2. via_ir が有効でない場合は、このサブセクションをスキップしてください。ファズプロファイルは不要です。
3. via_ir が有効な場合は、次を実行します。

bash {SKILL_PATH}/scripts/setup_fuzz_profile.sh {PROJECT_ROOT}

このスクリプトは次の処理を行います。

• via_ir = false を含む [profile.fuzz] セクションを foundry.toml に追加します。
• FOUNDRY_PROFILE=fuzz forge build を実行します。
• コンパイルに成功した場合：終了コード 0 を返し、FUZZ_PROFILE=no-ir を出力します。
• "stack too deep" エラーが発生した場合：via_ir = true と optimizer_runs = 0 を設定して再試行し、終了コード 0 を返して FUZZ_PROFILE=ir-no-opt を出力します。
• どちらも失敗した場合：終了コード 1 を返します（デフォルトプロファイルを使い、カバレッジの低下を受け入れます）。

4. スクリプトの出力を読み、ファズプロファイルのモードを確認します。

   • FUZZ_PROFILE=no-ir → 正確なカバレッジ。標準の目標値を使用します。
   • FUZZ_PROFILE=ir-no-opt → 低下は軽減されますが一部残るため、カバレッジ目標値を約 10% 下げます。
   • スクリプトが失敗 → デフォルトプロファイルにフォールバックし、カバレッジ目標値を約 15～20% 下げます。

5. プロファイルモードを {PROJECT_ROOT}/{META_DIR}/coverage-targets.md の先頭に記録します。

   • no-ir：「ファズプロファイル：via_ir 無効 — カバレッジ数値は正確です」
   • ir-no-opt：「ファズプロファイル：via_ir が必要（stack too deep）、optimizer_runs=0 — カバレッジが約 10% 低下するため、目標値を調整済み」
   • デフォルトへのフォールバック：「ファズプロファイル：オプティマイザーを使用する via_ir が必要 — カバレッジが約 15～20% 低下するため、目標値を調整済み」

6. ステップ 8～11 の後続のすべての forge build コマンドでは、次を使用します。

   • {cd {PROJECT_ROOT} && FOUNDRY_PROFILE=fuzz forge build}（ファズプロファイルを作成した場合）
   • {cd {PROJECT_ROOT} && forge build}（ファズプロファイルが不要な場合）

後続のステップで再利用できるよう、ビルドコマンドを変数 {FUZZ_BUILD_CMD} に格納します。

Medusa の実行

このステップでの Medusa の各実行では、再実行もハーネスの変更後も、必ず run_medusa.js を使用してください。このステップの後続サイクルで、通常の medusa fuzz に切り替えないでください。

Medusa を起動する前に、ファズプロファイルが設定されている場合は、それを使って再ビルドしてください。

{FUZZ_BUILD_CMD}

エージェントのコマンド実行ツールを使用して、Medusa スクリプトを非同期で実行してください。これは非常に重要です。シェルのバックグラウンド実行（&）は使用せず、ポーリングに sleep と tail を組み合わせて使用せず、単一のブロッキングコマンドで同期的に待機しないでください。エージェントのランタイムがプロセスを追跡し、完了時に通知できる方法でプロセスを開始してください。

node {SKILL_PATH}/scripts/run_medusa.js {PROJECT_ROOT} --meta-dir {META_DIR} --coverage-mode

ラッパーは一時的なローカルのブラウザーログビューアーを起動して URL を出力しますが、既定ではブラウザーを開きません。ラッパーの出力からビューアーの URL を読み取り、ユーザーに提示してください。ユーザーがビューアーを自動的にブラウザーで開くよう求めた場合にのみ、コマンドに --logs を追加してください。

バックグラウンドコマンドが完了して通知を受け取ったら、周辺のモックやヘルパーライブラリではなく、コアプロトコルのコントラクトに重点を置いて、生成されたカバレッジを確認してください。

動的カバレッジ目標

すべてのコントラクトに同じカバレッジ目標が必要なわけではありません。コントラクトの役割に基づいて、コントラクトごとに目標を設定してください。

コントラクトの役割	目標（no-ir）	目標（ir-no-opt）	目標（ir フォールバック）
コアプロトコルロジック（vault、pool、lending core、staking engine）	80% 以上	70% 以上	65% 以上
アクセス制御／ロール管理	60% 以上	50% 以上	45% 以上
周辺ヘルパー（routers、views、adapters）	50% 以上	40% 以上	35% 以上
ライブラリと数学ユーティリティ	呼び出し元から継承されるカバレッジ	同左	同左

ステップ 8.0 で判定したファズプロファイルのモードに対応する列を使用してください。

最初の Medusa 実行後、コントラクトごとのカバレッジレポートを確認し、各コントラクトを分類してください。ハーネスのコンテキストで到達不能なパス（例：フォークでのみ実行される分岐、複数ブロックにまたがる MEV パス、オラクル障害時のパス）が正当に存在する場合は、それらを記録し、到達不能なコードにサイクルを費やさないよう、そのコントラクトの目標を引き下げてください。

コントラクトごとの目標と、スキップする理由を {PROJECT_ROOT}/{META_DIR}/coverage-targets.md に記録し、ユーザーが確認できるようにしてください。

カバレッジ反復ループ

• --coverage-mode を指定すると、ラッパーは medusa fuzz --timeout 300 を実行し、少なくとも 60 秒間のファジングを行います。その後、5 回連続して進捗行の branches hit が増加しなければ早期に停止し、完了時にカバレッジレポートのパスを出力します（--logs を追加するとブラウザでも開きます）
• カバレッジが目標を下回っている場合は、ハンドラーの形状、クランピング、セットアップ、承認、シード残高、呼び出し元のロール、および不足しているライフサイクルアクションを改善します
• 特定のハンドラーや呼び出しシーケンスが期待されるコードパスに到達しない理由をデバッグするとき、または仮説を検証するときは、FoundryTester.sol を使って迅速に PoC を行います
• 新しい Medusa 実行の前に毎回 {FUZZ_BUILD_CMD} を再実行します
• 1 サイクルは次のように扱います: node {SKILL_PATH}/scripts/run_medusa.js {PROJECT_ROOT} --meta-dir {META_DIR} --coverage-mode を実行し、カバレッジを確認し、ハーネスを調整してから再ビルドします

各サイクルの後、Medusa カバレッジレポートからコントラクトごとのカバレッジサマリーテーブルを作成して出力します:

Contract	Role	Target	Hit	Status

Status は Hit ≥ Target なら ✅、そうでなければ ❌ です。同じテーブルを、タイムスタンプ付きの ## Cycle N 見出しの下に {PROJECT_ROOT}/{META_DIR}/coverage-targets.md へ追記し、履歴を保持します。

次に {MODE} で分岐します:

• {MODE} = "automatic": すべてのコントラクトが目標を満たしていれば、簡単なサマリーを示して進みます。そうでなければループします。合計 3 サイクルを上限とし、その後は残っているギャップを coverage-targets.md に記録し、現在のハーネスのまま次のステップへ進みます。
• {MODE} = "guided": 毎サイクル後（サイクル 1 を含む）に、ユーザーへ "iterate / adjust targets / proceed" と尋ねます。iterate = 現在のハーネス調整で別のサイクルを実行します。adjust targets = 次のサイクルの前に、ユーザーが coverage-targets.md 内のコントラクトごとの目標を編集できるようにします。proceed = ギャップに関係なくループを終了します。ユーザーの選択に従います。guided モードにはハードキャップはありません。

ループを終了した後、任意レビュー用のカバレッジレポートのパスを提示します: {PROJECT_ROOT}/{META_DIR}/corpus_medusa/coverage/coverage_report.html。

許容されるスキップ理由

次の場合、特定の関数またはパスのカバレッジをスキップすることは許容されます:

• その関数がシミュレートできない外部状態を必要とする場合（例: ライブフィードからの特定のオラクル価格）
• そのパスが、ハーネス内で意図的に到達不能な revert 専用ガードである場合（例: require(msg.sender == bridgeContract)）
• その関数が、ハーネスがシミュレートしないタイムロックやマルチシグの背後にある場合
• その関数が、モックされていない外部プロトコルと相互作用する場合

各スキップを、その理由とともに {PROJECT_ROOT}/{META_DIR}/coverage-targets.md に記録します。

選択したフローに対して Medusa カバレッジがまだ明らかに低すぎる間は、ユーザーが明示的に進めるよう指示しない限り、不変条件生成へ進まないでください。

ステップ 9: 不変条件を生成する（5 つの並列ディスカバリーエージェント + シンセサイザー + 2 つの実装エージェント）

ユーザーが --no-invariants を渡した場合にのみ、このステップをスキップしてください。

これは成否を分けるステップです。これは 5 つの特化したディスカバリーエージェントを並列で使用し、それぞれがファザーによって捕捉された 50 以上の実際の DeFi バグから引き出された、異なる不変条件ディスカバリーアプローチを適用します。

Step 9a: 不変条件のコンテキストを構築する

property-generation.mdを読んだ後、以下を読み込んでINVARIANT_CONTEXTを構築します。

• {PROJECT_ROOT}/x-ray/x-ray.mdから取得したStep 3の不変条件に関するメモ（利用可能な場合）。それ以外の場合は{PROJECT_ROOT}/{META_DIR}/protocol-understanding.md
• 存在する場合は{PROJECT_ROOT}/{META_DIR}/additional-context.md（Step 3のガイド付きモードにおける補足ドキュメント／リンク）
• 対象範囲内のすべてのソースファイル
• Base.sol、Snapshots.sol、Properties.sol
• 生成されたすべてのハンドラーファイル

コードベースから以下を抽出します。

• AGGREGATE_VARIABLES：total*、sum*、accumulated*という名前の変数、または複数の関数が書き込む変数をgrepで検索します
• PAIRED_OPERATIONS：関数のペアを特定します（deposit/withdraw、mint/burn、add/remove、lock/unlock、open/close、stake/unstake、borrow/repay、create/destroy、join/exit）
• CONVERSION_FUNCTIONS：convertTo*、preview*、toAssets、toShares、または2つの単位系の間で変換する関数をgrepで検索します
• ACCESS_CONTROL：onlyOwner、onlyAdmin、onlyRole、require(msg.sender、カスタムのロール修飾子をgrepで検索します

Step 9b: 5つのディスカバリーエージェントを並列で起動する

重要：5つすべてのエージェントを単一のメッセージで起動する必要があります（エージェントごとに1回のツール呼び出しを、すべて同じ応答内で行います）。

エージェント	ファイル	ディスカバリー手法
1. 保全性監査者	{SKILL_PATH}/agents/invariant-discovery/conservation-auditor.md	すべての集計変数について、部分の合計＝追跡対象の全体となることを確認します
2. 往復変換と丸めの分析者	{SKILL_PATH}/agents/invariant-discovery/roundtrip-rounding-analyst.md	順方向と逆方向の操作、および方向ごとの丸めを分析します
3. 状態遷移マッパー	{SKILL_PATH}/agents/invariant-discovery/state-transition-mapper.md	事後条件、単調性、エンティティ数、状態機械を分析します
4. 敵対的利益最大化者	{SKILL_PATH}/agents/invariant-discovery/adversarial-profit-maximizer.md	攻撃者の視点で、DoS、価値の引き出し、エッジ状態を分析します
5. プロトコル型スペシャリスト	{SKILL_PATH}/agents/invariant-discovery/protocol-type-specialist.md	型を自動検出し、ドメインテンプレート（vault/lending/AMMなど）を適用します

各エージェントファイルを読み、{INVARIANT_CONTEXT}と{FILE_PATHS}を実際の値に置き換え、model: "{AGENT_MODEL}"を指定してgeneral-purposeエージェントとして起動します。

ステップ 9c：プロパティ計画を統合する

5 つのエージェントすべてから結果が返されたら、Synthesizer エージェントのファイルを読み込みます。

エージェント	ファイル
6. Synthesizer	{SKILL_PATH}/agents/invariant-discovery/synthesizer.md

{AGENT_OUTPUTS} をエージェント 1～5 の出力に、{META_DIR} を実際の {META_DIR} パスに、{PROJECT_ROOT} を実際の {PROJECT_ROOT} パスに、{SUITE_DIR} を実際の {SUITE_DIR} パスに置き換えてから、model: "{AGENT_MODEL}" を指定した general-purpose エージェントとして起動します。 Synthesizer は統合、重複の排除、優先順位付けを行い、次の BOTH を書き出します。

• {PROJECT_ROOT}/{META_DIR}/property-plan.md — 安定した Spec ID（GL-NN、SP-NN）を付与した実装テーブル
• {PROJECT_ROOT}/PROPERTIES.md — [ ] チェックボックスを含む英語の仕様書。各プロパティを 1 件ずつ記載し、同じ Spec ID で識別します。これは /fizz-convert コマンドとステップ 9d の実装者が操作する成果物です。

各プロパティには、生成時に設定される Guarantee タグが付きます。SHOULD-HOLD（ドキュメント、仕様、標準、または厳密な恒等式で明示的に保証され、根拠が引用されている）または EXPLORATORY（推論による）のいずれかです。このタグによって、ステップ 10 ではキャンペーン後に重大度を推測することなく、違反をトリアージできます。SHOULD-HOLD プロパティの違反は確認済みのバグ、EXPLORATORY プロパティの違反は人によるレビューの手がかりです。

概要を出力します。「X 件のプロパティを生成しました（HIGH N 件、MEDIUM N 件、LOW N 件、SHOULD-HOLD P 件、EXPLORATORY Q 件）」という形式で、優先度の高いプロパティを簡潔に列挙します。

{MODE} = "guided" の場合は、ここで一時停止します。ファイルパス（{PROJECT_ROOT}/PROPERTIES.md）をユーザーに伝え、Synthesizer が生成した内容を要約し、次のように尋ねます。「PROPERTIES.md を確認し、自由に編集してください。名前の変更、追加、削除、言い換えができます。実装するエントリーでは Spec ID（GL-NN / SP-NN）を残し、[ ] チェックボックスは変更しないでください。完了したら「proceed」と返信してください。Synthesizer を追加の指示付きで再実行する場合は「regenerate」と返信してください。」ユーザーが regenerate と返信した場合は、変更内容を尋ねてから、追加の指示を入力に加えて Synthesizer を再起動します（ステップ 9c）。proceed と返信した場合は、ステップ 9d に進みます。{MODE} = "automatic" の場合は、一時停止せずに直接進みます。

ステップ 9d：プロパティを実装する（並列エージェント 2 つ）

各エージェントのファイルを読み込みます。

エージェント	ファイル	範囲
7A. グローバルプロパティ実装エージェント	{SKILL_PATH}/agents/implementers/global-property-implementer.md	Base.sol の Ghost、Snapshots.sol の State、Properties.sol のグローバルプロパティ、必要に応じたハーネスコントラクト
7B. 個別プロパティ実装エージェント	{SKILL_PATH}/agents/implementers/specific-property-implementer.md	Properties.sol の個別プロパティ、ハンドラーの接続（Ghost の更新＋スナップショット呼び出し＋プロパティのアサーション）

{META_DIR} を実際の {META_DIR} パスに、{SKILL_PATH} を実際の {SKILL_PATH} パスに、{PROJECT_ROOT} を実際の {PROJECT_ROOT} パスに、{SUITE_DIR} を実際の {SUITE_DIR} パスに置き換えてから、両方を model: "{AGENT_MODEL}" を指定した general-purpose エージェントとして並列で起動します。

両方の実装者は、実際に実装した各プロパティについて、{PROJECT_ROOT}/PROPERTIES.md の [ ] を [x] に変更しなければなりません（Spec ID GL-NN / SP-NN で照合します）。TODO スタブのままのプロパティは [ ] のままにし、後で /fizz-convert が処理できるようにします。

ステップ 9e：検証する

編集後に {FUZZ_BUILD_CMD} を実行します。コンパイルエラーがあれば修正します。

実装後にプロパティの信頼度が低い場合は、脆弱なアサーションよりもコメント付き TODO を優先します。

ステップ 10：キャンペーンを実行する

不変条件の生成と検証後、プロパティ違反を見つけるために、ファジングキャンペーンを完全に実行します。

ファザーの選択

• {MODE} = "automatic"：デフォルトでMedusaを使用します。複数ワーカーによる並列処理で高速に実行でき、初回の実行に適しています。
• {MODE} = "guided"：ユーザーに 「このキャンペーンで使用するファザーはどれですか？ Medusa（デフォルト、並列ワーカー）またはEchidna」 と尋ね、回答に従います。希望が示されない場合は、デフォルトでMedusaを使用します。

両方のファザーを同時に実行しないでください。過剰なリソースを消費し、システムの不安定化やクラッシュを引き起こす可能性があります。もう一方のファザーを併用する実行は、下記の「キャンペーンの反復」で提案します。

キャンペーンの実行

選択したファザーであるMedusaまたはEchidna（どちらか一方のみ）のラッパーを、エージェントのコマンド実行ツールを使って非同期で実行し、その後、追跡対象のバックグラウンドジョブが終了するまで待ちます。ラッパーは、ファザー独自の停止条件が満たされるか、--timeoutに達すると終了します。どちらのラッパーも一時的なローカルのブラウザーログビューアーを起動してURLを出力しますが、デフォルトではブラウザーを開きません。ラッパーの出力からビューアーのURLを確認し、ユーザーに提示してください。ユーザーがブラウザーでビューアーを自動的に開くよう求めた場合に限り、コマンドに--logsを追加します。

Medusaの場合は、次のコマンドを実行します。

node {SKILL_PATH}/scripts/run_medusa.js {PROJECT_ROOT} --meta-dir {META_DIR} --timeout 600

Echidnaの場合は、次のコマンドを実行します。

node {SKILL_PATH}/scripts/run_echidna.js {PROJECT_ROOT} --meta-dir {META_DIR} --timeout 600

Echidnaでunlinked libraries detected in bytecodeエラーが発生した場合は、echidna.yamlでライブラリをリンクします。

deployContracts: [["0xf1", "Lib1"], ["0xf2", "Lib2"]]
cryticArgs: ["--compile-libraries=(Lib1,0xf1), (Lib2,0xf2)"]

Lib1、Lib2は実際のライブラリ名に、0xf1、0xf2は指定するデプロイアドレスに置き換えます。

結果の解釈

キャンペーンの完了後：

• プロパティ違反（アサーションの失敗）がないか確認します。
• 違反ごとに、その違反を引き起こした呼び出しシーケンスを抽出します。
• 違反がハーネスの問題ではなく、実際のバグであることを確認します。プロパティまたはハンドラーにバグがある場合は修正して、再実行します。
• 違反したプロパティのGuaranteeタグ（PROPERTIES.mdを参照）に基づいてトリアージします。違反したSHOULD-HOLDプロパティは確認済みのバグです。プロトコルが文書化された、または数学的に保証された条件を破っているため、その旨を報告します。違反したEXPLORATORYプロパティは人によるレビューの対象です。実際のバグである場合も、推論による仮定が過度に強い場合もあるため、バグだと断定せず、呼び出しシーケンスを提示して人が判断できるようにします。タグにかかわらず、まず必ずハーネスまたはプロパティのバグではないことを確認します。
• 違反が見つからなかった場合は、達成したカバレッジとともに、キャンペーンが問題なく完了したことを報告します。
• 違反が見つかった場合は、失敗したプロパティ名、そのGuaranteeタグ、呼び出しシーケンス、および失敗時のコントラクトの状態を含めて、それぞれ記録します。

キャンペーンの反復

最初のキャンペーン後にユーザーがさらに調査したい場合：

• 補完的な実行として、もう一方のファザー（Medusaを使用した場合はEchidna、その逆も同様）の実行を提案します。
• タイムアウトまたはテスト上限の引き上げを提案します。
• キャンペーン中に確認されたカバレッジの不足に基づいて、ハンドラーの形状を調整することを提案します。

ステップ11：検証と報告

次を実行します。

1. {FUZZ_BUILD_CMD}
2. FoundryTester.solが存在する場合は、cd {PROJECT_ROOT} && FOUNDRY_PROFILE=fuzz forge test --match-contract FoundryTesterを実行します（fuzzプロファイルを作成していない場合は、FOUNDRY_PROFILEを指定せずに実行します）。

検証に失敗した場合：

• 該当する壊れたファイルを修正します。
• ユーザーが求めない限り、テストスイート全体を再生成しないでください。
• 修正の再試行は最大3サイクルに制限し、その後、残った問題を明確に報告します。

違反の再現テストを生成する

ステップ 10 のキャンペーンでプロパティ違反が見つかった場合は、FoundryTester.sol に違反ごとの Foundry 再現テストを生成します。これにより、ファザーの出力を、違反が実在することを証明する決定論的なワンコマンドテストに変換できます。

実行するタイミング：{PROJECT_ROOT}/{META_DIR}/corpus_medusa/test_results/ に違反を示す JSON ファイルがある場合（Medusa）、または Echidna のログに呼び出しシーケンスを含む failed! 行がある場合に限ります。キャンペーンで違反が見つからなかった場合、このサブステップは完全にスキップしてください。

再現テストの生成方法：

1. 各違反ファイルを読み込みます（Medusa：test_results/ 内の違反ごとの JSON ファイル。Echidna：ログ内の各 failed! 行の後から呼び出しシーケンスを解析します）。
2. 違反されたプロパティごとに（同じプロパティの再現テストはまとめ、最短の呼び出しシーケンスのみ使用します）：
   • FoundryTester.sol に test_repro_<propertyName>() 関数を作成します。
   • JSON の methodSignature フィールドと inputValues フィールドからハンドラー関数を直接呼び出し、縮小された呼び出しシーケンスを再実行します。
   • 呼び出しの間に vm.roll() と vm.warp() を使用し、各呼び出しエントリーの blockNumberDelay と blockTimestampDelay の分だけブロック番号とタイムスタンプを進めます。
   • ファザーの from アドレスはインデックスに応じてアクターに対応します：0x10000 → actors[0]、0x20000 → actors[1]、0x30000 → actors[2]。クランプ済みハンドラーは toActor() を通すアクターシードパラメーターを受け取るため、生のファザー入力値を渡します。シードの剰余演算で適切なアクターが選択されます。
   • 違反パターンによって、必要なテスト構造が異なります：
     • グローバルプロパティ違反（bool を返す property_* 関数）：呼び出しシーケンス全体を再実行し、続けてプロパティが false を返すことをアサートします：assertFalse(property_xxx(), "property should be violated");。プロパティ違反が確認されると、テストは成功します。
     • インラインアサーション違反（ハンドラー内の _prop_* / _check* アサーションが assert() / t() によってリバートする場合）：違反を引き起こすハンドラー呼び出しは、呼び出し後のアサーションが実行される前に panic(0x01) でリバートします。違反を引き起こす呼び出しを try this._repro_helperN() { revert("assertion should have fired"); } catch {} で囲みます。_repro_helperN() はハンドラーを呼び出す external ヘルパー関数です。try/catch によってアサーションが発生したことを確認できます。catch が実行されると、テストは成功します。
3. {FUZZ_BUILD_CMD} を実行し、その後 cd {PROJECT_ROOT} && FOUNDRY_PROFILE=fuzz forge test --match-contract FoundryTester -vvv を実行して、すべての再現テストが成功することを確認します。
4. 再現テストのコンパイルに失敗した場合、または違反を再現できない場合は、修正します（テストごとに最大 2 回まで試行）。それでも失敗する場合は、テスト本体をコメントアウトし、// TODO: manual repro needed — fuzzer sequence did not reproduce under Foundry という注記を付けて次に進みます。

再現テストの命名規則：test_repro_<propertyName>（例：test_repro_property_solvency、test_repro_prop_depositIncreasesShares）。同じプロパティが複数の異なる根本原因（異なる呼び出しシーケンスが異なるコードパスに到達する場合）によって違反された場合は、_1、_2 のように接尾辞を付けます。

最終レポート

検証が成功したら、Report Writer サブエージェントを起動して最終レポートをまとめます。{SKILL_PATH}/agents/report-writer.md を読み込み、{SKILL_PATH} を実際の {SKILL_PATH} に、{PROJECT_ROOT} を実際の {PROJECT_ROOT} に、{META_DIR} を実際の {META_DIR} に、{SUITE_DIR} を実際の {SUITE_DIR} に置き換えたうえで、model: "{AGENT_MODEL}" を指定して general-purpose エージェントとして起動します。

このエージェントはキャンペーンの出力（カバレッジ、コーパス、medusa-run.log、PROPERTIES.md、Properties.sol、ハンドラーファイル、未解決の TODO）を読み込み、{PROJECT_ROOT}/{META_DIR}/report.md にレポートを作成します。

Report Writer エージェントは、ユーザーがインラインで確認できるよう会話にもレポートの内容を出力し、キャンペーンを手動で実行するためのコマンドも案内します。

• medusa fuzz（プロジェクトルートから実行）
• echidna . --contract FuzzTester --config echidna.yaml

将来の再利用に備えたスナップショット

最終レポートの作成後、同期スナップショットを取得しておくと、以降のソース変更時に /fizz-sync スキルがパイプライン全体を再実行せずに差分を検出できます。

node {SKILL_PATH}/scripts/fizz_sync.js {PROJECT_ROOT} --init --meta-dir {META_DIR} --suite-dir {SUITE_DIR}

以前の実行ですでに初期化されているなど、スナップショットがすでに存在する場合は、--refresh-snapshot を指定して再実行し、新しいベースラインに現在の状態を反映させてください。

node {SKILL_PATH}/scripts/fizz_sync.js {PROJECT_ROOT} --refresh-snapshot --meta-dir {META_DIR} --suite-dir {SUITE_DIR}

これにより、スコープ内のコントラクト、ハンドラー、PROPERTIES.md のエントリーのハッシュとシグネチャを記録したスナップショット {PROJECT_ROOT}/{META_DIR}/last-run.json が書き込まれます。その後、ユーザーがソースを変更して /fizz-sync を実行すると、このスキルはこのファイルとの差分を調べ、追加・削除・変更された関数を検出し、古くなったプロパティを隔離して、差分があったハンドラースタブのみを再生成します。