The judges' lab

One command builds Proven and starts a Gitea lab on this machine. The lab binds to 127.0.0.1. Nothing in it is published on another address: each port line of lab/compose.yaml names 127.0.0.1 itself, so starting that file directly, with any environment, publishes nothing beyond loopback. No setting chooses the address. The old LAB_BIND is retired: make up refuses it when it is set (an empty value too), names it, and starts no container. The lab does not serve SSH. It publishes three ports, all on that address: Gitea's web UI (GITEA_HTTP_PORT, 3000), Grafana's (LGTM_GRAFANA_PORT, 3001) and the collector's OTLP/HTTP endpoint (LGTM_OTLP_PORT, 4318).

You need GNU make and Docker. Docker Compose v2 is the docker compose command. Windows is not a target. On macOS the make from Homebrew is GNU make; the make that ships with the system is not.

Every version, port and name is a setting in lab/versions.env. The environment overrides the file. The list is in CONFIGURATION.md. The image tags were chosen as pins and were not pulled when this page was written. The first make up is the check that each tag exists. A missing tag is changed by setting the variable, not by editing the Makefile.

Start

From a checkout of this repository, run make up.
The first run prints the admin user and the lab URL, and generates a password. When the output is a terminal, the password is printed once. When it is not (CI, a redirect, a pipe), the password is not printed: it is written to lab/.state/admin-password, readable only by you (mode 0600), and make up prints that path. To choose the password yourself, set LAB_ADMIN_PASSWORD (8 characters or more) in the environment of the first make up: it is used, and neither printed nor written to a file on the host, and it never appears in the Compose environment or in docker compose config. The password is also kept in the lab's volume until make clean, which removes the file too. A later make up does not print it again and does not write the file again. It does not stop because the volume is already there. It creates the admin user, the runner registration and the pull request when any of those is missing.
Open the URL in a browser. Sign in with that user and password.
Open the discount repository. It has one open pull request.
The pull request runs the workflow in lab/workflow/proven.yml. When the job finishes, the pull request has a comment whose body starts with ``. That comment is the sample review, and the marker names the run that posted it.
make up also prints the dashboard's address, http://127.0.0.1:3001/d/proven-review by default. See The dashboard.

make status prints the containers, Gitea's health, whether the runner is registered, whether that comment is present, and the URL.

make logs follows every service. make logs SERVICE=gitea follows one of gitea, dind, runner, lgtm.

The seed always runs as a user that is not root, and that user owns the state volume, mode 700, with the password and tokens at mode 600. A state volume made by an older lab is owned by root and the seed cannot write to it: run make clean, then make up.

make down stops the lab and removes its containers. The volume, the admin user and the password remain. make clean removes the volumes, the local images, ./bin and ./dist.

The dashboard

A review is observable while it runs (ADR-0045). Proven sends an OpenTelemetry trace and metrics. The lab runs grafana/otel-lgtm as one more container, lgtm: an OpenTelemetry collector, Prometheus, Tempo, Loki and Grafana in one image, pinned by LGTM_VERSION. It is not part of Proven's code or image. make up starts it, waits for Grafana, and prints the dashboard's address. make down removes the container with the others, and make clean removes it with the lab's volumes.

The lab's pull-request review is told where to send its data, with the standard variables and nothing of Proven's own: the seeded workflow starts Proven on the lab network with OTEL_EXPORTER_OTLP_ENDPOINT, OTEL_SERVICE_NAME and OTEL_METRIC_EXPORT_INTERVAL set from lab/versions.env. It also runs the review with a second reviewer model (LAB_SPECIAL_REVIEWER), so there are two reviewers to show. The sample generator answers for both; the findings are the same as with one. The same proven.yaml turns on autofix, the one automated fix attempt of ADR-0050, which is on in the lab and off everywhere else until it is measured; the lab's sample change records no answer for it, so the sample review prints what it printed before.

Watch a review

Run make up. Open the dashboard address it printed. Sign-in is not asked: the lab turns Grafana's anonymous access on, as an administrator, because the lab binds to 127.0.0.1. The lab publishes nothing beyond loopback, so only this machine reaches Grafana.
Leave the dashboard open. It refreshes every 5 seconds and shows the last 30 minutes.
Start a review of the pull request: push a commit to the change branch of discount, or close and reopen the pull request in Gitea. The workflow runs on the runner (make logs SERVICE=runner).
Watch the first panel. Each agent is a row, and the planner and the skeptic have one row per reviewer model. A row is grey while it waits, blue while it works, green when done, red when it failed. A review is short in sample mode: a live review, with a model behind each call, is the one where a reviewer finishes while the other still works.
When the review is done, the other panels hold its numbers. The Review menu at the top picks one review; the default is all of them in the time range.
make trace asks the trace store for the latest review's trace, the same query the last panel runs, and prints its span names and the reviewers they name. It exits 1 when the trace is missing a span or a reviewer.

What each panel shows

Panel	What it shows	Where it comes from
The agents and the two reviewers	A state timeline: every agent, and each reviewer model's planner and skeptic, waiting, working, done or failed	the `proven.agent.state` gauge, one value per agent and reviewer
Verdicts, side by side	What each reviewer's skeptic said of each finding (refuted, upheld, not attempted), one column per reviewer	the `proven.reviewer.verdicts` counter
Where the reviewers disagree	Findings on which they differ: `verdict` (both ran it and judged it differently) or `one_reviewer` (only one named it)	the `proven.reviewer.disagreements` counter
Claims dropped	What the Judge did not keep, by reason: `no_evidence`, `refuted`, `suppressed`	the `proven.review.claims.dropped` counter
Findings by level of proof	What the review kept: proved by test, by tool, by data, or agreed by two models and not proven (ADR-0044)	the `proven.review.findings` counter
Model latency	The mean time of a call to a model, by agent and reviewer	the `gen_ai.client.operation.duration` histogram
Model calls	Calls made, by reviewer and outcome	the `proven.model.calls` counter
Guardrail checks	Every prompt and answer that was checked, by side and verdict; red for `unsafe` and `refused`	the `proven.guardrail.checks` counter
Unsafe verdicts	How many checks said unsafe	the `proven.guardrail.unsafe` counter
Reviews seen	How many reviews reported in the time range	the `proven.agent.state` gauge
The spans	The trace of each review from Tempo: one trace, one span per agent, one per model call under it, with its reviewer and model. A trace ID opens the waterfall, where the two reviewers sit side by side	the trace; TraceQL `{ span.proven.agent != "" }`

The dashboard is the JSON file lab/grafana/dashboards/proven-review.json, provisioned on start. Nothing in it is drawn by hand, and Grafana does not let the page change it. To change it, edit the file; Grafana reads it again within 10 seconds.

Use it outside the lab

The same data goes to any OpenTelemetry backend. Set OTEL_EXPORTER_OTLP_ENDPOINT to its OTLP/HTTP address, and Proven exports; leave it unset and Proven exports nothing and opens no connection. For a review run on the host against the lab's collector: OTEL_EXPORTER_OTLP_ENDPOINT=http://127.0.0.1:4318 proven scan --sample <path>. The settings are listed in CONFIGURATION.md. The collector's Prometheus is inside the container and is not published; to scrape Proven's numbers from an existing monitoring stack, point OTEL_EXPORTER_OTLP_ENDPOINT at that stack's own collector.

The keys a live review needs

This page says which keys the lab needs for each way of running the model generator, and where to get each one (ADR-0031 point 6). It covers keys only. Every setting and its default is in CONFIGURATION.md. Sample mode needs no key and makes no call: SAMPLE_MODE.md.

With one NVIDIA key (no Nightshift needed)

A free NVIDIA API key is enough to see Proven's agents work on live models.

Go to https://build.nvidia.com and sign in.
Open any model and choose Get API Key. Copy the key; it is shown once.
Put the key in the environment, never in a file that is committed:
PROVEN_GENERATOR_MODE=nvidia PROVEN_GENERATOR_KEY=<the key> PROVEN_GUARDRAIL_MODE=nvidia PROVEN_GUARDRAIL_KEY=<the same key, or another>
Check it before a review with livecheck. Its generator line names the mode, and a missing or rejected key.

The address and the models have defaults, so nothing else is needed. In this mode the address is PROVEN_NVIDIA_BASE_URL (https:// only; any other value is refused by name). PROVEN_GENERATOR_BASE_URL is not read here, so a Nightshift address left in the environment never receives the key. livecheck names the host the answer came from. The hosted API signs no receipt, so the trace says no receipt for each call, and the requirement that an agent be answered by an nvidia/* model is checked against the model field of the answer. A free key is rate limited; a review that meets the limit names it as a failed service.

With Meterless Nightshift (the default)

Set METERLESS_RUNTIME_TOKEN to the runtime token of the Nightshift you run, and PROVEN_GENERATOR_BASE_URL to its address (this variable is read in nightshift mode only). PROVEN_GENERATOR_MODE is left empty or set to nightshift. Nightshift is the team's own service: a judge without one uses the NVIDIA key above.

Keys of the other services

Service	Key	Where it comes from	If it is empty
Guardrail	`PROVEN_GUARDRAIL_KEY`	the same NVIDIA key page, when `PROVEN_GUARDRAIL_MODE=nvidia`	every model call is refused and the review names the guardrail
Zetaris evidence	see CONFIGURATION.md	the Zetaris account	Zetaris is down and the review names it; the rest runs

A second reviewer: one more key

The lab runs with NVIDIA alone (ADR-0037 point 6). Every change gets one independent review, from the default reviewer, and nothing else is needed.

Proven can review every change with two models. The second one is any model behind an OpenAI-compatible chat API: OpenAI, Anthropic through its compatible endpoint, or a server on your own machine. You switch it on with three settings in the environment Proven runs in, and the key is the switch:

Variable	Value
`PROVEN_SECOND_REVIEWER_KEY`	the API key. Secret: never printed, never written to the trace or the result
`PROVEN_SECOND_REVIEWER_BASE_URL`	the API address, for example `https://api.openai.com/v1` or `http://localhost:11434/v1`
`PROVEN_SECOND_REVIEWER_MODEL`	the model name the API knows, for example `gpt-5`

Add the three variables and run the lab as before. Take the key away and the lab is back to one reviewer. Nothing else changes.

What you see once it is connected

Both reviewers look at every change. They work independently: neither is shown the other's answer. A change under review cannot narrow this for itself: proven.yaml is read from the baseline.
Where they differ, the review says so. Each finding carries both reviewers' verdicts and reasons, and the review counts the disagreements; the two are kept side by side and never averaged. The block The reviewers disagree, which shows them in the text, Markdown, HTML and pull-request comment output, and the verdicts in the JSON and SARIF output, arrive with the shell train (see ARCHITECTURE.md); the command line does not render them yet. Evidence still decides what is reported: a risk neither reviewer can prove is not a finding, however many models name it.
Every review names its reviewers, and whether either of them is the model that wrote the change.

What it costs

Two reviewers cost two model calls per review step. To spend less, name the classes the second reviewer covers in proven.yaml, for example doubled_classes: security,backend. The security class is always doubled when a second reviewer is connected. See CONFIGURATION.md for the settings and their refusals: a key with no address or no model, or an address that is not an http or https URL, stops Proven before any review starts and names the variable.

If the second reviewer is down

A review whose second reviewer fails still completes with the first reviewer's findings. The failure is listed under second-reviewer in the review's failed services, and the findings show the second reviewer's verdict as no answer, which is not a disagreement.

What the workflow runs

Proven's Action is not on main yet, so the workflow does not use it. It runs:

proven scan --sample --md /opt/proven/fixture/discount

That is the recorded sample in testdata/fixture/discount, baked into Proven's image. It does not review the diff of the demo pull request. Sample mode uses no keys, no Docker and no model: it makes no call to a service. In the lab the job also sends the review's telemetry to the lab's own collector (see The dashboard), which is why the seeded copy starts Proven on the inner daemon's network; the committed workflow does not. The comment is the Markdown of that review (Markdown): a verdict line, a findings table and each finding's evidence in a collapsible block. The lab, like the Action, posts that one comment and no line comments (ADR-0020 §7).

One comment per pull request

The workflow posts ONE comment on a pull request and edits it in place on every new run, so run=1, run=2 and so on no longer pile up. The comment's first line is still ``, now with the latest run and head: make e2e reads that line and passes only when a comment by proven-bot starts with it for the current run and head.

How the step finds its comment: it asks the server which account the token is (GET /user), lists the pull request's comments page by page (GET /repos/{repo}/issues/{pr}/comments), takes the first comment written by that account whose body starts with ``, where N is that run's number and the commit is the pull request's current head. The workflow fills both from github.run_number and github.event.pull_request.head.sha. No time is compared, because two events in one second cannot be told apart by time. A run still pending, or no status yet, is waited for. make check-e2e-parse checks the parsers offline against comments and statuses shaped as Gitea serves them; it covers the lab admin posting the exact marker after a successful run that posted nothing, an unrelated account's marker, a successful run that posted nothing, an older run's review from the same second, and a review of another head commit. A review comment of an older run, of another commit, or by another account does not count and e2e says which it ignored: a lab volume kept by make down keeps its comments. If a kept volume still holds an older copy of the workflow on the pull request's branch, the run posts the old marker and e2e fails closed; run make clean && make up.

It exits 1 when that run finished as failure or error, and names the run and its status:

e2e: workflow run #2 for pull request #1 (head commit <sha>) finished with status failure

It also exits 1 when the wait ends with no run, a run that is still going, or a successful run with no new review.

If Gitea is already running and the runner container is not, make e2e does not start the runner. It exits 1 and prints:

e2e: runner is not running, so the workflow cannot post a review

That is the check that a stopped runner cannot look like a successful rehearsal. From the repository root, stop the runner and run the rehearsal again:

docker compose --env-file lab/versions.env -f lab/compose.yaml --project-directory lab stop runner
make e2e

A second check proves e2e cannot be fooled by an old comment. With the runner alive and an old review comment on the pull request, make the current run fail and require make e2e to refuse:

make e2e
make e2e-failed-run

make e2e-failed-run commits a workflow that fails on purpose to the pull request's head branch, runs make e2e, and puts the original workflow back. It exits 0 when e2e exited non-zero and named the failed run, and 1 when e2e accepted it. It needs the first make e2e to have passed, so an old comment exists. Restoring the workflow starts one more run; wait for it to finish before you run make e2e again.

Third-party images

These pins are not built here. make scan replaces the block below with Docker Scout's output. A finding in a third-party image does not refuse the scan: we cannot patch it, and a judge should see it.

Not scanned in the change that added the lab. The seat that wrote this page could not run Docker Scout. make scan fills this block.

Images: gitea/gitea:1.22.6, gitea/act_runner:0.2.11, grafana/otel-lgtm:0.11.0, docker:29.9.1-dind, docker:29.9.1-cli.

The judges' lab

On this page