Add proofcheck: evidence checks for pull requests

.github/workflows/proofcheck-agent.yml

@@ -0,0 +1,63 @@
+# proofcheck agent evidence (EXPERIMENTAL, opt-in).
+#
+# When the evidence run finds no proof for a "fixes #N" claim, an LLM agent
+# tries to write a reproduction test, and proofcheck runs it on base and head.
+# The work is split over separate jobs (separate VMs):
+#   gate    - decides whether to run; reads the API only, runs no PR code
+#   propose - holds the LLM key; reads the PR as data, never installs or runs it
+#   verify  - runs the candidate tests on base and head; no secrets, read-only token
+#   comment - re-posts the card with the agent section; never runs PR code
+#
+# Setup: repository secret PROOFCHECK_LLM_API_KEY, repository variables
+# PROOFCHECK_LLM_PROVIDER (anthropic | openai) and PROOFCHECK_LLM_MODEL
+# (optional: PROOFCHECK_LLM_BASE_URL). By default the agent only runs for pull
+# requests by owners, members and collaborators, or labelled `proofcheck:agent`.
+#
+# Generated by `proofcheck init --agent`.
+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
+    with:
+      proofcheck-ref: v1.0
+      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: >-
+        python -m pip install --quiet --no-deps -e ./adapters/python &&
+        python -m pip install --quiet pytest pytest-asyncio "langgraph>=1.0" "langchain-core>=1.0" "openai-agents>=0.22" "claude-agent-sdk>=0.2" pyyaml
+      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
+    with:
+      proofcheck-ref: v1.0
+      # 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

.github/workflows/proofcheck-comment.yml

@@ -0,0 +1,29 @@
+# proofcheck, part 2 of 2: post the proof card (PRIVILEGED, never runs PR code).
+#
+# Triggered when the `proofcheck` workflow completes. `workflow_run` runs with
+# a token that can comment, so the reusable workflow never checks out,
+# installs or executes anything from the pull request: it downloads the result
+# artifact, validates it, re-renders the card, upserts one comment and sets a
+# `proofcheck: <verdict>` label. Do not use `pull_request_target` instead.
+#
+# Generated by `proofcheck init`.
+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
+    with:
+      proofcheck-ref: v1.0
+      labels: true

.github/workflows/proofcheck.yml

@@ -0,0 +1,35 @@
+# proofcheck, part 1 of 2: gather evidence (UNPRIVILEGED).
+#
+# Runs on `pull_request`, so for pull requests from forks GitHub gives this
+# workflow a read-only token and no secrets. Untrusted PR code (tests, issue
+# reproducers) only ever runs here. The proof card goes to the job summary and
+# into the `proofcheck-result` artifact; proofcheck-comment.yml posts it.
+#
+# Generated by `proofcheck init`. Pin the reusable workflow to a release tag
+# or, stricter, to a full commit SHA, and keep `proofcheck-ref` the same.
+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
+    with:
+      proofcheck-ref: v1.0
+      python-version: "3.12"
+      timeout-minutes: 90   # Rust: compiling the workspace for base, head and ablation takes a while
+      # Installs the project under test; this runs PR code (unprivileged job).
+      install-command: >-
+        python -m pip install --quiet --no-deps -e ./adapters/python &&
+        python -m pip install --quiet pytest pytest-asyncio "langgraph>=1.0" "langchain-core>=1.0" "openai-agents>=0.22" "claude-agent-sdk>=0.2" pyyaml
+      fail-on: never   # or "contradicted" / "no-evidence" to fail the check

proofcheck.toml

@@ -0,0 +1,52 @@
+# proofcheck configuration (https://github.com/bhaskargurram-ai/proofcheck).
+#
+# Read from the pull request's BASE commit, so a PR cannot weaken its own
+# check. Every key is optional; the commented values are the defaults.
+
+# runner = "cargo"               # pytest | unittest | jest | cargo
+# test_command = ""                 # custom command; placeholders {junitxml} and {tests}
+# setup_command = ""                # run once in each worktree before the tests
+# timeout = 600                     # seconds per test run
+# test_env = { PYTHONHASHSEED = "0" }
+# benchmark_command = ""            # e.g. "python bench.py": lets "2x faster" claims be checked
+# benchmark_runs = 5
+# large_diff_threshold = 1000
+# max_issues = 5
+
+# [repro]                           # replay ```python and >>> reproducers from linked issues
+# enabled = true
+# timeout = 60
+
+[ablation]                          # diff evidence map: revert each changed hunk, re-run the evidence
+enabled = true
+max_hunks = 12
+time_budget_s = 1200                # Rust: each hunk rebuilds the crate
+# exclude = ["*.md", "*.rst", "*.txt", "docs/*", "LICENSE*", "CHANGELOG*", ".github/*"]
+
+# [llm]                             # optional LLM claim extraction (off by default)
+# enabled = false
+# provider = "anthropic"            # or "openai" for any OpenAI-compatible endpoint
+# model = ""                        # the key comes from PROOFCHECK_LLM_API_KEY, never from this file
+
+[agent]                             # experimental agent evidence (proofcheck-agent.yml)
+enabled = true
+# variants = 3
+# max_rounds = 2
+# max_tool_calls = 25
+# when = "missing-evidence"         # or "always"
+# test_dir = "tests/proofcheck_agent"
+
+# Test projects (detected by `proofcheck init`). Each changed file belongs to the deepest
+# project containing it; tests run inside the project's directory. Per-project keys:
+# runner, test_command, setup_command, test_paths, timeout, test_env, cargo_target_dir.
+
+[[project]]
+name = "rust"
+path = "."
+runner = "cargo"
+# timeout = 1800                   # seconds per run (cargo default: 30 minutes)
+
+[[project]]
+name = "python"
+path = "adapters/python"
+runner = "pytest"