Generated banner for Prove Patch
Generated logo for Prove Patch

Prove Patch

Trail of BitsOfficialPublished by Trail of Bits

  • Skill
  • Review and audit
  • Security
  • CC-BY-SA-4.0
  • No issues found

From the author

Use when a local security patch commit needs independent scoped and three-arm proof.
— the description by Trail of Bits

AutoGineer summary

Written by AutoGineer from the skill’s own files, not by the author

The prove-patch skill provides a structured methodology for validating local security patch commits. It requires an independent, three-arm proof process that compares the baseline, the patched state, and a reverted state to ensure the fix is effective, reproducible, and does not introduce regressions. The process emphasizes strict evidence collection, requiring detailed receipts for all test executions, build identities, and source tree states to ensure the patch behaves exactly as expected under controlled conditions.

What it does

  • Executes scoped test cases against baseline and patched trees to verify fix effectiveness.
  • Performs a three-arm proof check to confirm baseline failure, patch success, and reverted failure.
  • Validates build identity and source tree consistency across all test states.
  • Generates a structured proof manifest and JSON record for auditability.
  • Requires independent inspection of raw receipts and native proof assessments.
  • Identifies evidence gaps and findings to prevent inconclusive or unverified results.

When to use it

  • When you need to independently verify a local security patch before deployment.
  • When a security fix requires a formal, evidence-backed proof of its effectiveness.
  • When you need to ensure that a patch does not negatively impact existing project functionality.
  • When you must provide a verifiable audit trail for a security-related code change.

Advantages

  • Ensures high confidence in security patches through rigorous three-arm verification.
  • Eliminates ambiguity by requiring raw receipts for every test execution.
  • Provides a standardized schema for documenting proof results and evidence.
  • Promotes reproducibility by enforcing strict baseline and revert checks.

Usage examples

“Verify the security patch for the recent buffer overflow vulnerability.”
The agent initiates the prove-patch workflow, running the baseline and patched trees through the required test harness, generating the necessary receipts, and producing a prove.json manifest for review.
“Audit the patch commit bbbb... for the authentication bypass.”
The agent performs the three-arm proof, verifying that the baseline fails, the patch passes, and the reverted tree returns to a failing state, while documenting all build and execution receipts.

Install

  1. Download the skill as a ZIP:

    https://autogineer.com/agent-skills/trailofbits/prove-patch/download
  2. Unzip it into the cross-client skills folder of your project:

    mkdir -p .agents/skills && unzip prove-patch.zip -d .agents/skills

Documentation by Trail of Bits

Prove 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.

  1. 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 print PATCH_REACHED as 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 under receipts/. 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.

  2. 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.

  3. Run the three-arm helper with the proof-type recipe in the record contract, reproduce.baseline_commit, and final patch_commit. Require the baseline to fail, patch to pass, and complete baseline revert to fail again. Require receipts/source.json to 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.

  4. Write prove.json and a final manifest covering it and every receipt. Run uv run --no-project <script> manifest <prove-attempt-dir> and then uv 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.

Prove record schema:

{
  "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

Requirements and compatibility

Works with: Claude Code, Claude apps, OpenAI Codex, GitHub Copilot, Cursor, Gemini CLI, Kiro, OpenCode, Goose, Amp, Roo Code, JetBrains Junie, Factory Droid, Devin (ex-Windsurf), Mistral Vibe, OpenHands, Letta

“Works with” means the tool reads the open Agent Skills format; a skill written for one tool may use features others lack.

Needs: Needs Python

Security

No issues found by our static scan· No issues found

A static scan is not a guarantee. Skills are third-party content: review a skill before you let an agent use it.

Attribution and licence

Published by
Trail of Bits
Publisher
Trail of Bits (Official)
Source
trailofbits/skills · plugins/patching-bugs/skills/prove-patch · commit e4dd0bb
Licence
Creative Commons Attribution-ShareAlike 4.0 International (redistribution allowed)
  • LICENSE (added by AutoGineer from LICENSE)
  • ATTRIBUTION.md (written by AutoGineer)
Synced

AutoGineer is not affiliated with or endorsed by Trail of Bits or Trail of Bits.

Download ZIP

The ZIP holds the skill’s files, its licence files and an ATTRIBUTION.md. Download prove-patch.zip