proofcheck-ai 1.0.1

proofcheck checks whether a pull request does what it claims.
It runs the PR's tests before and after the change, replays the linked issue's reproducer,
and matches every claim in the description to the evidence it measured.

It makes no attempt to guess whether a human or an AI wrote the code. It only looks at evidence.

_{A real card: proofcheck 0.2 run on one of its own pull requests (#2). Running it there also caught a bug in proofcheck itself: quoted example phrases in the description were being counted as claims.}

Contents

• Why evidence instead of AI detection?
• How it works
• Quick start
• What's on the card
• Diff evidence map
• Agent evidence (experimental)
• Security model
• How proofcheck compares
• Configuration
• CLI reference
• FAQ
• Limitations
• Roadmap
• Contributing · License

Why evidence instead of AI detection?

Maintainers increasingly get pull requests that look right: tidy code, a confident description, "Fixes #123", a new test. Some come from people and some from AI tools. Classifying a PR as AI-generated answers a question maintainers don't need answered, and false positives hurt real contributors.

proofcheck asks the questions a careful reviewer asks first:

• Does the new test fail without the fix and pass with it? A test that also passes on the base commit doesn't exercise the change, however plausible it looks. This is the fail-to-pass criterion used to validate fixes in benchmarks such as SWE-bench.
• Does the issue's reproducer behave differently after the change?
• Which parts of the diff does that evidence actually depend on?
• Do the description's claims hold up? "Fixes #N", "adds tests", "3x faster", "no behaviour change", "backwards compatible".
• Does the diff touch anything surprising, such as CI workflows, dependency manifests or binaries?

A good human PR and a good AI-assisted PR both pass. A sloppy PR from either source gets a card that shows exactly what is missing. ⚠️ means no evidence, not wrong.

How it works

1. Claims. A rule-based extractor reads the PR title and description and finds claims such as Fixes #12, adds tests or 2x faster. It ignores code blocks, quotes and unfilled templates. An optional LLM extractor can add claims, but never verdicts.
2. Evidence. proofcheck checks out the base and head commits as git worktrees and gathers evidence from up to four sources:
   • Changed tests on base and head. The PR's added or modified tests run against the base code (with the new tests copied in) and against the head. A test that fails before and passes after is fail → pass.
   • Issue reproducer replay. Python snippets from the linked issue run on both commits; proofcheck records whether the behaviour changed.
   • Diff evidence map. Each changed hunk is undone in turn and the fail → pass evidence is rerun, which shows which hunks the evidence depends on.
   • Agent reproduction test (opt-in, experimental). If a fixes #N claim still has no evidence, an LLM writes a candidate test and proofcheck runs it on base and head itself.
3. Verdicts. Fixed rules match each claim to the evidence: ✅ verified, ❌ contradicted, or ⚠️ no evidence.
4. Card. The result is posted as a single PR comment that is updated in place, written to the job summary, and summarised in a label: proofcheck: verified, partial, contradicted or no evidence.

Quick start

1. Install

pip install proofcheck-ai             # the command and the import are `proofcheck`
# or, straight from GitHub:
pip install "git+https://github.com/bhaskargurram-ai/proofcheck@v1.0.1"

2. Generate the workflows

From the root of your repository:

proofcheck init            # add --agent to also set up the experimental agent

init detects your test runner (pytest, Jest or unittest), writes the caller workflows below plus a commented proofcheck.toml, refuses to overwrite existing files unless you pass --force, and prints the next steps. Commit the files and open a pull request.

3. The workflows it writes

proofcheck runs as separate workflows so that untrusted PR code and privileged tokens never share a job (why). Each caller is a few lines that point at a reusable workflow in this repository. Pin @v1.0.1, or a full commit SHA if you want to be strict.

.github/workflows/proofcheck.yml gathers evidence. It is unprivileged and is where PR code runs.

name: proofcheck

on:
  pull_request:
    types: [opened, synchronize, reopened, edited]

permissions:
  contents: read
  issues: read   # read linked issues on private repositories (read-only)

concurrency:
  group: proofcheck-${{ github.event.pull_request.number }}
  cancel-in-progress: true

jobs:
  evidence:
    uses: bhaskargurram-ai/proofcheck/.github/workflows/evidence.yml@v1.0.1
    with:
      proofcheck-ref: v1.0.1
      python-version: "3.12"
      # Installs the project under test; this runs PR code (unprivileged job).
      install-command: 'pip install -e ".[dev]" pytest || pip install pytest'
      fail-on: never   # or "contradicted" / "no-evidence" to fail the check

.github/workflows/proofcheck-comment.yml posts the card and the label. It is privileged and never runs PR code.

name: proofcheck comment

on:
  workflow_run:
    workflows: ["proofcheck"]   # must match the `name:` of proofcheck.yml
    types: [completed]

permissions: {}

jobs:
  comment:
    if: github.event.workflow_run.event == 'pull_request' && github.event.workflow_run.conclusion != 'cancelled'
    permissions:
      contents: read
      actions: read          # download the artifact of the triggering run
      pull-requests: write   # upsert the comment and the verdict label
    uses: bhaskargurram-ai/proofcheck/.github/workflows/comment.yml@v1.0.1
    with:
      proofcheck-ref: v1.0.1
      labels: true

.github/workflows/proofcheck-agent.yml (optional, experimental) tries to write a reproduction test when a fixes #N claim has no evidence. It runs only for PRs labelled proofcheck:agent or opened by owners, members and collaborators, unless you set run-for: everyone.

name: proofcheck agent

on:
  workflow_run:
    workflows: ["proofcheck"]   # must match the `name:` of proofcheck.yml
    types: [completed]

permissions: {}

jobs:
  agent:
    if: github.event.workflow_run.event == 'pull_request' && github.event.workflow_run.conclusion != 'cancelled'
    permissions:
      contents: read
      actions: read
      pull-requests: read
      issues: read
    uses: bhaskargurram-ai/proofcheck/.github/workflows/agent.yml@v1.0.1
    with:
      proofcheck-ref: v1.0.1
      llm-provider: ${{ vars.PROOFCHECK_LLM_PROVIDER }}
      llm-model: ${{ vars.PROOFCHECK_LLM_MODEL }}
      llm-base-url: ${{ vars.PROOFCHECK_LLM_BASE_URL }}
      llm-reasoning-effort: ${{ vars.PROOFCHECK_LLM_REASONING_EFFORT }}
      python-version: "3.12"
      install-command: 'pip install -e ".[dev]" pytest || pip install pytest'
      run-for: trusted   # or "everyone" (spends API credits on any fork PR)
    secrets:
      llm-api-key: ${{ secrets.PROOFCHECK_LLM_API_KEY }}

  comment:
    needs: agent
    if: needs.agent.outputs.verified == 'true'
    permissions:
      contents: read
      actions: read
      pull-requests: write
    uses: bhaskargurram-ai/proofcheck/.github/workflows/comment.yml@v1.0.1
    with:
      proofcheck-ref: v1.0.1
      # Trusted values: the PR number comes from the gate job (API data, no PR
      # code ran there) and the artifact from this run's verify job.
      pr-number: ${{ needs.agent.outputs.pr-number }}
      artifact-run-id: ${{ github.run_id }}
      labels: true

For the agent, add a repository secret PROOFCHECK_LLM_API_KEY and repository variables PROOFCHECK_LLM_PROVIDER (anthropic or openai) and PROOFCHECK_LLM_MODEL (optional: PROOFCHECK_LLM_BASE_URL, and PROOFCHECK_LLM_REASONING_EFFORT: OpenAI's GPT-6 Luna and Sol only call tools through Chat Completions with none); init --agent also sets [agent] enabled = true in proofcheck.toml. The key is only ever passed to the propose job, which never runs PR code. The agent workflow posts its own updated card through the same privileged comment workflow, so the comment workflow only listens for the evidence run.

On fork PRs the evidence workflow has no write token, so the card also appears in the run's job summary even before the comment workflow posts it.

proofcheck run --repo . --base origin/main --head HEAD \
    --pr-body-file pr.md --issue-body-file issue.md \
    --out card.md --json result.json

examples/demo/run_demo.sh /tmp/proofcheck-demo

What's on the card

Diff evidence map

A fail → pass test proves the PR changed something the test checks. The diff evidence map shows which parts of the diff that evidence depends on. It is deterministic and uses no LLM.

For each hunk in the changed non-test files, proofcheck takes a fresh worktree of the head, reverse-applies just that hunk, and reruns only the fail → pass tests and any reproducers whose behaviour changed:

The card shows a table of file:lines, status and which evidence broke, with a summary such as "3/4 changed hunks are required by the tests". Unexercised hunks also get a ⚠️ scope note ("changed, but no evidence depends on it"). That is a useful way to spot unrelated changes riding along in a PR. It is not proof that they are wrong: refactors, logging and docs are often unexercised by design. In Python files, a hunk that changes only comments, docstrings or formatting (the code's syntax tree is the same without it) is marked 📝 docs only, is not run and gets no scope note.

The map runs only when there is at least one fail → pass test or behaviour-changing reproducer, and is capped by ablation.max_hunks (default 12) and ablation.time_budget_s (default 300 s). Turn it off with --no-ablation or [ablation] enabled = false.

Agent evidence (experimental)

Many real PRs say "Fixes #123" but add no test, and many issues have no runnable reproducer. For exactly that case, proofcheck can ask an LLM to write a reproduction test, then run it on base and head itself. The agent is off by default.

• Propose (proofcheck agent propose). The model gets read-only tools (list_files, read_file, grep, get_diff, get_issue, list_tests) implemented with git plumbing. It cannot write files, run code or reach the network; its only output is a schema-validated submit_test call. Several different prompt variants run (by default reproduce-issue, exercise-diff, mimic-existing-tests), because varied prompts find more reproductions than resampling one. Candidates must parse, contain a test function, live under tests/proofcheck_agent/, and import modules that exist at head; near-miss module names are repaired by edit distance.
• Verify (proofcheck agent verify). No LLM. Each candidate runs on base and head through the same engine as the PR's own tests:

Agent evidence can never produce ❌. An LLM-written test that fails on head says more about the test than about the PR, so the card says "no evidence found" instead.

Expect it to fail often. Published research on generating issue-reproducing tests (Otter / Otter++, arXiv:2502.05368; see also SWT-bench) reports fail-to-pass success on roughly a third of issues (about 31–37 %), at under $0.10 per issue in that setup. We have not benchmarked proofcheck's agent; its token use and cost are recorded on every card. When it succeeds, the card shows the test in a collapsible block: commit it to keep the evidence.

Projects and Rust. In a repository with several [[project]] tables, the agent works in the project whose source the PR mainly changes, and runs its candidates there with that project's runner. For a cargo project it writes a Rust integration test (<crate>/tests/proofcheck_agent_<variant>.rs) in the crate with the most changed lines, using only the crate's public API (use <crate>::...); private items and inline #[cfg(test)] modules are out of reach, and a candidate that only fails on base because it does not compile there counts as weak evidence. Rust candidates have their own static checks (balanced brackets, a #[test] fn, no processes, network, unsafe or environment reads). See docs/AGENT.md.

proofcheck agent run chains propose and verify with up to agent.max_rounds refinement rounds that feed execution output back to the model. Use it only locally or in trusted contexts: it runs untrusted code in the same process that holds the API key. In CI, the agent workflow keeps propose and verify in separate jobs. Details are in docs/AGENT.md.

Security model

Running PR code safely is the core problem. proofcheck splits the work into three trust zones, connected only by artifacts:

• Untrusted code runs only in jobs without secrets. The evidence job runs on pull_request with contents: read, persist-credentials: false, a scrubbed environment, timeouts, and config read from the base commit. The agent's verify job has no secrets either.
• The LLM key never meets PR code. The propose job reads the PR's files as data through git and never installs or runs anything. Separate jobs run on separate VMs, so code in the verify job cannot read the key from the propose job's memory. The agent only runs for PRs labelled proofcheck:agent or from owners, members and collaborators, unless you opt in to everyone.
• The privileged comment job never checks out or executes PR code. It treats the artifact as hostile: it validates the PR number and the result.json schema, re-renders the card itself (the uploaded card.md is ignored), checks that the result matches the PR's current head SHA, and warns on the card when the PR modifies workflows or test-harness files.
• Never use pull_request_target together with a checkout of the PR head. That combination runs attacker code with a write token and your secrets.
• All PR-derived text is escaped on the card: HTML, @mentions, issue references, links, table pipes and control characters.
• Prompt injection. The rule-based path has nothing to inject into. PR text, issue text and file contents reach an LLM only as delimited, untrusted data; the model has no write, exec or network tools; its output is schema-validated and can't produce a ❌, and generated code only runs in a job without secrets.

proofcheck raises the bar for low-effort PRs. It is not a sandbox and not a defence against a determined attacker: a malicious PR can still tamper with its own evidence inside the unprivileged job. Read docs/SECURITY_MODEL.md for the full threat model.

How proofcheck compares

Different tools answer different questions. This table is our best reading of each category as of October 2026; corrections are welcome.

These tools are complementary. An AI reviewer comments on code quality and design, which proofcheck doesn't do at all. reprove's mutation testing measures how strong the tests are, which proofcheck doesn't do either. proofcheck focuses on one thing: whether the evidence backs the PR's claims.

Configuration

Put a proofcheck.toml at the repository root, or a [tool.proofcheck] table in pyproject.toml. The file is read from the PR's base commit, so a PR cannot change how it is checked. proofcheck init writes a commented starting point.

runner = "pytest"                      # pytest | unittest | jest | cargo
test_command = "python -m pytest -x"   # optional; {junitxml} and {tests} placeholders supported (cargo: a prefix, default "cargo test")
test_patterns = ["tests/*", "test_*.py", "*_test.py", "conftest.py"]   # files copied from head into base
test_module_patterns = ["test_*.py", "*_test.py"]                     # files that are run
timeout = 600                          # seconds per test run (cargo projects: 1800 unless set)
setup_command = ""                     # optional, run in each worktree before tests (e.g. a build step)
cargo_target_dir = ""                  # cargo: shared target dir (default $CARGO_TARGET_DIR, else <tmp>/proofcheck-cargo-target)
large_diff_threshold = 1000            # changed lines
max_issues = 5

# Optional benchmark for performance claims: runs N times on base and head
# (interleaved) and compares median wall time.
benchmark_command = ["python", "benchmarks/bench_parse.py"]
benchmark_runs = 5
benchmark_timeout = 600

[test_env]                             # extra env vars for test runs
APP_ENV = "test"

[repro]
enabled = true
timeout = 60
python = "python"                      # interpreter for issue snippets

[ablation]                             # diff evidence map
enabled = true
max_hunks = 12
time_budget_s = 300
exclude = ["*.md", "*.rst", "*.txt", "docs/*", "LICENSE*", "CHANGELOG*", ".github/*"]

[agent]                                # experimental reproduction-test agent
enabled = false
when = "missing-evidence"              # or "always"
variants = 3                           # 4 adds "localize-first"
max_rounds = 2                         # refinement rounds, `agent run` only
max_tool_calls = 25                    # per variant
test_dir = "tests/proofcheck_agent"
# test_timeout = 120                   # seconds per candidate and commit (default 120; cargo: the project's timeout)
max_output_tokens = 4096               # per model response
max_total_tokens = 1500000             # input + output over the whole run
max_cost_usd = 0                       # 0 = no cap; enforced only when prices are set
# price_input_per_mtok = 0.0           # USD per million tokens, to report cost
# price_output_per_mtok = 0.0
# temperature = 0.0                    # omitted from requests unless set
request_timeout = 120
max_retries = 4

[llm]                                  # optional LLM claim extraction
enabled = false                        # the API key is never read from this file
provider = "openai"                    # or "anthropic"
model = ""
base_url = ""

[[project]]                            # optional, repeatable: a test project in a subdirectory
name = "python-sdk"                    # prefixes test ids when there is more than one project
path = "adapters/python"               # relative POSIX path, no ".."; "." for the root
runner = "pytest"                      # also: test_command, setup_command, test_paths, timeout, test_env, cargo_target_dir

Several projects in one repository. Without [[project]] tables the top-level keys describe the one project at the repository root, exactly as before. Each [[project]] table adds a project in a subdirectory (or replaces the root project when path = "."; the top-level runner/test_command/setup_command/test_patterns must then move into that table). Every changed file belongs to the deepest project that contains it, is classified by that project's runner, and its tests run with the project directory as the working directory in the base and head worktrees (Python: <project>/src and <project> go on PYTHONPATH). With more than one project, test ids are prefixed with the project name (python-sdk:tests.test_client::test_x), the card lists each project's status, and result.json gains tests.projects. proofcheck init detects projects (the root plus pyproject.toml, setup.cfg, package.json with a Jest test script and cargo workspace roots up to three levels deep, skipping examples/, fixtures/, vendor/, packaging/, docs/ and the like) and writes the tables when it finds more than one.

Rust (runner = "cargo"). Changed integration tests (<crate>/tests/<name>.rs) run per target with cargo test -p <package> --test <name> --no-fail-fast -- --test-threads=1; libtest's plain output is parsed (no nightly flags). When a PR changes a #[cfg(test)] mod tests { ... } block inside a src/ file, only that module is transplanted from the head version into the base version of the file and run with cargo test -p <package> --lib <module>::tests:: on both commits; files whose test module cannot be separated from the code by proofcheck's small lexer are skipped with a note. A test target that does not compile on the base commit counts as fail → pass, and the card says it failed only because it did not compile there (the API is new). Base, head and the diff evidence map share one CARGO_TARGET_DIR so dependencies compile once; the evidence workflow installs the toolchain from rust-toolchain.toml and uses Swatinem/rust-cache in the unprivileged job only. Allow 60–120 minutes (timeout-minutes) for large workspaces.

Environment variables

The optional LLM claim extractor sends PR text as untrusted data inside random delimiters, gives the model no tools, and accepts only strict JSON. Every claim must quote text that actually appears in the PR, and LLM-found claims can only add things to check.

CLI reference

proofcheck init      [--repo .] [--agent] [--force] [--ref v1.0.1]
proofcheck context   --out context.json [--max-issues 5]
proofcheck run       --base REF [--head HEAD] [--repo .] [options]
proofcheck summary   --json result.json
proofcheck comment   --json result.json --pr N [options]
proofcheck agent propose --repo DIR --base REF --head REF --out-dir DIR
                         [--context-file F] [--result result.json] [--config F]
proofcheck agent verify  --repo DIR --base REF --head REF --candidates DIR
                         --result result.json --json OUT --out card.md
proofcheck agent run     (propose + verify + refinement; local or trusted use only)

FAQ

Limitations

• A fail-to-pass test proves the PR changes behaviour the test checks, not that the test checks the right behaviour.
• Test runs share the CI job with PR code, so a malicious PR can tamper with its own results.
• proofcheck does not measure test strength: there is no mutation testing.
• The diff evidence map reverts one hunk at a time; hunks that only matter in combination may show as unexercised.
• Benchmarks on shared CI runners are noisy. Differences under 5 % are treated as noise.
• Issue reproducers are Python only and are compared with the previous behaviour, not with an expected output.
• The agent is experimental and often finds nothing. Its tests can be wrong, which is why they can never contradict a claim.
• The Jest runner is experimental and has not been tested against many real projects.
• Rust: only integration tests and inline #[cfg(test)] modules of changed files in existing crates are run (not doctests, benches or examples); #[path] module attributes, out-of-line mod tests; files and inline tests in new files are not handled. Build scripts and proc macros run on base and head like any test code.

Roadmap

• Runners for Vitest, Go (go test + go-junit-report), cargo-nextest (JUnit, per-test timeouts) and a hardened Jest runner
• Optional mutation testing of changed lines, to report how strong the fail → pass tests are
• Benchmark integrations (pytest-benchmark, hyperfine, criterion) and memory measurements
• Reproducers in other languages, and expected-output assertions from issues
• A GitHub App mode that runs checks in isolated sandboxes instead of the PR's CI job
• Check-run annotations next to the PR comment

Contributing

Contributions are welcome. See CONTRIBUTING.md. In short:

pip install -e ".[dev]"
python -m pytest            # or, without pytest: python -m unittest discover -s tests

The test suite builds real throwaway git repositories and worktrees, so it needs git on PATH. docs/TESTING.md describes every test level, including the packaging check and the end-to-end harness in e2e/ that opens real pull requests against a test repository. Please report security issues privately through the repository's security advisory form rather than in a public issue.

License

MIT © 2026 Bhaskar Gurram