Certifying a change¶
mini-ork certify answers one question about a patch: does this change
actually fix the claimed bug, or does it merely make the reported example
pass? It runs the candidate against generated invariants on a real base and
writes a signed-by-digest certificate you can attach to a review or gate in CI.
It is independent of mini-ork run: point it at any git repository, any two
commits, and an issue statement.
The command¶
mini-ork certify \
--base <commit-before> \
--head <commit-with-fix> \
--issue "median([1, 2, 3, 4]) returns 3; it should return 2.5"
Typical result:
PROVEN the fix holds across 100% of 4 perturbed inputs (supermajority)
change 1 file · sha256 506d0947 claim "median([1,2,3,4]) returns 3; …"
proof .mini-ork/certificates/<id>.json cost $0.03 · 129s
The unit of cost is a certificate: roughly three cents and one to three minutes in the published measurements.
Options¶
| Flag | Default | Meaning |
|---|---|---|
--repo <path> |
. |
Repository to certify |
--base <ref> |
HEAD~1 |
Commit before the change |
--head <ref> |
— | Commit with the change |
--diff <path> |
— | Use this patch file instead of git diff base head |
--issue <text> |
— | What the change claims to fix |
--issue-file <path> |
— | Read the issue from a file |
--image <ref> |
— | Prebuilt image; /testbed is the repo at BASE |
--workdir <path> |
/testbed |
Repository location inside the image |
--mr-n <n> |
4 |
Metamorphic invariants to generate |
--out <path> |
<repo>/.mini-ork/certificates/<id>.json |
Certificate path |
--json |
off | Print the certificate JSON instead of the summary |
Exactly one of --issue or --issue-file is required. --head is ignored
when --diff is supplied.
What the oracle does¶
flowchart LR
R[reproduce the issue<br/>on BASE] --> D{red → green?}
D -- no --> U[UNVERIFIED]
D -- yes --> I[generate invariants<br/>from BASE source]
I --> T[run them on HEAD]
T -->|all hold| P[PROVEN]
T -->|any violated| F[REFUTED]
T -->|cannot execute| U
- Probe-plus — reproduce the issue on the base commit, then on the candidate. A patch that does not turn a red into a green has not fixed anything.
- Invariants — generate
--mr-nmetamorphic relations: a SOURCE input, a transform, a FOLLOWUP input, and a relation between the outputs. Each runs as a real test against both revisions. - Supermajority —
PROVENrequires the invariant pass rate to clear the proven bar (0.667 in the certificate method block), with at least one repaired invariant. - Abstention — anything that cannot execute is
UNVERIFIED, never a pass.
A patch that special-cases the reported input passes the probe and breaks the invariants. That is the case the certificate exists to catch.
The certificate¶
Every outcome writes a mini-ork.certificate/v1 JSON, including short-circuits
and usage failures. The shape:
{
"schema": "mini-ork.certificate/v1",
"id": "<uuid>",
"issued_at": "2026-10-18T12:00:00Z",
"verdict": "PROVEN",
"reason": "the fix holds across 4/4 perturbed inputs",
"repo": {
"path": "/path/to/repo",
"remote": "https://github.com/owner/repo",
"base": "<sha>",
"head": "<sha>"
},
"change": { "sha256": "<patch-digest>", "files": ["src/tally.js"] },
"claim": { "sha256": "<issue-digest>", "summary": "…" },
"method": {
"oracle": "probe+delta+invariants",
"mr_n": 4,
"proven_bar": 0.667,
"model": "<model-id>",
"image": ""
},
"evidence": {
"probe": { "…": "red→green detail" },
"mr_pass_rate": 1.0,
"invariants": ["…"]
},
"cost": { "usd": 0.03, "llm_calls": 12 },
"duration_s": 129,
"digest": "<sha256 over every other key>"
}
The digest is computed over the canonical JSON of every other key
(sort_keys=True, compact separators). Recomputing it must yield the same bytes;
that is what makes the certificate auditable rather than merely recorded.
evidence.invariants is the part reviewers read: each entry names the transform,
the input pair and the observed outputs. A REFUTED certificate names the exact
relation that broke.
Exit codes¶
| Code | Meaning |
|---|---|
0 |
PROVEN |
1 |
REFUTED |
2 |
UNVERIFIED, including an unsupported project or unavailable runtime |
64 |
Bad invocation — unreadable issue file, unresolvable git refs |
The mapping is stable so CI can gate on it:
Contracts and images¶
By default the oracle runs against the local repository. For reproducibility —
and for repos whose dependencies are expensive to install — build an image whose
/testbed holds the repo at BASE:
mini-ork certify \
--base "$BASE_SHA" --head "$HEAD_SHA" \
--issue-file issue.md \
--image ghcr.io/org/repo-testbed:latest \
--workdir /testbed
With an image, dependency setup happens once and every certificate runs in the
same environment. The certificate records the image in method.image.
To certify a patch that is not committed:
Generated invariants¶
--mr-n controls how many relations the model proposes (default 4). More
relations mean more chances to catch a special-case patch, and more execution
time. A relation counts only if it executes; a relation that cannot run is an
abstention, not a success.
The relations and the differential term can be disabled independently:
What it does not prove¶
- It does not prove the fix is the best one. It proves the change generalises across the generated invariants.
- It does not prove the tests are adequate. That is the suite-adequacy
instrument in a
run, not part ofcertify. - It is model-assisted. The invariants are generated; execution decides whether they hold. A relation that cannot be constructed reduces coverage.
- It is not a substitute for review. It answers "does this change fix the claimed bug without breaking related behaviour", not "should this ship".
The measured record — false PROVENs, abstentions, cost — is in Results and benchmarks.