前言¶

寫測試時最常見的做法，是先手搓幾個例子：空字符串、最大值、一份「看起來像生產數據」的 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