fizz

Fizz

在 {SUITE_DIR} 下生成有状态的 Solidity 模糊测试套件（默认：test/fizz/），并在 {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 仅跳过步骤 9。
• --max（或 --opus，或“max quality”）会将本次运行中的所有子 Agent 从 Sonnet 升级为 Opus。请参阅下方的“子 Agent 模型”。
• --guided / --automatic 用于选择运行模式。请参阅下方的“运行模式”。

运行模式

此技能以两种模式之一运行；在运行开始时确定模式，并在下方每个检查点中保持不变：

• {MODE} = "guided" — 父 Agent 会在关键检查点暂停并等待用户输入：步骤 3（补充文档）、步骤 4（交互式函数选择器 UI）、步骤 4.5（成本确认）、步骤 6（设置审查）、步骤 8（每轮覆盖率决策）、步骤 9c（属性审查）、步骤 10（模糊测试器选择）。
• {MODE} = "automatic" — 父 Agent 不会暂停。步骤 4 使用 --auto 运行；步骤 8 最多进行 3 轮覆盖率循环后继续；步骤 10 默认选择 Medusa；步骤 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} 未确定；步骤 0 会在打印横幅后通过选择提示询问用户。

所有后续引用 {MODE} 的指令都必须替换为已确定的值。运行过程中不得切换模式。

子 Agent 模型

此技能启动的所有子 Agent（步骤 3 的后备协议分析器、步骤 9b 的 5 个发现 Agent、步骤 9c 的综合 Agent、步骤 9d 的 2 个实现 Agent，以及步骤 11 的报告撰写 Agent）默认使用 Sonnet，以控制成本和延迟。

负责协调整个流程的父 Agent 使用用户 Claude Code 会话当前运行的模型（此技能无法控制该模型）。只有受委派的子 Agent 使用 {AGENT_MODEL}。

确定 {AGENT_MODEL}

在运行开始时确定一次，并在下方每次启动子 Agent 时保持不变：

• 如果用户使用 --max / --opus / “max quality” / “run on opus” / 类似选项调用 → {AGENT_MODEL} = "opus"。
• 如果用户使用 --sonnet / “use sonnet” / “default model” 调用 → {AGENT_MODEL} = "sonnet"。
• 否则，保持 {AGENT_MODEL} 未确定；步骤 0 会在打印横幅后通过选择提示询问用户。

下方所有后续启动子 Agent 的指令都会引用 {AGENT_MODEL}——实际调用工具时请替换为已确定的值。单次运行中不得混用不同级别的模型。

步骤 0：打印横幅

每次运行技能时，首先打印一次此 ASCII 横幅，然后才能输出任何其他内容（包括任何选择提示）：

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

打印横幅后，根据“运行模式”部分解析 {MODE}，并根据“子 Agent 模型”部分解析 {AGENT_MODEL}。对于仍未通过调用标志解析的值，通过一次 AskUserQuestion 工具调用询问用户，该调用只包含尚未解析的问题（如果两个值都已通过标志解析，则完全跳过调用）。

输出规范（强制）：在横幅块与 AskUserQuestion 调用之间，不得输出任何面向用户的文本——不说“我将询问……”，不说“正在加载工具……”，也不确认缺少标志。如果必须先通过 ToolSearch 获取 AskUserQuestion 的架构，也要静默执行。用户应看到：横幅 → 选择界面 → 已解析的值；中间不得有任何内容。此规定优先于工具调用前叙述意图的默认行为。

• 关于 {MODE} 的问题 — header: "Run mode"，question: "How should I run?"，选项：
  • label: "Automatic (Recommended)"，description: "Run end-to-end with no prompts."
  • label: "Guided"，description: "Pause at 7 checkpoints: extra docs, entry-point picker (browser UI), cost confirm, setup review, per-cycle coverage decision, property review, fuzzer choice."
• 关于 {AGENT_MODEL} 的问题 — header: "Subagent model"，question: "Which model should drive the subagents?"，选项：
  • label: "Sonnet (Recommended)"，description: "Default. Faster and cheaper for the 5 discovery agents, synthesizer, and 2 implementers."
  • label: "Opus"，description: "Higher quality but ~10× the cost. Equivalent to passing --max / --opus."

将用户的选择映射回 {MODE}（automatic / guided）和 {AGENT_MODEL}（sonnet / opus），然后打印以下两行，让已解析的值显示在对话记录中：

• Mode: guided 或 Mode: automatic — 已解析的 {MODE}。
• Subagent model: sonnet（默认）或 Subagent model: opus (--max)（如果用户请求了 --max / --opus / “max quality” / “use 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（每行一项，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 获取协议。在尝试 1–3 均已执行且结果记录到 /tmp/x-ray-attempts.md 之前，禁止使用协议分析器回退方案（尝试 4）。“我认为无法获取 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，并为每次尝试追加一条记录：时间戳、尝试名称、调用的命令/工具、准确输出（或“no output”）、结果（SUCCESS / FAILED: {reason} / SKIPPED: {reason}）。Attempt 4 要求文件中恰好包含 3 条记录（分别对应 Attempt 1、2、3）——SKIPPED 条目也计入总数。

• Attempt 1 — 调用技能。 使用 Skill 工具，调用 x-ray 技能，参数为 args="{PROJECT_ROOT}"。不要预先判断其是否可用——直接调用。只有形如“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) → 停止该技能。只有用户明确授权选择 (b) 时，才允许执行 Attempt 4。在 {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}，然后以 general-purpose Agent 启动，并设置 model: "{AGENT_MODEL}"。该 Agent 读取源文件，然后将分析结果写入 {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-ray 入口点映射（如果有）和源代码级访问控制观察结果。如果第 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 之前退出，请停止并报告该失败。

打印简短摘要：

• 已选合约
• 各合约已选函数
• 值得注意的排除函数

低频函数的分发器

读取选择结果后，将已选函数分为两个层级：

• 主要：应由模糊测试器频繁调用的核心用户流程（存款、取款、铸造、赎回、借款、还款、交换、质押、解除质押、领取、清算等）
• 次要：仍然有用但调用频率应较低的函数（管理员设置函数、配置变更、暂停/取消暂停、授予角色、调整参数等）

将此分类写入 {PROJECT_ROOT}/{META_DIR}/entry-point-selection.json，为每个函数条目添加 "tier": "primary" 或 "tier": "secondary" 字段。

在第 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}

这会将完整的模板脚手架复制到 {PROJECT_ROOT}/{SUITE_DIR}/，包括核心测试框架文件和实用工具文件，例如 utils/MockERC20.sol。它还会将模糊测试器配置文件（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 作为以下内容的权威依据：

• 代理和可升级性检测
• 设置要求和合理的默认值
• Mock 与真实依赖项的选择
• 依赖签名的设置指导
• Base.sol 集成点和 TODO/FIXME 策略

当目标协议依赖的简单外部 ERC20 不属于范围内的部署图时，优先使用脚手架中的 utils/MockERC20.sol 助手，除非项目已有更贴近实际的代币 Mock。

本步骤的关键产出是一个能够编译的脚手架，其中包含切实可用的 Base.sol::setup() 函数，其余核心脚手架也已相应调整。

如果 {MODE} = "guided"，在完成对 Base.sol 的修改后、运行 forge build 前，打印一个设置审查块，总结已接入的内容：

• 在 setup() 中部署的合约（名称 + 地址变量 + 构造函数参数来源）
• 检测到的代理及其封装的实现合约
• 使用的 Mock 与真实依赖项，以及每个 Mock 的原因
• 配置的 Actor（地址 + 角色），以及模糊测试器将通过处理器调用方选择进行模拟的 Actor
• 注入的余额（代币、接收方、数量）
• 角色／访问控制授权（角色、被授权方）
• 授权（代币、所有者、支出方、数量）

然后询问用户："设置看起来正确吗？回复“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 下驱动足够的协议覆盖率。

通过 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}

此脚本将：

• 在 foundry.toml 中追加 [profile.fuzz] 配置段，并设置 via_ir = false
• 运行 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，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}

使用 Agent 的命令执行工具异步运行 Medusa 脚本。这一点至关重要——请勿使用 shell 后台运行（&），请勿使用 sleep + tail 轮询，也不要在单个阻塞命令中同步等待。启动进程时，应确保 Agent 运行时可以跟踪进程，并在进程完成时通知你。

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

此包装脚本会启动一个临时的本地浏览器日志查看器并输出其 URL，但默认不会打开浏览器。请从包装脚本的输出中读取查看器 URL，并提供给用户。只有在用户要求自动在浏览器中打开查看器时，才将 --logs 添加到命令中。

后台命令完成并收到通知后，请检查生成的覆盖率，重点关注核心协议合约，而非外围模拟对象或辅助库。

动态覆盖率目标

不同合约所需的覆盖率并不相同。请根据合约的作用设定各自的目标：

合约角色	目标（no-ir）	目标（ir-no-opt）	目标（ir fallback）
核心协议逻辑（vault、pool、借贷核心、staking engine）	80%+	70%+	65%+
访问控制 / 角色管理	60%+	50%+	45%+
外围辅助组件（路由器、视图、适配器）	50%+	40%+	35%+
库和数学工具	由调用方继承覆盖率	同左	同左

使用与第 8.0 步中确定的模糊测试配置文件模式相匹配的列。

首次运行 Medusa 后，请查看各合约的覆盖率报告并对合约进行分类。如果在测试框架上下文中确实无法到达某些路径（例如，仅限 fork 的分支、跨多个区块的 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}
• 一个周期的流程为：运行 node {SKILL_PATH}/scripts/run_medusa.js {PROJECT_ROOT} --meta-dir {META_DIR} --coverage-mode，检查覆盖率，调整测试框架，然后重新构建

每个周期结束后，根据 Medusa 覆盖率报告生成并打印每个合约的覆盖率摘要表：

合约	角色	目标值	命中值	状态

Status 为 ✅（当 Hit ≥ Target），否则为 ❌。将同一张表追加到 {PROJECT_ROOT}/{META_DIR}/coverage-targets.md 中带时间戳的 ## Cycle N 标题下，以保留历史记录。

然后根据 {MODE} 分支处理：

• {MODE} = "automatic"：如果所有合约都达到目标，则简要总结并继续。否则继续循环；总计最多进行 3 个周期，然后在 coverage-targets.md 中记录剩余缺口，并使用当前测试框架继续下一步。
• {MODE} = "guided"：每个周期结束后（包括第 1 个周期），询问用户 "迭代 / 调整目标 / 继续"。iterate = 使用当前测试框架调整再运行一个周期。adjust targets = 让用户在下一个周期前编辑 coverage-targets.md 中每个合约的目标值。proceed = 无论是否存在缺口，都退出循环。遵循用户的选择；引导模式没有硬性上限。

退出循环后，提供覆盖率报告路径，供用户选择查看：{PROJECT_ROOT}/{META_DIR}/corpus_medusa/coverage/coverage_report.html。

可接受的跳过理由

在以下情况下，可以跳过特定函数或路径的覆盖率：

• 函数依赖无法模拟的外部状态（例如来自实时数据源的特定预言机价格）
• 路径属于仅触发回滚的保护逻辑，且在测试框架中有意设置为不可达（例如 require(msg.sender == bridgeContract)）
• 函数受时间锁或多签保护，而测试框架无法模拟这些机制
• 函数与未进行模拟的外部协议交互

请在 {PROJECT_ROOT}/{META_DIR}/coverage-targets.md 中记录每项跳过及其原因。

除非用户明确要求无论如何都继续，否则在 Medusa 覆盖率对于所选流程仍明显过低时，不要进入不变量生成步骤。

第 9 步：生成不变量（5 个并行发现 Agent + 综合器 + 2 个实现 Agent）

仅当用户传入 --no-invariants 时才跳过此步骤。

这是成败攸关的一步。此步骤会并行使用 5 个专门的发现 Agent，分别采用不同的不变量发现方法，这些方法源自模糊测试器发现的 50 多个真实 DeFi 漏洞。

步骤 9a：构建不变量上下文

阅读 property-generation.md，然后通过阅读以下内容构建 INVARIANT_CONTEXT：

• 步骤 3 中记录的不变量说明：如有，则读取 {PROJECT_ROOT}/x-ray/x-ray.md；否则读取 {PROJECT_ROOT}/{META_DIR}/protocol-understanding.md
• 如果 {PROJECT_ROOT}/{META_DIR}/additional-context.md 存在，则读取该文件（步骤 3 中引导模式提供的补充文档／链接）
• 所有范围内的源文件
• Base.sol、Snapshots.sol、Properties.sol
• 所有生成的处理器文件

从代码库中提取：

• AGGREGATE_VARIABLES：搜索名为 total*、sum*、accumulated* 的变量，或任何由多个函数写入的变量
• 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，或任何在两种单位体系之间进行映射的函数
• ACCESS_CONTROL：搜索 onlyOwner、onlyAdmin、onlyRole、require(msg.sender、自定义角色修饰符

步骤 9b：并行启动 5 个发现 Agent

重要：必须在同一条消息中启动全部 5 个 Agent（每个 Agent 调用一次工具，且都在同一条响应中）。

Agent	文件	发现方法
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 等）

读取每个 Agent 文件，将 {INVARIANT_CONTEXT} 和 {FILE_PATHS} 替换为实际值，并以 general-purpose Agent 启动，设置 model: "{AGENT_MODEL}"。

步骤 9c：综合属性计划

所有 5 个 Agent 返回后，读取 Synthesizer Agent 文件：

Agent	文件
6. Synthesizer	{SKILL_PATH}/agents/invariant-discovery/synthesizer.md

将 {AGENT_OUTPUTS} 替换为 Agent 1–5 的输出，将 {META_DIR} 替换为实际的 {META_DIR} 路径，将 {PROJECT_ROOT} 替换为实际的 {PROJECT_ROOT} 路径，并将 {SUITE_DIR} 替换为实际的 {SUITE_DIR} 路径，然后以 general-purpose Agent 身份启动，并设置 model: "{AGENT_MODEL}"。 Synthesizer 会合并、去重、确定优先级，并写入以下两个文件：

• {PROJECT_ROOT}/{META_DIR}/property-plan.md — 包含稳定 Spec ID（GL-NN、SP-NN）的实现表
• {PROJECT_ROOT}/PROPERTIES.md — 英文规格文档，包含 [ ] 复选框，每个属性对应一个条目，并使用相同的 Spec ID 标识。这是 /fizz-convert 命令和步骤 9d 中的实现者要操作的产物。

每个属性在生成时都会附带一个 Guarantee 标签——SHOULD-HOLD（由文档、规格、标准或精确恒等式明确保证，并引用了证据）或 EXPLORATORY（推断得出）。此标签可让步骤 10 在出现违规时直接进行分流，无需在活动结束后猜测严重程度：违反 SHOULD-HOLD 属性属于已确认的 Bug；违反 EXPLORATORY 属性则是需要人工审查的线索。

打印摘要：“Generated X properties (N HIGH, N MEDIUM, N LOW; P SHOULD-HOLD, Q EXPLORATORY)”，并简要列出优先级最高的属性。

如果 {MODE} = "guided"，请在此处暂停：告知用户文件路径（{PROJECT_ROOT}/PROPERTIES.md），总结 Synthesizer 生成的内容，并询问 "Review PROPERTIES.md and edit freely — rename, add, remove, or reword properties. Keep the Spec IDs (GL-NN / SP-NN) on entries you want implemented, and leave [ ] checkboxes unchanged. Reply 'proceed' when done, or 'regenerate' to re-run the Synthesizer with additional guidance." 如果用户回复 regenerate，询问需要更改什么，然后将补充指导附加到 Synthesizer 的输入中，并重新启动 Synthesizer（步骤 9c）。如果用户回复 proceed，继续步骤 9d。在 {MODE} = "automatic" 下，跳过暂停并直接继续。

步骤 9d：实现属性（2 个并行 Agent）

读取每个 Agent 文件：

Agent	文件	范围
7A. 全局属性实现者	{SKILL_PATH}/agents/implementers/global-property-implementer.md	Base.sol 中的 Ghosts、Snapshots.sol 中的 State、Properties.sol 中的全局属性，以及所需的 harness 合约
7B. 特定属性实现者	{SKILL_PATH}/agents/implementers/specific-property-implementer.md	Properties.sol 中的特定属性、handler 接线（ghost 更新 + 快照调用 + 属性断言）

将 {META_DIR} 替换为实际的 {META_DIR} 路径，将 {SKILL_PATH} 替换为实际的 {SKILL_PATH} 路径，将 {PROJECT_ROOT} 替换为实际的 {PROJECT_ROOT} 路径，并将 {SUITE_DIR} 替换为实际的 {SUITE_DIR} 路径，然后以 general-purpose Agent 身份并行启动两个 Agent，并设置 model: "{AGENT_MODEL}"。

两个实现者都必须针对实际实现的每个属性（按 Spec ID GL-NN / SP-NN 匹配），将 {PROJECT_ROOT}/PROPERTIES.md 中的 [ ] 改为 [x]。仍为 TODO 存根的属性保持 [ ]，以便 /fizz-convert 稍后处理。

步骤 9e：验证

编辑后运行 {FUZZ_BUILD_CMD}。修复所有编译错误。

如果某个属性在实现后置信度较低，应优先使用带注释的 TODO，而不是脆弱的断言。

步骤 10：运行测试活动

生成并验证不变量后，运行完整的模糊测试活动以查找属性违规。

Fuzzer 选择

• {MODE} = "automatic"：默认使用 Medusa——它支持多工作进程并行，速度更快，也更适合初次运行。
• {MODE} = "guided"：询问用户 "本次测试活动使用哪种 fuzzer——Medusa（默认，支持并行工作进程）还是 Echidna？"，并按用户的回答选择。如果用户没有偏好，则默认使用 Medusa。

不要同时运行两个 fuzzer——这会消耗过多资源，并可能导致系统不稳定或崩溃。下文的“测试活动迭代”会提供使用另一个 fuzzer 进行补充测试的选项。

运行测试活动

使用 Agent 的命令执行工具，以异步方式运行所选 fuzzer 的包装器，即 Medusa 或 Echidna（只能选一个），然后等待该跟踪中的后台作业完成——包装器会在 fuzzer 自身的停止条件触发或达到 --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 替换为所需的部署地址。

解读结果

测试活动完成后：

• 检查是否违反属性（断言失败）
• 对于每项违规，提取触发该违规的调用序列
• 确认该违规确实是一个 Bug，而不是测试框架问题——如果属性或处理器存在 Bug，则修复并重新运行
• 根据被违反属性的 Guarantee 标签进行分类（见 PROPERTIES.md）：违反 SHOULD-HOLD 属性表示已确认的 Bug——协议违反了文档记录或数学上的保证，因此应如实报告；违反 EXPLORATORY 属性则标记为需要人工审核——它可能是真正的 Bug，也可能是推断出的假设过强，因此应提供调用序列，由人工判断，而不要直接认定为 Bug。无论标签为何，都应先排除测试框架或属性本身存在 Bug 的可能性。
• 如果没有发现违规，报告测试活动已顺利完成，并说明达到的覆盖率
• 如果发现违规，逐项记录失败的属性名称、其 Guarantee 标签、调用序列以及失败时的合约状态

测试活动迭代

如果用户希望在首次测试活动后继续探索：

• 提议使用另一个 fuzzer 运行测试（如果使用了 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");。属性被违反时，测试通过。
     • 内联断言违规（处理函数内部通过 assert() / t() 触发回退的 _prop_* / _check* 断言）：违规的处理函数调用会在任何调用后断言运行前，通过 panic(0x01) 回退。将违规调用封装在 try this._repro_helperN() { revert("assertion should have fired"); } catch {} 中，其中 _repro_helperN() 是调用处理函数的 external 辅助函数。try/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}，然后以 general-purpose Agent 启动该代理，并设置 model: "{AGENT_MODEL}"。

该代理会读取测试活动的输出（覆盖率、语料库、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 skill 在后续源代码变更时检测差异，而无需重新运行完整流程：

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}

这会写入 {PROJECT_ROOT}/{META_DIR}/last-run.json，其中包含一份涵盖范围内的契约、处理程序和 PROPERTIES.md 条目的哈希+签名快照。之后，用户修改源代码并调用 /fizz-sync 时，该 skill 会与此文件进行差异比较，以检测新增、移除或变更的函数，隔离过时的属性，并仅重新生成发生差异的处理程序桩。