agentic-actions-audito…
Audits GitHub Actions workflows for security vulnerabilities in AI agent integrations including Claude Code Action, Gemini CLI, OpenAI Codex, and GitHub AI…
Writes, reviews, and debugs property-based tests — Hypothesis, fast-check, proptest, jqwik, rapid, and Echidna or Medusa for Solidity invariants. Use whenever tests should cover a whole input domain instead of a hand-picked list of examples: encode/decode and
$ npx -y skills add trailofbits/skills --skill property-based-testing --agent claude-codeHow it fires
How this skill gets triggered: by you, by Claude, or both.
/property-based-testingContext preview
The summary Claude sees to decide when to auto-load this skill.
Writes, reviews, and debugs property-based tests — Hypothesis, fast-check, proptest, jqwik, rapid, and Echidna or Medusa for Solidity invariants. Use whenever tests should cover a whole input domain instead of a hand-picked list of examples: encode/decode and
name: property-based-testing effort: low description: "Writes, reviews, and debugs property-based tests — Hypothesis, fast-check, proptest, jqwik, rapid, and Echidna or Medusa for Solidity invariants. Use whenever tests should cover a whole input domain instead of a hand-picked list of examples: encode/decode and serialize/deserialize pairs, parsers, canonicalizers and normalizers, validators, numeric and Decimal types, comparators and sort order, data structures, and smart-contract state invariants. Also use when adding cases to an existing @given, fast-check, or proptest suite, when judging whether existing property tests assert anything real, and when a generator has shrunk a counterexample and you need to tell a wrong property from a genuine bug. Not for coverage-guided binary fuzzing (libFuzzer, AFL), mutation-testing campaigns, static analysis, benchmarking, or end-to-end UI tests."
An example test asserts one point. A property asserts a rule over the whole input domain and lets the generator hunt for the counterexample. That trade is worth making when the code has an algebraic shape — an inverse, an invariant, an oracle — and not otherwise. Code with no such shape gets example tests; saying so is a valid outcome.
Check first whether the shape is missing or merely buried. A calculation wrapped in I/O, a string built by concatenation, an in-place mutation — each has a property and no seam to assert it through. See [references/refactoring.md](references/refactoring.md) before concluding there is nothing to assert.
| Property | Formula | Where it applies | |---|---|---| | Roundtrip | `decode(encode(x)) == x` | Serialization, conversion pairs | | Inverse | `f(g(x)) == x` | encrypt/decrypt, compress/decompress | | Oracle | `new(x) == reference(x)` | Optimization, refactoring, reimplementation | | Idempotence | `f(f(x)) == f(x)` | Normalization, formatting, sorting | | Invariant | Holds before and after | Any transformation, contract state | | Easy to verify | `is_sorted(sort(x))` | Complex algorithms with cheap checkers | | Commutativity | `f(a, b) == f(b, a)` | Binary and set operations | | Associativity | `f(f(a,b), c) == f(a, f(b,c))` | Combining operations | | Identity | `f(x, e) == x` | Operations with a neutral element |
Strength ordering, weakest to strongest: `no crash → type preservation → invariant → idempotence → roundtrip / oracle`.
Assert the strongest property the code supports. "No crash" alone rarely justifies the dependency — if that is all you can find, either a small rearrangement exposes something stronger, or the honest report is that this code is a poor PBT candidate. Rule out the first before settling for the second.
share can fail it. Pick a property that constrains the function without recomputing it. Note the exception: `f(x) == f(x)` is a genuine determinism property when `f` is not obviously pure — serializers over dicts or sets, hashing, anything reading the clock.
exercising anything, and self-contradictory `assume()` passes having run zero cases. Push constraints into the strategy so the generator produces valid inputs directly.
Load the one that matches the task in front of you:
| Task | File | |---|---| | Writing new tests, designing strategies | [references/generating.md](references/generating.md) | | The code has no property to assert yet | [references/refactoring.md](references/refactoring.md) | | Reviewing existing property tests | [references/reviewing.md](references/reviewing.md) | | A property test just failed | [references/interpreting-failures.md](references/interpreting-failures.md) | | Library choice, Echidna and Medusa | [references/libraries.md](references/libraries.md) |
If the project already uses a PBT library, just write the tests in it. If it does not, adding one is a dependency decision that belongs to the user — offer it once with the specific property you would write, and take the answer either way.
A Claude Code plugin marketplace from Trail of Bits providing skills to enhance AI-assisted security analysis, testing, and development workflows. Codex can load this marketplace through its Claude marketplace compatibility.
Audits GitHub Actions workflows for security vulnerabilities in AI agent integrations including Claude Code Action, Gemini CLI, OpenAI Codex, and GitHub AI…
Understand a codebase before looking for bugs in it - what each function assumes, what it guarantees, and what it depends on elsewhere. Use when starting an…
Scans Algorand smart contracts for 11 common vulnerabilities including rekeying attacks, unchecked transaction fees, missing field validations, and access…
Prepares codebases for security review using Trail of Bits' checklist. Helps set review goals, runs static analysis tools, increases test coverage, removes…
Scans Cairo/StarkNet smart contracts for 6 critical vulnerabilities including felt252 arithmetic overflow, L1-L2 messaging issues, address conversion problems,…
Systematic code maturity assessment using Trail of Bits' 9-category framework. Analyzes codebase for arithmetic safety, auditing practices, access controls,…