red-green-proof 0.1.0

A gate that answers, with evidence, whether a change causes a test to pass.

red-green-proof

An agent writes a fix, runs the test, sees green, and reports the change done. Nothing checked that the test was ever red, that it fails for a behavioural reason, or that the fix — rather than a test shaped to fit it — is what turned it green. red-green-proof answers one question with evidence instead of assertion: is there empirical evidence that this change causes this test to pass?

The harness runs the target and the suite in defined states, records what it observed in a machine-readable document, and returns exactly one of three words: proven, unproven, or unstable.

A real run

The bundled leap_year_proven example is a leap-year check missing the Gregorian century rule: is_leap_year(1900) returns True when it should be False. A committed regression test is red at HEAD; the working-tree change adds the century correction.

$ python examples/leap_year_proven/run.py
$ python -m rgp test_leap.py::test_gregorian_century_rule --repo /tmp/rgp-leap-XXXXXXXX
{
  "audit": { "blocking": false, "findings": [] },
  "change": {
    "carried_files": [],
    "diff_sha256": "...",
    "source_files": [ "leap.py" ],
    "test_files": []
  },
  ⋮   (created_at, error, and the full per-gate G1-G5 detail omitted)
  "repo": {
    "branch": "master",
    "dirty": true,
    "head": "b85487653b8c52c3bd7d06f58e5c203328ffae74"
  },
  "schema": "rgp/1",
  "target": {
    "runner": "pytest",
    "runner_version": "pytest 8.4.2",
    "selector": "test_leap.py::test_gregorian_century_rule"
  },
  "verdict": "proven",
  "waiver": null
}

The five gate statuses from that document:

G1 pass  (assertion)   red at HEAD: assert True is False on the 1900 case
G2 pass  (assertion)   the red is behavioural, not a failure to collect or import
G3 pass  (none)        the target passes against the working-tree fix
G4 pass                no baseline-passing test regressed
G5 pass  (assertion)   revert leap.py, keep the test: red again -> the fix is causal

The output above is real (pytest 8.4.2 / Python 3.12.4 on Windows), with the per-gate detail elided; the --repo path is a temp directory and changes each run. The full JSON is written to the proof's .rgproof/ directory.

The five gates

All five must pass, in order; the first that does not is terminal and the verdict is unproven (or unstable if a sampled gate's runs disagree).

• G1 RED-EXISTS — the target test does not pass against the baseline (HEAD).
• G2 RED-VALID — that failure is behavioural (an assertion or an application error), not a test that failed to load, import, or was skipped.
• G3 GREEN — the target passes against your working tree.
• G4 NO-COLLATERAL — no test that passed at baseline fails against the working tree.
• G5 CAUSALITY — with your source change reverted but your test kept, the target fails again, behaviourally. This is the gate that rejects a test which passes regardless of the change.

G1 and G5 run the target three times ([stability].samples); if the runs disagree the verdict is unstable, never proven. G5 is built in an isolated git worktree, never by mutating your working tree — a stash/reset that is interrupted mid-restore can lose uncommitted work, which is exactly what this tool must not do.

Install and first run

The harness core is standard-library Python (requires Python 3.11+; developed and tested on 3.12.4). It has no runtime dependencies of its own — it needs the test runner of the project you point it at, and the two supported runners are pytest and vitest.

Install the rgp command with pipx (or pip) straight from the repository:

pipx install git+https://github.com/ismaellnog/red-green-proof.git
# or, into the current environment:
python -m pip install git+https://github.com/ismaellnog/red-green-proof.git

Then point it at a git repository whose working tree holds the change under proof:

rgp <selector> --repo <path-to-repo>

<selector> is a single test, e.g. tests/test_billing.py::test_prorates_mid_cycle. The repository must be a git repo with a dirty working tree (the change under proof) and the target test must exist at HEAD. Full CLI (rgp, or the equivalent python -m rgp from a source checkout):

rgp [-h] [--repo REPO] [--waiver WAIVER] selector

To try the bundled examples from a clone instead of installing:

git clone https://github.com/ismaellnog/red-green-proof.git
cd red-green-proof
python -m pip install pytest        # the runner the examples use
python examples/leap_year_proven/run.py   # ends in "verdict": "proven"

--waiver REASON waives only G5 and forces unproven (see Configuration). A completed run exits 0 whatever the verdict; a preflight or worktree abort (bad selector, clean tree, unsplittable change) exits 2 with an error object and no gate statuses.

What it does not do

Verbatim from CONTRACT.md §8:

• Generating tests. The skill judges tests; it does not write them.
• Measuring coverage. Coverage answers a different question.
• Behavioural parity for large refactors. Separate problem, separate tool.
• Proving absence of bugs. The skill proves one specific coupling, nothing wider.
• Replacing CI. The skill runs at authoring time and produces an artifact CI can check.

Known limitations

• Evidence is trust-on-execution, not cryptographic proof. The rgp/1 document records what the harness observed when it ran (CONTRACT §5). It is not signed, and it does not defend against a party who controls the harness or the machine it runs on. It replaces an unchecked claim with a checked observation; it does not make that observation unforgeable.

• Only pytest and vitest are supported. Each has an adapter backed by fixtures for all nine failure outcomes (docs/adapters.md §8-§9). CONTRACT.md §7 also names jest and go test, but those adapters are not built: the runners were not installable in the build environment, and an adapter with no fixture is not merged. Do not expect them to work.

• ADV-001 residual — a non-empty change plus a git-ignored dependency can still confound G5. G5 assumes the only difference between your working tree and its synthetic tree is the reverted source. That assumption is false for working-tree content git omits (git-ignored or untracked files): such content is present in your tree and absent in the synthetic checkout, and its absence is attributed to the revert. The source_files == [] (test-only change) case is closed — it can never reach proven — but with a non-empty source change an attacker could, in principle, place the real dependency in a git-ignored file and let a trivial classified edit take the credit. Reproduction and the full write-up: docs/adversarial-findings.md (ADV-001), fixtures under fixtures/adversarial/adv-001-hidden-gitignored-dep/.

• A blocking audit finding does not downgrade a proven verdict. The static tautology audit runs and its findings are recorded in audit.findings (CONTRACT §5.1). But the verdict is a pure function of the gate statuses, so a target that provably passes while asserting nothing can still be proven with audit.blocking == true. Whether a blocking hollowness finding should downgrade the verdict is an open question for the contract owner (docs/adversarial-findings.md, ADV-002 handoff). Today the audit is advisory.

Configuration

rgp.toml at the repository root. Every key below is optional; a repository with no rgp.toml behaves as if these defaults were in effect. The file in this repository documents each key inline.

Key	Default	Meaning
[runner].name	"pytest"	The runner adapter. Supported: "pytest", "vitest".
[runner].command	[]	Explicit argv overriding the adapter's canonical invocation.
[runner].timeout_seconds	120	Per-invocation bound; an over-run is classified timeout and never satisfies G1.
[patterns].test	["tests/**/*.py", "**/test_*.py", "**/*_test.py"]	Globs that classify a changed file as a test (retained in G5).
[patterns].source	["**/*.py"]	Globs that classify a changed file as source (reverted in G5). A changed file matching neither list is a hard error — classification is never guessed.
[patterns].carry	[]	Non-test files carried verbatim into G5's synthetic state. Each is a hole in the guarantee and is recorded in change.carried_files.
[scope].suite	"full"	G4 suite scope. "full" runs the whole suite at baseline and at the working tree.
[scope].select	[]	When suite is narrowed, the globs selecting in-scope tests. Recorded in gates.G4.collateral.scope.
[stability].samples	3	Times G1 and G5 sample the target. Divergence yields unstable; there is no majority rule. Values below 3 are discouraged.
[evidence].dir	".rgproof"	Where the evidence JSON and its output sidecars are written. Git-ignored by default.
[evidence].excerpt_bytes	4096	Maximum size of each gate's output_excerpt; truncated verbatim, never summarised.
[worktree].dependencies	"reuse"	How G5's worktree obtains dependencies. "reuse" shares the primary tree's environment.

Waivers. Some legitimate changes cannot satisfy G5 — a dependency bump, a configuration-only change, a pure refactor with no behavioural delta. Pass --waiver "<reason>"; the reason is recorded, G5 is written skipped, and the verdict is forced to unproven. A waiver never masks a G1-G4 failure and never yields proven. Waived is a visible state, not a pass.

Further reading

• CONTRACT.md — the normative specification (gates, evidence schema, non-goals).
• SKILL.md — the authoring procedure: write the failing test first, observe each state.
• docs/skill-install.md — installing SKILL.md as an agent skill (Claude Code and generic).
• docs/adapters.md — the observed per-runner behaviour, each claim backed by a fixture.
• docs/adversarial-findings.md — the adversary pass and its residual findings.
• docs/bootstrap.md — what was accepted before the harness could prove itself.
• SECURITY.md — how to report a way to obtain proven without a real fix.
• CONTRIBUTING.md — the one rule: never encode an unobserved claim about a runner.

Licensed under Apache-2.0 (LICENSE).