<p align="center"><strong>English</strong> · <a href="README.fr.md">Français</a></p>

<p align="center"><img src="assets/hero.svg" alt="heavnz0r'ProofMill — Every delta. Back to its source." width="100%"></p>
<p align="center">
  <a href="https://github.com/heavnzor/heavnz0r-proofmill/actions/workflows/ci.yml"><img src="https://github.com/heavnzor/heavnz0r-proofmill/actions/workflows/ci.yml/badge.svg" alt="CI"></a>
  <img src="https://img.shields.io/badge/Python-3.11+-70e1ef?style=flat-square&amp;labelColor=151b23" alt="Python 3.11 or newer">
  <img src="https://img.shields.io/badge/engine-DuckDB-70e1ef?style=flat-square&amp;labelColor=151b23" alt="DuckDB">
  <a href="LICENSE"><img src="https://img.shields.io/badge/license-MIT-70e1ef?style=flat-square&amp;labelColor=151b23" alt="MIT license"></a>
</p>
<p align="center"><strong>Your data changed. Your cleaning recipe changed too.<br>Which one moved the number?</strong></p>
<p align="center"><a href="#see-the-proof">Quickstart</a> · <a href="#four-runs-one-explanation">The method</a> · <a href="#ai-proposes-the-engine-verifies">Agent workflow</a> · <a href="docs/method.md">Method & limits</a></p>

---

ProofMill turns CSV/JSONL transformations into **reproducible, row-traceable experiments**. An agent proposes a bounded recipe. DuckDB executes it. A four-way comparison separates the data effect, recipe effect and their interaction, with source hashes and business-key-level evidence.

## See the proof

Requires Python 3.11+ and [uv](https://docs.astral.sh/uv/).

```bash
git clone https://github.com/heavnzor/heavnz0r-proofmill.git
cd heavnz0r-proofmill
uv sync
uv run proofmill demo
```

Open `.proofmill-demo/report.html`. The synthetic invoice demo produces:

<p align="center"><img src="assets/demo.png" width="100%" alt="Actual ProofMill report: four invoice totals and the exact data, recipe and interaction decomposition."></p>

| | Old recipe | New recipe: exclude void invoices |
|---|---:|---:|
| **Old data** | 525 | 450 |
| **New data** | 745 | 600 |

```text
Baseline          525
Data effect      +220
Recipe effect     -75
Interaction       -70
─────────────────────
Current           600      Net change: +75
```

The interaction matters: some new or changed invoices are precisely the ones removed by the new recipe. Counting data and recipe effects alone would overstate the result.

Trace a specific invoice:

```bash
uv run proofmill explain .proofmill-demo/comparison.json --key C
```

Each source reference includes the input SHA-256, one-based data record, inclusion/filter/quarantine status and numeric contribution. A repeated demo requires a fresh `--out` directory.

## Four runs, one explanation

```text
                         OLD RECIPE             NEW RECIPE
                       ┌────────────┐         ┌────────────┐
OLD DATA               │ baseline   │────────→│ recipe only│
                       └─────┬──────┘         └──────┬─────┘
                             │                      │
                       ┌─────▼──────┐         ┌──────▼─────┐
NEW DATA               │ data only  │────────→│ current    │
                       └────────────┘         └────────────┘
```

For the same declared metric and unit:

- `data = F(new data, old recipe) − baseline`
- `recipe = F(old data, new recipe) − baseline`
- `interaction = current − data-only − recipe-only + baseline`
- **`data + recipe + interaction = current − baseline`**

The same conservation identity is checked across row-level contributions. This is an execution decomposition, not proof of real-world business causality.

If one combination cannot execute, the report says **not comparable** and preserves the failure. It does not invent an attribution.

## AI proposes. The engine verifies.

The recipe is a small typed language: **rename**, **cast**, **filter**, then **grouped sum**. Unknown operations and arbitrary SQL are rejected.

```json
{
  "schema": "proofmill.recipe/v1",
  "name": "Paid revenue by region",
  "key": "invoice_id",
  "steps": [
    { "op": "cast", "column": "amount", "to": "decimal" },
    { "op": "filter", "column": "status", "operator": "eq", "value": "paid" }
  ],
  "metric": {
    "id": "invoice-total", "column": "amount",
    "group_by": ["region"], "unit": "EUR"
  }
}
```

An OpenCode/Claude Code agent can inspect the source schema, obtain the recipe JSON Schema, propose and validate a recipe, present its assumptions, then run the accepted comparison. Its model and authentication stay in the client.

Example MCP configuration for OpenCode:

```json
{
  "$schema": "https://opencode.ai/config.json",
  "mcp": {
    "proofmill": {
      "type": "local",
      "command": [
        "uv", "run", "--project", "/path/to/heavnz0r-proofmill",
        "proofmill", "mcp", "--root", "/path/to/data-workspace"
      ]
    }
  }
}
```

Merge and restart OpenCode. Claude Code can register the same stdio command. All tool paths must resolve inside `--root`. The profiling tool returns column names and counts, not raw row samples; an explicit explanation can return a selected record's provenance. The [workflow skill](skills/proofmill/SKILL.md) describes the full loop.

## Use your own snapshots

```bash
uv run proofmill profile exports/old.csv
uv run proofmill schema
uv run proofmill validate recipes/new.json

uv run proofmill compare \
  --old-data exports/old.csv --new-data exports/new.csv \
  --old-recipe recipes/old.json --new-recipe recipes/new.json \
  --out comparison
```

For a single transformation:

```bash
uv run proofmill run --input exports/new.csv --recipe recipes/new.json --out cleaned
```

Each successful cell exports:

```text
data.parquet       transformed records + source record/hash columns
metrics.parquet    grouped totals + contributing record numbers
quarantine.json    rejected values and reasons
receipt.json       recipe, hashes, counts, groups and row provenance
```

A comparison adds `comparison.json` and a self-contained HTML report. Output directories must be new, so a previous result is not silently overwritten.

## Contracts that matter

- A **unique, nonempty source business key** aligns records across snapshots. Duplicate identities block the run.
- Metric identity, unit, grouping columns and source key must agree between recipes.
- Decimal casts use **DECIMAL(38,6)**. Values that would round, overflow, or become non-finite are quarantined; integer casts reject fractional input.
- A source record is a logical CSV/JSONL record, not necessarily a physical file line. Hashes identify the exact input bytes.
- Filtering uses SQL null semantics. Invalid cast rows are quarantined; filtered rows remain traceable with a reason.
- Grouped sums are the v0.1 metric. Flat UTF-8 CSV/JSONL inputs are bounded to 25 MiB and 100,000 records. No joins, OCR, arbitrary SQL, or warehouse connector is implied.
- Receipts and quarantine outputs contain local data. Inspect them before sharing. The demo uses synthetic invoices.

See [the method](docs/method.md) for comparison semantics and precision boundaries.

## Development

```bash
uv sync
uv run ruff check .
uv run pytest
```

Tests exercise the known decomposition, conservation, missing schema, duplicate identities, decimal precision, quarantine, SQL-parameter escaping, Parquet provenance, and MCP transport.

Inspired by the reproducibility and lineage concerns explored by [Hamilton](https://github.com/apache/hamilton) and [OpenLineage](https://github.com/OpenLineage/OpenLineage). ProofMill's focus is the small, inspectable **data × recipe experiment**.

<p align="center"><strong><a href="https://github.com/heavnzor/heavnz0r-racer">Racer</a> builds · <a href="https://github.com/heavnzor/heavnz0r-crashlab">CrashLab</a> challenges · ProofMill explains</strong></p>