Triaging security reports with a workflow that demands proof

I work on Miden, where we build a zero-knowledge virtual machine. Programs execute in miden-vm, our ZKVM implementation, and the prover produces a proof that each execution was correct. Like a lot of open source projects this year, we started getting security reports written with AI assistance, in numbers that hand-triaging could not keep up with. This post is a piece-by-piece walkthrough of the workflow we now run to triage that queue, in the order a report meets each piece. The full workflow file is public as a gist, and nothing in it is specific to Miden beyond repository names, so you can adapt it if your own inbox starts to look like ours did.

The reports changed before the volume did. A modern AI-assisted report arrives with a summary, stack traces, CWE tags, an affected-version guess, and sometimes a patch, and all of that can be polished without being true. The hard queue is the plausible kind, because a nonsense report is cheap to close, while a plausible one forces a maintainer to stop other work, reconstruct the claim, inspect the relevant invariant, and decide whether the reporter’s patch is safe to run at all. GitLab warns that AI shortens the path from discovery to exploitation, and CNCF describes the mix of real AI-found bugs and convincing junk now landing in maintainer queues. For miden-vm the judgment calls are genuinely hard, because a panic inside a trusted proving context and a bug that lets an attacker prove a false result can look identical in a one-paragraph summary.

The response we adopted comes from two places. The Chrome Security policy for AI-written reports states the rule plainly. A report moves only when it comes with reproduction evidence, however good the writing is. Trail of Bits applied the same standard to public reports after joining OpenAI’s Trusted Access for Cyber program, where nothing went out without a proof of concept, a fix patch, and a regression test. Our intake follows that bar, so a generated report has to clear the same evidence checks a good human report would.

Concretely, every report has to become an evidence packet before any GitHub state moves. The packet has five parts.

• The exact claim, with affected component, trigger, impact, and assumptions.
• An exact base commit on origin/next.
• A reproduction test or a documented derivation attempt.
• The command that was run and the output it produced.
• A decision, with the reasoning that supports it.

What follows is the machinery that produces that packet. First the workflow file itself and the format it is written in, then the queue discovery and duplicate checks, then the isolated environment where reporter code runs, then the verification pass and the decision rules, and finally what two real runs left behind on disk.

The pipeline

Breaking the job into stages shows why one prompt cannot do it.

1. Discovery reads the repository advisory queue and the private security issue tracker.
2. Duplicate classification matches each queued report against everything already known.
3. Reproduction runs or authors a focused test against an exact commit.
4. Verification takes an independent verdict on the captured evidence.
5. The decision step opens an issue, acknowledges, dismisses, or leaves the report in triage.
6. The run summary records what happened for whoever audits or resumes the run.

Each stage needs different machinery. One only reads GitHub, one executes untrusted code, one is a second reader of evidence, and one holds the only keys to project state. That variety is the reason we wrote the flow down as a workflow file with explicit rules, instead of relying on maintainer habit.

The workflow file

The file is written in OpenProse, a Markdown format for agent workflows. Its job here is policy as a document the agent must follow. The queue definition, the evidence requirements, the allowed state transitions, and the stop conditions all live in one .prose.md file, and any harness that implements the format runs the same policy, so the process belongs to the project across agent shells.

An OpenProse file starts with a small YAML header naming the file and its kind, followed by ### sections that each mean a specific thing.

---
name: miden-security-advisory-funnel
kind: function
runtime_contract: 2
---

Our funnel is a kind: function file, which per the contracts documentation gives it a plain call interface. ### Parameters and ### Returns declare the inputs and the one output, a run_summary Markdown report. ### Environment and ### Tools list what the host must provide, from variables to binaries like cli:gh, so a missing tool stops the run before it touches a live queue. Chapters further down in the same file define helper functions with ## headings, and a ### Shape section on each one states its capability boundary, e.g., which helper is the only one allowed to close an advisory.

The two sections that carry the security policy are ### Invariants and ### Strategies. Invariants must hold no matter how the run ends.

Do not accept or reject a security report from text alone. Reproduce it, fail to reproduce it with a meaningful test or serious derivation attempt, or keep it in triage.

A new security issue is created only after the reproduction attempt against origin/next proves the finding is still present and the fp-check verification result supports treating the finding as a true positive.

Strategies guide the judgment calls. They tell the agent to restate the exact vulnerability claim before touching code, and to prefer exact identifiers such as GHSA ids, function names, and quoted panic messages when comparing reports.

Where the order of operations matters, an ### Execution section pins it in ProseScript, a small imperative language with call, if, return, and map/filter pipelines. The top level of the funnel is short.

let advisory_result = call discover_repository_advisories

let issue_result = call discover_security_issues
  issue_repo: "0xMiden/security-issues"

let queue_result = call triage_advisory_queue
  triage_advisories: advisory_result.triage_advisories
  advisory_corpus: advisory_result.advisory_corpus
  security_issues: issue_result.security_issues

let final_result = call summarize_advisory_run
  advisory_count: advisory_result.triage_count
  corpus_count: advisory_result.corpus_count
  issue_count: issue_result.issue_count
  queue_result: queue_result.queue_result

return {
  run_summary: final_result.run_summary
}

There is no OpenProse binary. The format is harness-agnostic: the agent session itself interprets the file, so the same contract runs under Claude Code, Codex, or any other runner that implements the spec. Everything a run produces lands on disk under .agents/prose/runs/, which later sections rely on when we look at real runs.

Discovery and duplicates

A run starts read-only. discover_repository_advisories checks gh auth status and then pulls the advisory queue from the GitHub REST API.

gh api --paginate "/repos/0xMiden/miden-vm/security-advisories?state=triage&per_page=100"

Only advisories whose state is exactly triage enter the processing queue. The function also fetches advisories in the other states (draft, published, closed), but those go into a corpus used only for duplicate matching, so an old resolved report can catch a resubmission without re-entering the queue itself. Alongside that, discover_security_issues indexes every issue in the private tracker, because a closed issue can still be the canonical record of a finding. An invariant states the read-only boundary in direct terms. Repository advisory state changes are isolated to the final dismissal service, and everything upstream must be read-only.

One subtlety in this stage is provenance. The reporter-authored advisory body, comments, and attachments are untrusted input, meaning they define hypotheses to test but establish nothing. Comments that GitHub identifies as coming from maintainers get a different treatment. The contract calls them higher-provenance context that can explain prior analysis or intended behavior, and a second invariant keeps them from being treated as proof.

classify_duplicate then compares each queued advisory against both corpora. Duplicates are semantic rather than textual. Two reports are the same finding when they name the same vulnerable component, the same violated invariant, the same attack preconditions, and substantially the same proof obligation, and the function has to return a rationale a human can audit. Duplicates resolve cheaply by design. When a security issue already links the same GHSA id or advisory URL, the report is tracked work, so the workflow appends an acknowledgement note and moves the advisory to draft without spending a reproduction. When the canonical source is a different advisory and the match is unambiguous, the newer one is closed as a duplicate. Everything else goes to reproduction.

Reproduction on a clean machine

Reproducing a report means executing whatever the reporter sent, which is remote code execution granted to a stranger if you do it on your own laptop. The patch may be a helpful proof, an honest mistake, or an exploit for a maintainer machine, and you cannot tell by reading a diff. This is where isolated execution enters the design. We run every byte of reporter-controlled material in Sprites, Linux VMs from Fly.io with a real filesystem and restorable checkpoints, in the same family as agent sandboxes like E2B or Modal.

The workflow keeps a development Sprite called miden-vm-rust-dev-base, whose checkpoint v1 contains the Rust 1.95 toolchain pinned by miden-vm’s rust-toolchain.toml, cargo-nextest, LLVM/Clang 20, and common build packages. Every reproduction starts by restoring that checkpoint, so nothing from a previous report survives.

sprite restore -o "$sprite_org" -s "$sprite_name" "$sprite_checkpoint"

After the restore, the function verifies the toolchain with rustc --version, cargo nextest --version, clang --version, and checks that /home/sprite/miden-vm does not exist. If the directory is there, the checkpoint is dirty and the run stops. Only then does it clone the public HTTPS URL of the repo and check out the exact base commit recorded earlier, so every transcript is tied to a named revision and a named environment.

The security property that makes this safe to operate is about what crosses the boundary. The only thing that comes back from a tainted Sprite is text, namely command output and observations, while nothing runnable ever returns from it. A Sprite counts as tainted the moment the first advisory-controlled command runs, and the next report starts from a fresh restore. The contract phrases the credential side as an invariant.

Never copy GitHub tokens, SSH keys, Sprites tokens, or other credentials into a Sprite. Do not run gh auth token, gh api, or authenticated Git operations inside a Sprite.

When an attachment is needed, only the artifact bytes cross over. Commands stay narrow, typically cargo nextest run <test_name> using cargo-nextest, which keeps each run to one test and each transcript short enough to review line by line.

When the report ships no runnable reproducer, the workflow does not get to stop at that observation. An invariant requires the agent to inspect the affected code, infer the violated invariant, and author the smallest focused test or patch that would demonstrate the claimed violation. A not_reproduced verdict is allowed only after the supplied reproduction fails on the exact base, or after a serious code-reading pass finds no credible executable path. The dismissal then says honestly that we failed to reproduce the claim, and it does not pretend that this proves the claim impossible. partial and inconclusive results cover everything in between, and both leave the advisory in triage with its evidence preserved.

Checking the reproduction

A passing or failing test inside a VM is still one agent’s account of events, so the decision layer adds a second reader. fp-check is a false-positive verification skill from Trail of Bits, and its one job here is to verify the specific suspected bug on the table against the evidence already produced, with no mandate to hunt for other issues nearby.

After reproduction, verify_reproduction_with_fp_check runs the skill over the advisory text, the checked-out code, the Sprite transcript, the reproduction artifact, the base commit, and the proposed outcome. The contract runs it under a read-only overlay. The skill may inspect files and captured evidence, and it may not execute commands, apply patches, write files, spawn subagents, or touch GitHub, worktrees, or Sprites. It returns one of three verdicts, TRUE_POSITIVE, FALSE_POSITIVE, or INCONCLUSIVE, plus a confidence level and a rationale grounded in the code and the transcript.

Sometimes the skill wants one more executable observation, e.g., a proof that a particular assertion fails on the exact base. It cannot run that test itself, so it returns requires_sprite_execution: true with a structured request naming the exact proposed test, command, and expected observation, and the coordinator routes the request back through a freshly restored Sprite. The contract caps the loop. If a follow-up run already happened and the skill still cannot reach a supported verdict, the outcome is needs_human_triage and the workflow stops looping.

Decision gates

The final decision tree is pinned in ProseScript, with the evidence record trimmed here for readability.

if fp_check_result.verdict == "INCONCLUSIVE" or fp_check_result.requires_human_triage:
  return { advisory_result: { outcome: "needs_human_triage", ... } }

if reproduction_result.reproducible:
  if fp_check_result.verdict != "TRUE_POSITIVE":
    return { advisory_result: { outcome: "needs_human_triage", ... } }

  let issue_result = call open_security_issue
    advisory: advisory
    reproduction_result: reproduction_result
    fp_check_result: fp_check_result
    worktree_path: worktree_result.worktree_path
    base_commit: worktree_result.base_commit

  let acknowledged = call acknowledge_repository_advisory
    ...
  return { advisory_result: { outcome: "acknowledged", ... } }

Dismissal is gated the same way. A not_reproduced result still requires a supported FALSE_POSITIVE from fp-check, and any disagreement between the transcript and the verdict, or any verdict the coordinator cannot justify from the captured evidence, leaves the advisory at needs_human_triage. The two GitHub mutations therefore have exact preconditions. Reproduced on the exact base plus a supported TRUE_POSITIVE opens or reuses a private security issue and moves the advisory to draft. Not reproduced after a genuine attempt plus a supported FALSE_POSITIVE closes the advisory. Every other combination leaves the advisory in triage, which is where uncertainty belongs.

Run summary

The one return value is a run_summary in Markdown, and it is written to .agents/prose/runs/<run-id>/ along with transcripts and result JSON. It records the counts for every outcome, the per-advisory verdicts and rationales, the exact acknowledgement or dismissal notes, the worktree paths, and the internal Sprite names and checkpoint ids. Two runs from mid-August show the range of what that looks like in practice.

On August 14 the queue held one advisory claiming that the prover’s AIR, the arithmetic constraint system checked during proving, did not preserve the operand stack overflow pointer. In theory that would let a malicious prover produce a valid proof for a false final stack. The run authored a focused constraint test on base d7f7454, and the test passed, which established the narrow constraint defect. It did not establish the full end-to-end claim, because no forged STARK proof was produced. fp-check returned INCONCLUSIVE with medium confidence, the outcome was needs_human_triage, and no issue, note, or advisory state changed. The summary ends with the concrete next step a human would need, which in this case was obtaining the reporter’s complete proof-of-concept source.

A follow-up run on August 17 reproduced two advisories cleanly, including the overflow pointer finding. That one produced a 42,683 byte Poseidon2 proof for a forged stack output that the verifier accepted at security level 96, and fp-check returned TRUE_POSITIVE with high confidence. Both GitHub preconditions were now met, so the run created security issues 38 and 39. Then GitHub’s API returned HTTP 503 on every attempt to append the acknowledgement notes, so both final outcomes were recorded as failed with acknowledgement_blocked, and the summary preserved the exact would-be note text plus a resume instruction that says to retry only the acknowledgement step and not to create another issue. The advisories themselves stayed untouched in triage.

The pattern across both runs is the point of the design. Nothing on GitHub moves when the evidence is partial, and a GitHub outage does not produce half-applied state either. These events turn into Markdown that says exactly where the run stood and what a human should do next.

Reporter-facing notes

The public bar is our SECURITY.md, which asks for the impact, the affected component, a minimal proof of concept, and a fix patch and regression test where possible. Clear input lets the funnel spend its budget on verification, and vague input still gets a specific answer back.

When a finding reproduces, the acknowledgement note appended to the advisory names the tracking issue, the base commit, the reproduction command, and the observed result, and explains that the move to draft keeps later triage runs from reprocessing it. When a finding does not reproduce, the dismissal note states what was tried on origin/next, including any test the agent authored, and asks for a failing regression-test patch plus the exact command to run it. Both notes stay free of internal detail. Sprite names, checkpoint ids, private worktree paths, and anything else about the reproduction environment stay in the internal summary and the private issue, and the notes never ask the reporter to reproduce our setup. The private issue carries the complete record, from the original report to the full reproduction instructions and observed output, because attachment links alone do not count as a reproduction source.

Running it yourself

OpenProse installs as a skill, and the documentation has the harness-specific setup.

npx skills add openprose/prose

You can watch the whole machinery without letting it touch anything. Setting SECURITY_DRY_RUN=1 runs discovery, duplicate classification, worktree setup, reproduction, and note drafting, and then returns the exact text it would have submitted instead of submitting it.

SECURITY_DRY_RUN=1
# then, in the agent session:
prose run miden-security-advisory-funnel.prose.md

Setting SECURITY_GRILL_AMBIGUOUS=1 turns every needs_human_triage outcome into a ready-to-paste handoff prompt with the captured evidence, so a person can grill the result instead of reconstructing it. The remaining ### Environment variables retarget the funnel without editing the contract, with defaults that match our setup.

That is the whole setup. The report’s prose can claim whatever it wants, and the workflow answers with a base commit, a test, a command, an output, and a verdict, each traced to a run directory you can open later. GitHub records a change only after the evidence has earned it.

Feedback

Got a better idea? Found a problem, a security issue or a way to improve the above? Please get in touch!