Graham Sutherland
04b241176f
* Rework property-based-testing skill and add eval suites. * Fix shellcheck SC2015 and exclude eval fixtures from CI pytest * Run eval self-tests under uv so `make check` survives the python3 shim `eval-self-tests` discovers harnesses repo-wide, and all three it finds today pipe a script to `python3`: property-based-testing's run.sh and effectiveness.sh, and writing-lean-proofs' run.sh. On any machine with the modern-python plugin installed, its `python3` shim rejects those calls and `make check` fails for reasons that have nothing to do with the code under test. That is the trap #207 documents, and the reason `shell-suites` is deliberately kept out of `check`. Excluding a second target is the wrong answer here — these self-tests are free and they are what makes an eval result trustworthy — so run them under `uv run --no-project`, which puts a real interpreter ahead of the shim on PATH. Harnesses should still call uv themselves. The wrapper only applies inside `make check`, and the real sweeps are invoked by hand. * Move evals-extra out of the skill directory to the plugin root `evals/` already sits at the plugin root; `evals-extra/` sat inside `skills/property-based-testing/`, so every user of the plugin shipped 900 lines of bash, a `requirements.txt` naming hypothesis, and a fixture whose tests are broken on purpose — inside the one directory the model reads guidance from. run.sh's own header notes the hazard of the model finding skill files by filesystem exploration; this removes the material it would find. Nothing in the machinery cares which of the two locations it is in: the Makefile, the CI pytest exclusion, ruff's per-file ignores and the plugin validator all match on an `evals*` prefix anywhere under `plugins/`. Verified by running eval-self-tests and validate from the new layout. `plugin_root` in both harnesses walks up one directory now instead of three. * Re-execute run.sh by path in its own self-test instead of $0 The four end-to-end assertions run the whole sweep in a subprocess by invoking `"$0"`. That is only a runnable command when the caller passed a path with a slash in it: `bash run.sh --self-test` from this directory sets `$0` to `run.sh`, which is not on PATH, so all four exited 127 while the eleven unit assertions passed. It worked by accident because the Makefile and the README both happen to pass a path. Use `$here/run.sh`, which is invocation-independent. * Report a detector that could not run as a failure, not as a non-trigger `skill_invoked` returned an exit status, and both "the model did not call the skill" and "python3 blew up" came back as 1. `check_triggered` then fell through its ladder to `no` — the one verdict the aggregator treats as a measurement. So a broken interpreter did not fail the sweep; it scored every positive session as a clean negative, and 45 sessions and $36 came back looking like a recall regression. This is not hypothetical. The modern-python plugin's `python3` shim rejects the call (#207), which is how it was found: the self-test's "skill invoked -> yes" case returned `no`. The verdict is now a printed token — `yes`, `no`, or `error:<detail>` — because an exit status cannot carry the distinction: 1 is both python3's own failure status and the detector's "not found". A healthy session whose detector failed lands in a new `crash:detector` branch, which invalidates the sweep like any other failed session and puts the interpreter's message in the NOTE column. Every python3 call in the script goes through `uv run --no-project` for the same reason, so the harness also runs correctly by hand under the shim rather than only under `make check`. That adds a uv dependency, guarded at startup alongside the existing claude CLI check. Pinned by a new assertion that points the detector at a nonexistent interpreter and asserts `crash:detector`, not `no`. 16 assertions, was 15. * Refuse to grade an effectiveness run whose patch never applied `grade()` diffs the failing tests before and after replacing canonicalize_url with an identity stub. It called `patch_codec` and never checked the result, on the assumption that `set -e` would abort — but errexit does not propagate out of a function into the command substitution `got="$(grade "$d")"` runs in. So a failed patch left the "after" suite running against the UNPATCHED fixture: before and after come out identical, nothing moves, and a suite that genuinely caught the defect is written down as `part` — "suite fails, but not on this defect". That also silently disarmed the drift guard inside patch_codec, whose entire job is to refuse to grade in exactly this situation. Its message went to stderr and the grade continued. A failed patch is now ERR, and the fixture is restored from the backup on that path. patch_codec goes through `uv run --no-project` like the rest of the repo, so the shim (#207) is not what triggers it either. Pinned by a new assertion that hands the grader a fixture with no canonicalize_url to replace and asserts ERR rather than a grade. 4 assertions, was 3. * Refuse a multi-level effort sweep while SKILL.md pins `effort:` A skill's `effort:` frontmatter overrides the session level, so the `--effort` that effectiveness.sh passes each session is ignored the moment the skill loads. SKILL.md pins `effort: low`, so the default `EFFORTS="low medium high"` ran three sessions at `low` and printed the level each one *asked* for in the EFFORT column. Nothing in the output gives that away. Three rows agreeing is also what a healthy sweep looks like when effort genuinely does not matter, which is the conclusion the table invites — and the conclusion that keeps the pin at `low` forever. It is the same shape as the failures this suite already guards against: a checker that has quietly stopped varying its independent variable reports a clean result. It also means the recorded sweep cannot be reproduced against the plugin as shipped. Either that sweep predates the pin, or it was already this artefact; there is no third reading. That matters because re-running an effort sweep is what AGENTS.md asks for whenever the model changes, and this is the check that would have been re-run. Requesting the pinned level alone is still allowed — that scores the shipped configuration and the label is true. NOPLUGIN loads no skill, so nothing overrides and a sweep there is honest. Anything else with a pin present exits 2 and names both ways forward. The `q` in the sed matters: a second `effort:` line anywhere in the file, a fenced YAML example say, would otherwise make `$pinned` multi-line and refuse even a correct `EFFORTS=low`. Both READMEs documented a bare `./evals-extra/effectiveness.sh`, which now exits 2, so they move to `EFFORTS=low` here rather than in a follow-up that would leave the docs describing a failing command in between. Known cost, not fixed here: `EFFORTS=low` is one session, where the broken sweep at least sampled the same configuration three times. run.sh:20-22 rejects n=1 for the sibling metric on the grounds that invocation is stochastic. Fixing it means a repetition knob or a different default — a change to how the eval samples rather than to what it reports, so it is left to the author. Pinned by two new assertions: a pinned skill refuses `low medium high`, and allows `low`. 6 assertions, was 4. * Check for the claude CLI below run.sh's --self-test dispatch, not above it The preflight sat at the top of the script, so it ran before the `--self-test` branch and the self-test exited 2 on any machine without Claude Code installed, having run zero of its sixteen assertions: $ env PATH=/usr/bin:/bin bash run.sh --self-test claude CLI not found: claude `claude_bin` is only swapped for the stub inside `self_test()` itself, which is far too late to matter. So the guarantee in the comment above that function — "uses a stub binary, so it costs nothing and can run in CI" — was false, and `make eval-self-tests`, and therefore `make check`, broke for any contributor without the CLI. AGENTS.md draws exactly this line for the two loadability checks: they run in CI rather than in `make check` precisely because needing the Claude Code CLI is not a reasonable local prerequisite. A self-test that claims to be free must not smuggle that requirement back in. The uv check stays above the dispatch, because the self-test genuinely needs it: the detectors run through `uv run --no-project python3`, and uv is already a prerequisite everywhere else in the repo. effectiveness.sh had this split right and was the template. Verified with `claude` absent from PATH and uv plus GNU coreutils present: all 17 assertions pass. With neither present it now stops on uv, which is the honest dependency rather than a borrowed one. Worth knowing and not fixed here: `timeout(1)` is still an undeclared dependency of both a real sweep and the self-test, and it does not exist on a stock macOS PATH. Absent, the child-sweep assertions fail with 127. CI is Linux so it is covered there, and the bash-3.2 accommodation at the end of the self-test suggests stock macOS is meant to work, so it wants either a preflight alongside uv or a documented prerequisite. Pinned by a new assertion that runs a real sweep with a nonexistent CLAUDE_BIN and asserts exit 2. The risk on the next edit is the check being deleted rather than moved, which would turn a typo'd CLAUDE_BIN into 45 crash:rc127 sessions instead of an immediate refusal. 17 assertions, was 16. * Fix sed issue on BSD * Restore refactoring.md --------- Co-authored-by: kz-tob <kara.zaffarano@trailofbits.com> Co-authored-by: Emilio López <emilio.lopez@trailofbits.com>
Property-Based Testing
Write, review, and triage property-based tests — Hypothesis, fast-check, proptest, and Echidna or Medusa for Solidity invariants.
Installation
This plugin is part of the Trail of Bits Skills marketplace.
Via Marketplace (Recommended)
/plugin marketplace add trailofbits/skills
/plugin menu
Then select the property-based-testing plugin to install.
Manual Installation
/plugin install trailofbits/skills/plugins/property-based-testing
What's Included
This plugin provides a skill covering three jobs: writing property tests, reviewing existing ones for tests that assert nothing, and triaging a shrunk counterexample into a wrong property, an ambiguous spec, or a real bug. It recognises these shapes:
- Serialization pairs: encode/decode, serialize/deserialize, toJSON/fromJSON
- Parsers: URL parsing, config parsing, protocol parsing
- Normalization: normalize, sanitize, clean, canonicalize
- Validators: is_valid, validate, check_*
- Data structures: Custom collections with add/remove/get operations
- Mathematical/algorithmic: Pure functions, sorting, ordering
- Smart contracts: Solidity/Vyper contracts, token operations, state invariants
Supported Languages
- Python (Hypothesis)
- JavaScript/TypeScript (fast-check)
- Rust (proptest, quickcheck)
- Go (rapid, gopter)
- Java (jqwik)
- Scala (ScalaCheck)
- Solidity/Vyper (Echidna, Medusa)
- And many more...
See skills/property-based-testing/references/libraries.md for the complete list.
Evals
The skill ships three evals, because "the skill fires" and "the skill helps" are different claims and only the second one matters to a user.
./evals-extra/run.sh # trigger rate against labelled queries
EFFORTS=low ./evals-extra/effectiveness.sh # does the generated suite catch a real bug?
Both spend real API budget — run.sh runs one session per query per run, 45 at its
defaults (measured at 51.9 min and $36.50 at JOBS=4), and effectiveness.sh is 3.
Neither runs in CI for that reason; they are what you run when you change the
description or the guidance. RUNS=1 ./evals-extra/run.sh is the cheap smoke test.
Both harnesses ship a --self-test that costs nothing and runs in make check, so a
harness that has stopped discriminating fails the build instead of reporting a green
skill forever. run.sh --self-test drives the classifier with a stub binary and
asserts, among other things, that a crashed session invalidates the sweep rather than
being absorbed by the pass threshold.
effectiveness.sh grades by running the generated tests against a fixture with a
known defect, not by reading what the model said about its own work. Both scripts
exit non-zero when they inspect nothing, so a broken harness fails loudly instead of
reporting a clean pass.
See skills/property-based-testing/README.md for what the queries cover and how to
run the no-skill baseline.
evals/ — the ablation suite
The third eval is not a shell harness. evals/ holds claude plugin eval cases, run
from the plugin root, and every case runs twice — once with the plugin loaded and once
without — so the number it reports is Δ against the unaided model rather than a raw
score. A skill that scores full marks in both arms is spending context and buying
nothing, and that is the failure this suite exists to catch.
claude plugin eval . --ablation with-without --judge-model sonnet --allow-tools Write
Two operational notes, both learned the hard way:
- It needs
ANTHROPIC_API_KEY. Each case runs in a sandboxed config dir, so an interactive login is not visible to it and a subscription OAuth token is ignored. Without the key every session dies instantly asNot logged in, costs a cent, and the judge then grades that string — which scores zero and looks like a real result. CheckapiKeySourcein a trace before believing any number. --allow-tools Writeis load-bearing, not convenience.03's strongest grader fires when the model creates arequirements.txt; denyWriteand it can never create one, so the grader passes for free.
Measured on opus, 3 runs per arm, ~$4.30 per full sweep:
| case | fires | with | without | Δ |
|---|---|---|---|---|
02-neg-cargo-fuzz-coverage |
no | 1.00 | 1.00 | 0.00 |
03-dependency-is-users-call |
yes | 0.50 | 0.00 | +0.50 |
02 is the over-trigger guard — coverage-guided fuzzing is on the description's
exclusion list, and the skill did not fire in any of the three with-plugin runs. Δ0 is
the correct result for a negative.
03 measures whether the skill leaves a new test dependency to the user. Unaided
opus wrote a requirements.txt in 3 of 3 runs; with the skill loaded it did so in 2
of 3, so the behaviour is improved and not fixed. The grader carrying that Δ is a regex
over the run's created-files list, so it cannot be talked round by a persuasive answer
the way an LLM judge can.
What this suite does not establish is that the skill helps you write better property
tests. Two cases is below the four-positive floor worth trusting, and three flows are
still unmeasured: reviewing existing tests (one 3-run sample suggested Δ+0.17, never
confirmed), declining PBT for code with no algebraic shape (three fixtures attempted,
opus found a legitimate property in all three — including a header-injection bug, so
it was right to), and triage, which is the gap skills/property-based-testing/README.md
already documents.
Costs real money per run, so like the harnesses above it is a manual check and does not
run in CI. evals/results/ is gitignored — those are run artifacts, not source.