Agentic Vulnerability Discovery Patch-Proof Replay

Patch-proof language needs more than a claim

"Found and fixed a security bug" is easy to type and hard to check, standing equally for a tested repair, a patch never run, a false positive, or an empty benchmark number. An agent that says it "found and fixed a security bug" is making a claim that is easy to type and hard to check. The phrase can stand for a real, tested repair. It can also stand for a patch that was never run, a false positive promoted to a finding, or a benchmark number with nothing behind it.

Seven evidence stages must agree

It breaks the claim into a synthetic evidence chain, from target through issue, trace, patch, test, witness, and verifier record, and checks the pieces line up before allowing patch-proof language. This component takes that claim apart into an inspectable chain of synthetic evidence and checks that the pieces line up before any patch-proof language is allowed. The chain runs from a made-up target, through a suspected issue, a trace that backs it, an abstract exploitability reference, a patch, a regression test, an executable witness, and a verifier record. Nothing in the chain is a real target, exploit, payload, or account secret. The result record says whether the declared chain holds together, and carries no attack material.

Synthetic replay grants no security authority

It is a synthetic, metadata-only replay, not live security work, that runs against no real system, judges no bug or fix as genuine, and produces no benchmark claims. The code lives in src/microcosm_core/organs/agentic_vulnerability_discovery_patch_proof_replay.py. It is a synthetic, metadata-only replay, not live security work. It does not run against real systems, does not judge whether the bug or fix is genuine, and does not produce a benchmark claims.

Purpose

Why two recompute checks exist

A summary can hide the absence of the work it summarises, so instead of trusting the fixture's labels two checks recompute the thing the fixture claims. The problem is that "found and fixed" is a summary, and a summary can hide the absence of the work it summarises. A loose check that only reads the fixture's own labels would pass a chain that asserts a green result without the work behind it. Two checks here refuse that by recomputing the thing the fixture claims, rather than trusting the field.

Recompute one: running the regression witnesses

The first recompute runs each witness's mini-target twice, unpatched and patched, and rejects any witness whose declared pre and post outputs do not match the computed ones. The first recompute is on the executable regression witnesses. Each witness names one of three small public mini-targets: a webhook redirect allowlist, a notebook log redactor, and a scheduler path normaliser. The validator runs that function twice, once unpatched and once patched, and compares its own computed outputs against the expected_pre_patch and expected_post_patch values the fixture declared. A witness whose declared output does not match the computed output is rejected.

Recompute two: the verifier verdict

The second recompute derives each verifier verdict from the joined hypothesis, proof, patch, test, and witness evidence, and requires the filename to match rather than trusting the record's own label. The second recompute is on the verifier records. Each record's pass or false_positive verdict is recomputed from the joined hypothesis, proof, patch, test, and witness evidence, and the record's filename must match that recomputed verdict. The record's own label is not taken on trust.

How it works

_build_result orchestrates the validators

_build_result loads inputs and policy, scans every path for secrets, builds the public trace, then runs one validator per evidence kind, passing only when every check and negative case clears. _build_result is the orchestrator. It loads the fixture inputs, loads the forbidden-class policy, runs a secret-exclusion scan over every input path, builds the public agent-execution trace, then runs one validator per evidence kind in dependency order. Each validator returns a status, exported rows, and a list of findings. A result reaches pass only when there are no missing negative cases, the secret scan has zero blocking hits, the public trace status is pass, every positive validator returned pass, and, for the exported bundle, the source-module manifest returned pass.

Each validator joins against the preceding stage

The validators form an ordered evidence join in which every stage resolves its rows against the stage immediately before it. The validators form a join, not a scanner. Each stage resolves its rows against the stage before it.

Three mini-target engines run both ways

Three MINI_TARGETS engines each take a patched flag: unpatched they leak or over-allow, patched they close the hole, and running both forms confirms a declared fails-before-passes-after test. The three mini-target engines are _webhook_redirect_allowlist, _notebook_log_redaction, and _scheduler_path_normalization, registered in MINI_TARGETS. Each takes an input and a patched flag. Unpatched, the webhook engine allows any redirect, the notebook engine leaks its sensitive refs, and the scheduler engine accepts a path that escapes the workspace. Patched, each closes its hole. Running both forms is what lets validate_executable_regression_witnesses confirm that a declared "fails before, passes after" test actually does.

Strict join order blocks broken chains

The join is strict: an unresolved hypothesis, a patch missing its proof or diff, a patch with no test, or a promoted false positive is each blocked. The join order is strict. A hypothesis that does not resolve to a synthetic target is blocked. A patch-required hypothesis missing either an exploitability proof or a metadata-only patch diff is blocked. A patch with no paired regression test is blocked. A false positive promoted to a finding is blocked, because validate_verifier_receipts will not recompute its verdict as pass.

flowchart TD targets["synthetic targets"] hypotheses["issue hypotheses"] traces["trace evidence"] proofs["exploitability proofs"] patches["patch diffs"] tests["regression tests"] witnesses["executable witnesses run mini-target twice"] verifiers["verifier records recompute verdict"] status["result status"] targets --> hypotheses hypotheses --> traces hypotheses --> proofs hypotheses --> patches patches --> tests tests --> witnesses witnesses --> verifiers verifiers --> status

Two runtime modes, both metadata-only

run drives the fixture with negative cases on, run_patch_proof_bundle drives the exported bundle as the public example, and both write metadata-only records with source bodies kept behind manifest hashes. The runtime keeps two modes separate. run drives the first-wave fixture with negative cases on, so it must observe every expected overclaim failure. run_patch_proof_bundle drives the exported bundle as the public runtime example, so its expected negative cases can be empty while it still proves the source-body floor, the public trace, the digest checks, and the regression witnesses. Both write metadata-only result records. Copied source bodies stay behind source_module_manifest.json refs and hashes; the exported bundle carries nine digest-verified public source bodies.

Negative cases

Eight overclaims the runtime must trip

Eight EXPECTED_NEGATIVE_CASES overclaims must each trip a matching error code or the run is blocked, and _has_forbidden_key separately rejects any row carrying a forbidden field. The first-wave fixture includes eight negative cases, held in EXPECTED_NEGATIVE_CASES. Each one is an overclaim the runtime must trip, not a capability it offers: live_target_material, real_cve_exploitation, weaponized_payload_export, account secret material, network_exfiltration, exploit_instruction_steps, patch_without_tests, and benchmark_score_claim. validate_negative_cases records the matching error code for each, for example AGENTIC_VULN_PATCH_WITHOUT_TESTS when a patch claim arrives with no regression test. If any expected case goes unobserved, the run is blocked. Separately, _has_forbidden_key rejects any row that carries a forbidden field such as a raw exploit payload, a account secret value, or a live target URL.

Prior Art Grounding

Test-backed repair lineage from SWE-bench

The design borrows the accountability pattern of SWE-bench, SWE-agent, and security benchmarks like CyberSecEval 2 and SecCodePLT, requiring evidence to line up before patch-proof language, without importing live exploits. This component borrows an accountability pattern from agentic software-engineering and security-evaluation work that treats a code repair as an executable, test-backed claim rather than a prose claim. SWE-bench framed repository issue resolution as a task with real codebases and test-based patch evaluation, and SWE-agent made the agent-computer interface part of the repair loop. Security benchmarks such as CyberSecEval 2 and SecCodePLT motivate separating a secure-code or vulnerability claim from an uninspected generated patch. The borrowed idea is narrow: hypotheses, traces, patches, tests, and verifier records must line up before patch-proof language is allowed. It does not import live targets, CVE exploitation, weaponized payloads, or benchmark claims.

Validation Result record Path

Fixture output stays outside the system tree

The first-wave validator runs from the system root and writes its result record to a disposable path outside the working tree. Run the first-wave fixture validator from the system root and write its record outside the working tree:

Then run the exported bundle validator:

cd microcosm-substrate && PYTHONPATH=src ../repo-python -m microcosm_core.organs.agentic_vulnerability_discovery_patch_proof_replay \
  run-patch-proof-bundle \
  --input examples/agentic_vulnerability_discovery_patch_proof_replay/exported_patch_proof_bundle \
  --out /tmp/agentic_vulnerability_patch_proof_bundle_receipt \
  --card > /tmp/agentic_vulnerability_patch_proof_bundle_card.json

The focused regression test is:

PYTHONPATH=src ./repo-pytest \
  tests/test_agentic_vulnerability_discovery_patch_proof_replay.py

What a pass and the rejection tests prove

A pass means the whole join held with both recompute checks agreeing, a clean scan, and every negative case tripped, while rejection tests mutate the chain and require a blocked result. A pass means the whole join held: the synthetic chain resolved end to end, both recompute checks agreed with the fixture, the secret scan was clean, and every expected negative case tripped. The rejection tests in the same file mutate the chain, remove a regression test, tamper a witness, cross-wire a verifier record, or alter a source-module digest, and require a blocked result with a specific error code.