前言¶

写测试时最常见的做法，是先手搓几个例子：空字符串、最大值、一份「看起来像生产数据」的 JSON。覆盖率数字上去了，边界仍可能漏掉：孤立代理字符、65536 字节对齐、浮点下溢、畸形 UTF-8。属性测试（Property-Based Testing，PBT）换了一种问法——不是「这几个输入对不对」，而是「这类输入上，某条性质是否始终成立」。库会随机生成大量用例，失败时再收缩成最小反例。

问题是门槛不低。要判断哪里适合 PBT、该断言哪条性质、生成器怎么约束、失败究竟是代码 bug 还是测试写错，往往依赖经验。Trail of Bits 把这套方法论收进 Agent Skill property-based-testing：遇到序列化对、解析器、归一化函数或智能合约不变量时，让编程助手按同一套目录去写测试、审测试、解释失败，而不是临时发挥。

这是什么¶

一句话定位：property-based-testing 是一份跨语言、含智能合约的属性测试指导 Skill。它不替代 Hypothesis、fast-check、proptest 或 Echidna 这些库，而是告诉 Agent：何时该用 PBT、该测哪条性质、去读哪份参考文档、失败时先别当 bug 报。

它由安全公司 Trail of Bits 维护，放在公开的 Skills 市场仓库 trailofbits/skills 里，归类为 Verification 插件。插件元数据 .claude-plugin/plugin.json 写明：

• name：property-based-testing
• version：1.1.1
• description：Property-based testing guidance for multiple languages and smart contracts
• author：Henrik Brodin（归属 Trail of Bits）

仓库整体许可证是 CC BY-SA 4.0。官方 README 把它描述成 Claude Code 插件市场；同一份 README 写明 Codex 可通过 Claude marketplace 兼容层直接加载，不必另做 sidecar 元数据。Skill 本体是标准 SKILL.md，其他能发现技能目录的编程助手也可以用；具体落盘路径以安装器输出为准，这里不猜测。

SKILL.md 的 description 约定了触发时机：写测试、审查带序列化 / 校验 / 解析模式的代码、设计功能，或者判断 PBT 会比例子测试覆盖更强时使用。

目录比一份孤立的 SKILL.md 完整。入口文件负责检测模式和路由；细节拆在 references/：

property-based-testing/
├── SKILL.md
├── README.md
└── references/
    ├── generating.md              # 怎么写出可运行的属性测试
    ├── strategies.md              # 输入生成器
    ├── design.md                  # Property-Driven Development
    ├── refactoring.md             # 为可测性做重构
    ├── reviewing.md               # 已有 PBT 测试的质量清单
    ├── interpreting-failures.md   # 失败分析与 bug 分类
    └── libraries.md               # 按语言列出的 PBT 库（含合约工具）

仓库里还有 agents/、assets/。Skill 的决策树以 references/ 为准：当前任务决定读哪一篇，而不是把全部方法论一次性塞进上下文。

核心功能与亮点¶

下面能力来自官方 SKILL.md、插件 README，以及 Trail of Bits 站点上的同一份 Guide，交叉一致。

1. 按代码模式自动判断要不要上 PBT¶

Skill 要求在检测到高价值模式时主动启用，而不是等用户说出「属性测试」四个字。检测列表包括：

• 序列化对：encode/decode、serialize/deserialize、toJSON/fromJSON、pack/unpack
• 解析器：URL、配置、协议、字符串到结构化数据
• 归一化：normalize、sanitize、clean、canonicalize、format
• 校验器：is_valid、validate、check_*（尤其和归一化成对出现时）
• 数据结构：带 add/remove/get 的自定义集合
• 数学 / 算法：纯函数、排序、比较器
• 智能合约：Solidity / Vyper、代币操作、状态不变量、访问控制

优先级表把 encode/decode 的往返、纯函数、合约状态不变量标成 HIGH；校验「归一化后仍合法」、排序的幂等与有序、归一化幂等是 MEDIUM；builder / factory 的输出不变量是 LOW。

仓库 README 里的示例提示词可以直接拿来显式调用：

Write property-based tests for this JSON serializer
Review this Hypothesis test for quality issues
Help me design this feature using properties first
This function is hard to test - how can I refactor it?
Write Echidna invariants for this token contract

2. 性质目录，而不是「再多写几个例子」¶

核心不是随机砸输入，而是先选一条应当始终成立的性质。SKILL.md 的速查表如下（公式按原文）：

强度从弱到强写死为：

No Exception → Type Preservation → Invariant → Idempotence → Roundtrip

Skill 明确反对停在「没抛异常」：那是最弱的一条，有更强性质时要往上推。它也拒绝几类常见借口，例如「例子测试够了」「函数很简单」「没时间写生成器」——官方立场是：输入域复杂（字符串、浮点、嵌套结构）时，简单函数反而更适合 PBT；多数库自带策略，自定义生成器不是默认前提。

3. 按任务路由到不同参考文档¶

入口 SKILL.md 很短，真正可操作的内容在 references/。决策树按任务分流：

• 写新测试 → generating.md，生成器复杂再读 strategies.md
• 设计新功能 → design.md（先写可执行规格再实现）
• 代码难测（I/O 混在逻辑里、缺少逆操作）→ refactoring.md
• 审查已有 PBT → reviewing.md
• 测试失败要解释 → interpreting-failures.md
• 查库 → libraries.md

这和「把一本测试手册整页贴进 prompt」不同：Agent 只加载当前步骤需要的那一篇。

4. 建议方式有约束，避免硬推 PBT¶

检测到高价值模式时，Skill 要求先当成选项提出，而不是直接改测试风格。官方示例句是：

I notice encode_message/decode_message is a serialization pair. Property-based testing with a roundtrip property would provide stronger coverage than example tests. Want me to use that approach?

如果仓库里已经在用 Hypothesis、fast-check、proptest 或 Echidna，可以更直接：「This codebase uses Hypothesis. I’ll write property-based tests for this serialization pair using a roundtrip property.」用户拒绝后，写好的例子测试即可，不要继续推销。

同时列出红线：不要给平凡 getter/setter 推荐 PBT；不要只看到 encode 没有 decode 就谈往返；不要一次抛出超过 5–10 个候选；用户拒绝后不要纠缠。

5. 语言表覆盖应用代码和 EVM 合约¶

libraries.md 与插件 README 的语言表一致。常用对应关系：

智能合约侧：

教程指向 secure-contracts.com，不把合约工具的完整手册内嵌进 Skill。

安装与启用¶

官方安装分两条线：一条是 Trail of Bits 插件市场（Claude Code / Codex），一条是通用 skills CLI（目录页 officialskills.sh）。第三方目录上的安装次数、安全扫描分数不是官方数据，命令以 GitHub README 和这条目录页为准。

1. Claude Code：先加市场，再选插件（仓库推荐）

/plugin marketplace add trailofbits/skills
/plugin menu

在菜单里选择 property-based-testing。

2. Claude Code：按插件路径直接装

Trail of Bits 站点与插件 README 都给出：

/plugin install trailofbits/skills/plugins/property-based-testing

站点说明：在 Claude Code 里运行后启用该 Skill。

3. Codex：走同一套 Claude marketplace

仓库根 README：

codex plugin marketplace add trailofbits/skills
codex plugin list
codex plugin add property-based-testing@trailofbits

占位符 <plugin-name>@trailofbits 对应本插件的 name 字段 property-based-testing。

4. 通用 Agent Skills CLI（Cursor 等能发现 SKILL.md 的工具）

npx skills add https://github.com/trailofbits/skills --skill property-based-testing

也可以把 GitHub 目录地址贴给编程助手，让它按 Agent Skills 流程安装：

https://github.com/trailofbits/skills/tree/main/plugins/property-based-testing

装的是指导文档，不会替你安装 Hypothesis 或 Echidna。真正跑测试还要按 libraries.md 装对应库，例如：

pip install hypothesis

npm install fast-check

[dev-dependencies]
proptest = "1.0"

Echidna 需要 crytic-compile，二进制从 crytic/echidna 获取；Medusa 为 go install github.com/crytic/medusa@latest。版本号以各库当前文档为准，libraries.md 里的 pin 只是参考。

典型用法示例¶

下列提示词、代码和设置均出自官方 SKILL.md / generating.md / libraries.md，可按项目语言复现。

1. 在助手里触发这条 Skill

用接近 description 的说法即可：

这段代码有 encode/decode 成对出现。
请使用 property-based-testing：先判断该不该上 PBT，
再按 roundtrip 性质写测试；如果仓库里还没有 Hypothesis / fast-check，先说明要装哪个库。
不要停在「合法输入不崩溃」。

审查已有测试时改口「Review this Hypothesis test for quality issues」；合约则用「Write Echidna invariants for this token contract」。

2. 往返：编码后再解码应回到原对象

generating.md 的完整 Python / Hypothesis 示例（节选核心断言）：

from hypothesis import given, strategies as st, settings, example
from myapp.codec import encode_message, decode_message, Message, DecodeError

messages = st.builds(
    Message,
    id=st.uuids(),
    content=st.text(max_size=1000),
    priority=st.integers(min_value=1, max_value=10),
    tags=st.lists(st.text(max_size=50), max_size=20),
)

class TestMessageCodecProperties:
    @given(messages)
    def test_roundtrip(self, msg: Message):
        """Encoding then decoding returns the original message."""
        encoded = encode_message(msg)
        decoded = decode_message(encoded)
        assert decoded == msg

    @given(messages)
    def test_encode_deterministic(self, msg: Message):
        """Same message always encodes to same bytes."""
        assert encode_message(msg) == encode_message(msg)

    @given(st.binary())
    def test_decode_invalid_raises_or_succeeds(self, data: bytes):
        """Random bytes either decode or raise DecodeError."""
        try:
            decode_message(data)
        except DecodeError:
            pass

同一篇文档给的最短往返模板是：

@given(valid_messages())
def test_roundtrip(msg):
    """Encoding then decoding returns original."""
    assert decode(encode(msg)) == msg

3. 幂等：归一化两次应等于一次

@given(st.text())
def test_normalize_idempotent(s):
    """Normalizing twice equals normalizing once."""
    assert normalize(normalize(s)) == normalize(s)

4. 排序：长度、元素、有序、幂等一起断言

@given(st.lists(st.integers()))
@example([])
@example([1])
@example([1, 1, 1])
def test_sort(xs):
    result = sort(xs)
    assert len(result) == len(xs)
    assert sorted(result) == sorted(xs)
    assert all(result[i] <= result[i + 1] for i in range(len(result) - 1))
    assert sort(result) == result

@example 是官方要求显式补上的边界：空、单元素、重复，而不是只靠随机生成。

5. 生成器把约束写进策略，而不是事后 assume()

design.md 的原则：策略本身就是规格。合法区间写在 st.integers(min_value=1, max_value=100) 里；用 @given(st.integers()) 再 assume(1 <= x <= 100) 会提高拒绝率，属于应当改掉的写法。

Hypothesis 的样本量建议（generating.md）：

# 开发：快速反馈
@settings(max_examples=10)

# CI：更充分
@settings(max_examples=200)

# 夜间 / 发布：更彻底
@settings(max_examples=1000, deadline=None)

跑测试：

pytest test_file.py -v
pytest test_file.py --hypothesis-seed=0 -v
pytest test_file.py --hypothesis-show-statistics

6. 合约：Echidna 不变量命名

libraries.md 的最小例子：

function echidna_balance_invariant() public returns (bool) {
    return address(this).balance >= 0;
}

函数名以 echidna_ 开头，返回 bool。这是工具约定，不是业务不变量的完整模板；代币总供应、余额上界等要按合约文档另写。

7. 失败先分类，再决定要不要报 bug

interpreting-failures.md 把失败分成三类：测试写错（性质不对、生成了非法输入）、规格含糊、真正违反文档保证。工作流是：用收缩后的最小输入单独复现 → 对照类型注解、docstring、已有单测和外部规格「锚定」性质 → 检查策略是否超出函数应当处理的定义域 → 再分类。

只有同时满足「最小复现、性质对得上文档、输入在定义域内、能指出被违反的那条保证」才按 bug 报。文档明确排除：违反前置条件、规格写明未定义、依赖未文档化的实现细节、只在罕见平台出现、加上现实约束后失败消失。

适用场景与注意事项¶

适合

• 编解码、JSON / MessagePack、压缩解压这类成对操作，要验证往返
• URL / 配置 / 协议解析，输入域大、手写例子容易漏边界
• normalize / sanitize 需要幂等；校验器需要「归一化后仍合法」
• 纯函数、排序、自定义集合，能写出不变量或对照 oracle
• Solidity / Vyper 代币与状态不变量，配合 Echidna / Medusa
• 新功能希望先把性质写成可执行规格（design.md 的 Property-Driven Development）
• 逻辑和 I/O 缠在一起、缺少逆操作，需要先按 refactoring.md 抽出纯核心再测

不适合（Skill 原文）

• 没有变换逻辑的简单 CRUD
• 一次性脚本、用完即扔的代码
• 副作用无法隔离（网络、写库）
• 例子已经够、边界也清楚
• 集成测试、端到端测试（PBT 更适合单元 / 组件）
• UI / 展示逻辑
• 需求还在变的原型
• 用户明确只要例子测试

使用上的限制

• 这是方法论与检查清单，不是测试运行器。装 Skill 之后，CI 里仍然要跑 Hypothesis / fast-check / Echidna
• 「没崩溃」不是完成标准；同义反复（assert sorted(xs) == sorted(xs)）、矛盾的 assume()、把实现抄进断言，在 reviewing.md 里分别标成 CRITICAL / HIGH
• 失败先当测试问题查，不要默认报缺陷
• SwiftCheck 在语言表里标明已停止维护，不要当默认推荐
• 插件版本以 plugin.json 的 1.1.1 为准；文档站若仍显示 1.1.0，以仓库元数据为更高权威
• 与同市场的 spec-to-code-compliance、testing-handbook-skills、constant-time-analysis 可组合，但各自解决不同问题，不要混成一个「全能测试 Skill」

小结¶

property-based-testing 把「该不该做属性测试、测哪条性质、生成器怎么写、失败怎么定性」收成一份可被 Agent 加载的流程。入口负责识别序列化对、解析器、归一化和合约不变量；细节按任务拆到生成、策略、设计、重构、审查和失败解释。它由 Trail of Bits 维护，以 Claude Code 插件市场为官方分发，Codex 走同一套 marketplace；通用 SKILL.md 也可以经 npx skills add 装到其他编程助手。

属性测试本身仍然要靠各语言的库去执行。Skill 的价值是减少「知道 PBT 好、不知道从哪条性质下笔」这一段空白，并拦住同义反复和过弱断言。

官方地址：
https://github.com/trailofbits/skills/tree/main/plugins/property-based-testing/skills/property-based-testing

插件说明：
https://github.com/trailofbits/skills/tree/main/plugins/property-based-testing

Trail of Bits 页面：
https://trailofbits.com/skills/property-based-testing/

市场仓库：
https://github.com/trailofbits/skills