From a35cc41422d8415dab4f84ed48928acbb3ed359f Mon Sep 17 00:00:00 2001 From: Bhaskar Gurram Date: Tue, 13 Oct 2026 17:37:16 -0400 Subject: [PATCH] Add proofcheck: evidence checks for pull requests proofcheck runs each PR's changed tests on the base and head commits, replays reproducers from linked issues, maps which changed hunks the evidence depends on, and posts a proof card. Two projects: the Rust workspace (cargo) and the Python SDK in adapters/python (pytest). The agent workflow is opt-in and needs the PROOFCHECK_LLM_* secret and variables. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_017bQP5nwJVPMXqMhewzhQv5 --- .github/workflows/proofcheck-agent.yml | 63 ++++++++++++++++++++++++ .github/workflows/proofcheck-comment.yml | 29 +++++++++++ .github/workflows/proofcheck.yml | 35 +++++++++++++ proofcheck.toml | 52 +++++++++++++++++++ 4 files changed, 179 insertions(+) create mode 100644 .github/workflows/proofcheck-agent.yml create mode 100644 .github/workflows/proofcheck-comment.yml create mode 100644 .github/workflows/proofcheck.yml create mode 100644 proofcheck.toml diff --git a/.github/workflows/proofcheck-agent.yml b/.github/workflows/proofcheck-agent.yml new file mode 100644 index 0000000..f5be16e --- /dev/null +++ b/.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 diff --git a/.github/workflows/proofcheck-comment.yml b/.github/workflows/proofcheck-comment.yml new file mode 100644 index 0000000..2cab83b --- /dev/null +++ b/.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: ` 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 diff --git a/.github/workflows/proofcheck.yml b/.github/workflows/proofcheck.yml new file mode 100644 index 0000000..63706d6 --- /dev/null +++ b/.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 diff --git a/proofcheck.toml b/proofcheck.toml new file mode 100644 index 0000000..b49c7eb --- /dev/null +++ b/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"