Tools · open source

Prove

Find where a system breaks, and prove whether your change moved it.

Name the conditions. Prove runs your system across them, before and after a change, and returns what moved, and what was too small for the run to detect. The physics or the agent, and what counts as failure, stay yours. It brings the sweep, the seeds, the store and the statistics.

Open source. Not released yet; we are using it on our own work first. Request early access.

It is one of the lab's open-source tools, and the one the others report to. The methods behind every number are one page.

The commands you run

# 1. sweep the conditions, before the change
proofload sweep quickstart.toml \
    --target proofload.examples.mock_agent:rollout --yes

# 2. sweep again after it, on the same seeds
proofload sweep quickstart.toml \
    --target ...mock_agent:rollout_patched --pair-with <run-a> --yes

# 3. diff the pair into report.md, heatmap.svg, receipt.html
proofload report <run-a> <run-b> \
    --event violated --x tool_fail_rate --y task_id

# in CI: exit 1 if any condition came back significantly worse
proofload check <run-a> <run-b> --event violated --fail-on worse

How it works

Map

The conditions you name, a seed per condition and replicate derived from a run salt, every episode appended to a store with its config, seed, outcome and time. A second run with the same salt gets the same seeds, cell for cell, without anyone arranging it.

Diff

Per condition, the event rate with censoring handled. Between two runs, a test per condition with a false-discovery correction across every condition, and a verdict for each: safer, worse, or no significant change.

The default test treats the two runs as separate samples; a paired test that uses the shared seeds is one flag away.

Say what it could not see

Every verdict carries the smallest effect that condition had the power to detect. "None worse" at a given N is a claim only above that number, and the report puts it on the line that matters. What was too small to see is said, not implied.

Out — 400 conditions × 32 trials is 12,800 rollouts, chunked into 200 batches of 64. Every shade in the upper strip is one batch, tinted by its place in that plan. Back — the same batches in the same tints, in the order they actually finished. The gradient is gone, and that scramble is the whole point: no batch waits for another and none of them share state, so the store fills in an order nothing chose. Each one is appended as a part and never rewritten. Only at the end, over the whole stack, does anything read it — Aalen–Johansen per cell, then Fisher exact and Benjamini–Hochberg across all 400, giving 60 safer · 0 worse.

Batch count, batch size and rollout count are this run's. Arrival order is illustrative — the golden fixture's wall_time is synthetic, so there is no real completion order to draw.

Fig. AWhat happens to a sweep. Batches leave in plan order, land in the store as they finish, and are never rewritten; the statistics read the whole stack once, at the end. The counts are the Go1 run's own.

v0 v1 censored — the episode ended without falling Greenwood 95%

Fig. BUnder one square of the map: a single Go1 condition, both versions, as the share still standing over time, with its band and a tick for every run that outlived the test. The estimator is Prove's. The drawing is this page's: the tool renders heatmaps and forest plots, not curves. Why runs that did not finish are counted this way

The sweep spec you write

target_id = "mock-agent@v0"
t_unit = "tool_calls"
replicates = 100

[axes.task_id]
type = "categorical"
values = ["search", "checkout", "refund"]

[axes.tool_fail_rate]
type = "continuous"
values = [0.0, 0.3, 0.55]

quickstart.toml, the example that ships with the tool: two axes crossing to 9 conditions, 100 replicates each, 900 rollouts. No API key, no network.

The one function you write

import proofload

def rollout(cfg: dict, seed: int) -> proofload.Episode:
    result = run_my_system(task=cfg["task_id"], seed=seed)
    return proofload.Episode(
        outcome=result.terminal_state,  # your label
        t=result.steps,
        horizon=20,
    )

Everything about your system stays behind this call. Prove hands it one condition and one seed, and takes back an outcome and a time.

The head of a real report.md

# Go1 v0 -> v1

fell: 60 safer, 0 worse
(aalen_johansen + fisher_bh, BH q<0.05 over 400 tests, unpaired)

Worst-powered unchanged cell (push_pct_bw=100, mu=0.95, n=32/32) can only detect a 34pp rise. "0 worse" is an honest claim only above that.
Worst-powered cell overall: 34pp (push_pct_bw=10, mu=0.1).

The pre-flight

At 100 replicates the quickstart clears the power gate on its own, so a run refuses to start only when the design cannot resolve the effect you asked it for.

The gate is the point. Prove works out the smallest effect your design can detect before it spends anything, and says so.

It brings the statistics and nothing else. There's no simulator in it, no environment framework, no benchmark and no training loop; it never reaches into your process, and it never phones home.

Agentic systems

The conditions are the task and the settings around it: which task, which temperature, how often a tool fails. The event is a failed assertion, a violated constraint, an error you've decided counts.

An agent on a sampling model is noisy in a way a policy in a fixed simulator isn't, so the first thing to measure is the noise itself. Run the same system twice on the same seeds with nothing changed, and whatever moves is the floor a real change has to clear. Prove derives both runs' seeds from one salt, so the two runs share every seed rather than hoping they line up; the test uses that matching only when asked.

1 worse 327 no significant change 0 safer coloured only at q<0.05, corrected across every condition

failed_assertion: 0 safer, 1 worse, 327 no significant change over 328 conditions. Hover any point.

Fig. 1A code agent against itself: each condition's failed_assertion rate in the first run against the second, one point per condition, 164 HumanEval tasks at temperatures 0 and 0.7, 32 episodes per cell, on the same seeds in both, tested by McNemar's test per condition and corrected across all 328. Agreement is the dashed diagonal. Ink: no significant change, 327 conditions. A purple diamond is significantly worse and a green circle significantly safer; here 1 is worse and 0 safer, and that one is the substrate moving on its own. The worst-powered cell could not have seen a change under 34pp. Model gpt-4o-mini-2024-07-18 on modal, runs 20260905T185407Z-0313 and 20260905T195009Z-18ac, same seeds, 40 min later. report.md · receipt.html

Robotics

The conditions are the physics: friction, push, mass, terrain, latency. The event is a fall, or whatever else you've decided counts as failure.

A policy that passes a benchmark still has a boundary, and the boundary has a shape. Prove maps it under the conditions you name, and when you retrain to move it, the diff says which conditions actually moved and which ones the run was too small to judge. The physics and the policy stay in your code; Prove never loads either.

0 worse 340 no significant change 60 safer coloured only at q<0.05, corrected across every condition

PUSH, % BODYWEIGHT → ↑ FRICTION μ 32 TRIALS PER CELL PER VERSION

Go1 locomotion, v0 → v1. Hover any cell, or focus the grid and use the arrow keys.

Fig. 2Go1 locomotion, v0 against v1: 400 conditions of floor friction (up) and lateral push in percent of bodyweight (across), 32 trials per cell per version, on the same seeds in both. Green: fell significantly less often, 60 conditions (Fisher's exact test per cell, corrected across all 400, which does not use the matching seeds). Grey: no significant change, darker where the baseline fell more often. 0 conditions got significantly worse, so the purple arm of the scale is empty. The worst-powered cell with no significant change could only detect a 34pp rise. Runs go1-v0 and go1-v1. report.md · receipt.html

5 worse 1 no significant change 8 safer coloured only at q<0.05, corrected across every condition

LATERAL PUSH, m/s → ↑ FRICTION μ 100 TRIALS PER CELL PER VERSION

Microduck walking, checkpoint 2250 → checkpoint 5999. Hover any cell.

Fig. 3A 14-DoF biped, checkpoint 2250 against checkpoint 5999: 14 conditions of lateral push from 0.55 to 0.7 m/s and floor friction 0.6 and 1, 100 trials per cell per checkpoint, on the same seeds in both, tested by McNemar's test per condition and corrected across all 14. Green: fell significantly less often, 8 conditions. Purple and hatched: significantly more often, 5. The later checkpoint is safer under a hard push and worse under a gentle one, and the ranking flips between 0.6 and 0.625 m/s. The one cell with no significant change could only have resolved a 8pp difference. Runs 20260909T010313Z-5abe and 20260909T010448Z-a6f1. report.md · receipt.html

2026.09
Where a 14-DoF Biped Falls Two checkpoints of a Microduck walking policy under a lateral push: a cliff and a slope, with a crossover between 0.600 and 0.625 m/s. A retrain meant to widen the boundary was worse in 14 of 14 cells. Microducklocomotion read report receipt retrain report
2026.08
Map the Failure Boundary A Go1 locomotion policy across 400 conditions of floor friction and lateral push. Retrained on the two gaps the map exposed: 60 conditions significantly safer, none worse. Go1locomotion read report receipt code

Empirical evidence under a stated test envelope, not formal verification. Conditions outside the envelope were not tested; conditions inside it can only resolve effects at or above the reported MDE.