Verifies local security patch commits using scoped case execution and three-arm proof methodologies.
- GitHub stars
- 8,136
- Files
- 1
- Last commit
- Nov 11, 2026
- License
- CC-BY-SA-4.0
- Allowed tools
- —
What does the prove-patch skill do?
prove-patch verifies local security patch commits using scoped case execution and three-arm proof methodologies.
Summary generated from the skill's SKILL.md.
About the prove-patch skill
Verifying local security patch commits through rigorous scoped case execution and three-arm proof methodologies is the primary function of this skill. It is designed for developers or security agents who need to independently validate that a specific patch commit fixes a vulnerability without introducing regressions. The process requires a baseline commit, the final patch commit, a declared repair scope, and an unchanged reproduction package.
An agent should load this skill when it needs to generate a formal proof of a fix. The tool executes planned inputs on both clean baseline and patched trees using a consistent harness to ensure results are comparable. It relies on the three-arm helper script to confirm that the baseline fails, the patch passes, and a complete baseline revert fails again. All execution data, including stdout, stderr, and exit statuses, are stored as receipts. The final output is a structured prove.json file and a manifest that undergoes validation to ensure no evidence gaps or findings exist.
What an agent can do with it
- 1Validate a security fixVerify that a specific commit correctly addresses a vulnerability by running scoped cases on both baseline and patched trees.
- 2Perform three-arm proof verificationConfirm the integrity of a patch by ensuring the baseline fails, the patch passes, and a reverted baseline fails again.
- 3Run project-specific regression checksExecute focused tests and security checks on the patched code to ensure no existing functionality is broken.
- 4Generate formal proof manifestsCreate a validated record of the entire proof attempt including all execution receipts and build identities.
Written from the skill's SKILL.md. Every use case is checked against a quote from it.
How to install the prove-patch skill
Each command copies the skill folder into the client's skills directory. Restart the client or start a new session to load it.Install the prove-patch skill in Plugin
/plugin marketplace add trailofbits/skills /plugin install patching-bugs@trailofbits
Install the prove-patch skill in Claude Code
~/.claude/skills/prove-patch/SKILL.md
$ npx degit trailofbits/skills/plugins/patching-bugs/skills/prove-patch ~/.claude/skills/prove-patchInstall the prove-patch skill in Claude Code (project)
.claude/skills/prove-patch/SKILL.md
$ npx degit trailofbits/skills/plugins/patching-bugs/skills/prove-patch .claude/skills/prove-patchInstall the prove-patch skill in Codex
~/.agents/skills/prove-patch/SKILL.md
$ npx degit trailofbits/skills/plugins/patching-bugs/skills/prove-patch ~/.agents/skills/prove-patchInstall the prove-patch skill in Gemini CLI
~/.gemini/skills/prove-patch/SKILL.md
$ npx degit trailofbits/skills/plugins/patching-bugs/skills/prove-patch ~/.gemini/skills/prove-patchInstall the prove-patch skill in Claude.ai
npx degit trailofbits/skills/plugins/patching-bugs/skills/prove-patch prove-patch && zip -r prove-patch.zip prove-patch # claude.ai → Customize → Skills → + → Create skill → Upload a skill → prove-patch.zip
Automated checks
Ran Nov 14, 2026Full report →Passed our automated checks. That is not a security audit: read the scripts before you let an agent run them. How checks work
- Source repository linked and reachabletrailofbits/skills/plugins/patching-bugs/skills/prove-patch is public and reachablegithub.com/trailofbits/skills/tree/HEAD/plugins/patching-bug ↗Pass
- Open source license (OSI)CC-BY-SA-4.0 is not OSI-approvedspdx.org/licenses/CC-BY-SA-4.0.html ↗Finding
- Commit or release in the last yearLast commit 2026-11-11github.com/trailofbits/skills/commits ↗Pass
- No download-and-run or credential theft in scriptsNo scripts in the skill folderPass
- No hidden instructions in SKILL.mdNo override phrases, safeguard switches, credential requests or hidden charactersgithub.com/trailofbits/skills/blob/HEAD/plugins/patching-bug ↗Pass
- Pre-approved tools are scopedNo pre-approved tools; the agent asks before using onegithub.com/trailofbits/skills/blob/HEAD/plugins/patching-bug ↗Pass
SKILL.md
View on GitHubProve Patch
Use the original baseline, final patch commit, declared repair_scope, and unchanged
reproduction package. Read the record contract. Do not
edit the patch or validate an uncommitted tree. Return failures for a new attempt.
Before target commands, follow its project guidance.
- Review the scoped cases and the patch without the patcher's conclusion. Execute
each planned input on clean baseline and patched trees with the same retained
harness source and command. The harness must print exactly one
PATCH_CASE {"input": ..., "actual": ...}from the exercised input and observed result, then printPATCH_REACHEDas its final stdout line immediately before the assertion. Representatives must fail on the baseline and pass on the patch. Valid controls must pass on both. Keep the baseline and patched stdout, stderr, exit status, elapsed time, command, and harness source underreceipts/. A timeout, setup failure, missing marker, mismatched input, or ambiguous observation is an evidence gap. A trustworthy patched failure is a finding. Never relabel a gap as a pass. - Run relevant project checks on the patch and retain the same raw receipts. Use baseline comparison for behavior checks and to attribute failed project checks; a passing patched suite may omit a baseline run. Include focused tests, regression and security checks where relevant. Record specific unproven limits; an empty list leaves the result inconclusive.
- Run the three-arm helper with the proof-type recipe in
the record contract,
reproduce.baseline_commit, and finalpatch_commit. Require the baseline to fail, patch to pass, and complete baseline revert to fail again. Requirereceipts/source.jsonto identify the pinned commits and the reverted tree to equal the original baseline tree. Require the type's build identity result. Retain all source-tree, build, and execution receipts. - Write
prove.jsonand a final manifest covering it and every receipt. Runuv run --no-project <script> manifest <prove-attempt-dir>and thenuv run --no-project <script> check <run-dir>with the validator. Independently inspect the native proof assessment and raw receipts before reporting a result. A complete proof has no findings or gaps. Return exact failures and receipt paths to the orchestrator.
{
"schema_version": 2,
"attempt": 1,
"failure_type": "runtime",
"baseline_commit": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa",
"patch_commit": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb",
"reverted": "pass",
"build_identity": "pass",
"hashes": {
"baseline": "1111111111111111111111111111111111111111111111111111111111111111",
"patched": "2222222222222222222222222222222222222222222222222222222222222222",
"reverted": "1111111111111111111111111111111111111111111111111111111111111111"
},
"reverted_hash_note": null,
"cases": [{
"check_id": "reported-input",
"argv": ["python", "receipts/case.py", "reported-input"],
"source": "receipts/case.py",
"runs": {
"baseline": {"exit_code": 1, "elapsed_ms": 15, "stdout": "receipts/case-base.stdout", "stderr": "receipts/case-base.stderr"},
"patched": {"exit_code": 0, "elapsed_ms": 14, "stdout": "receipts/case-patched.stdout", "stderr": "receipts/case-patched.stderr"}
}
}],
"project_checks": [{
"check_id": "focused-suite",
"kind": "suite",
"argv": ["pytest", "tests/test_upload.py"],
"baseline": null,
"patched": {"exit_code": 0, "elapsed_ms": 860, "stdout": "receipts/suite.stdout", "stderr": "receipts/suite.stderr"}
}],
"unproven": ["Inputs outside the declared boundary were not assessed."],
"agent": "prover-1"
}
For a bounded class, include at least two distinct failing representatives and a
valid control. The record must cover every planned case by unique check_id.
Use the same harness and command on both commits; do not reveal the side to the
harness or change expectations by side. Review the selected cases for relevance;
retained receipts establish only what those cases exercised.
Files in this skill
1prove-patch skill questions
How do I install the prove-patch skill in Claude Code?
Run npx degit trailofbits/skills/plugins/patching-bugs/skills/prove-patch ~/.claude/skills/prove-patch. Claude Code loads skills from ~/.claude/skills (all projects) or .claude/skills (one project) and uses a skill when its description matches the task.
Which clients can use the prove-patch skill?
Any client that reads the Agent Skills format: Claude Code, Codex, Gemini CLI and claude.ai (upload as a ZIP). Scripts in the skill run only where the client allows code execution.
What is required to perform a three-arm proof?
The process requires the baseline commit, the final patch commit, and a complete baseline revert to ensure the original state is restored.
What constitutes an evidence gap during the verification process?
An evidence gap occurs if there is a timeout, a setup failure, a missing marker, mismatched input, or an ambiguous observation.
How should the harness output be formatted for scoped cases?
The harness must print exactly one PATCH_CASE entry containing the input and actual result, followed immediately by PATCH_REACHED before the assertion.