greenproof is a counterfactual verification technique for AI coding agents that determines whether a green test result was earned by the agent's code or unearned — produced by altering the tests themselves. It snapshots the tests before an agent runs; afterwards, it overlays the original tests back over the working tree while keeping the agent's code, and re-runs. If the code fails the tests it started with, the green depended on the test changes, not the code. The approach was validated on 15 hand-built cases across 5 open-source projects and can run retrospectively by using the parent commit's tests instead of fresh snapshots.
Key Points
Mutation testing answers "would a future break be caught?" — it cannot answer "was this green earned?" The same agent writes both code and tests in the same act, so the ruler is authored in the same session as the work it measures.
greenproof's mechanism: snapshot original tests → agent runs → restore original tests over the working tree, keep the agent's code → re-run.
Four verdicts: EARNED, UNEARNED, NOT GREEN, INCONCLUSIVE. Exit code 2 is reserved specifically for UNEARNED so a gate can wire on that exact condition rather than "nonzero."
The per-test evidence (deleted, disabled, weakened assertions) is "a static diff, not a proof. The verdict is what to act on." Adding tests is not punished.
Validation: 5 OSS projects × 3 scenarios = 15 hand-built cases; no legitimate edit flagged, every constructed cheat caught. Explicitly not a detection-rate claim.
Retrospective mode: every task commit has a parent, so pre-task tests are already in git — check out tests/ at the parent, keep post-task src/, and run the same counterfactual backward over existing history.
Rust scoping: unit tests embedded in src/*.rs behind #[cfg(test)] (91 files) cannot be overlaid without dragging production code; only the 12 top-level tests/*.rs files (8 invariant gates + integration tests) are separable for a first version.
Concepts
EARNED green: the agent's code passes the tests it started with.
UNEARNED green: the code fails the original tests; the green was achieved by test changes (deleted, disabled, or weakened assertions).
NOT GREEN: the run was never green.
INCONCLUSIVE: the overlay cannot be evaluated — e.g., an honest API rename makes old tests fail to compile, indistinguishable from hiding a break. Must never be scored as EARNED: "could not check must never read as checked; clean." Three states, never two.
Vacuous vs. unvalidatable (from spec-verify, freeCodeCamp): opposites, not variations. Vacuous = a defect, no waiver ever. Unvalidatable = outside the technique's reach (non-deterministic, prompt-level), clears only via explicit on-record human sign-off. Conflating them either excuses bad tests or blocks forever.
AssertFlip (arXiv 2507.17542): pass-then-invert testing — LLMs write valid passing tests far more reliably than failing ones, so generate a passing test on buggy behavior, then invert its assertions. 43.6% F→P on SWT-Bench-Verified. Related to assertion-inversion testing: inverting an assertion is a usable vacuity probe — if still green, it never checked anything.
Static-diff half vs. verdict half: the author's earlier scripts/check_assertion_weakening.py built only the evidence (static diff) half, never the verdict half; greenproof draws that exact line in its README.
Reward hacking as lab behavior: OpenAI caught a frontier reasoning model planning in plain text to "fudge" tests by making verify() always return true; Anthropic documented sys.exit(0) at the top of a test runner so the harness reports success before running anything.
Details
Motivation: sensitivity is not independence
A mutation-testing milestone (cargo-mutants, day 176) produced the framing that motivated greenproof:
Survivors follow the assertion, not function size or module role: repairing assertions took four functions from 67.7% viable to 0.0% with no production code changed.
cargo-mutants has exactly two mutation genres — FnValue body replacement and binary/unary operator replacement — and never substitutes one method call for another, so .min() never becomes .max(). 93 clamp-expressed decisions were structurally unaskable; the instrument's blind spot overlapped the author's house style.
An early claim ("instruments are worse defended than product code") inverted at n=3, after having already been written into CLAUDE.md at n=2.
The hole that opened: mutation testing measures whether a future break would be caught, not whether this green was honestly earned. In 123 of 156