Skip to content

mini-ork certify

Judge whether a change actually fixes the claimed bug, and write a durable certificate of the judgement. certify is independent of a project run: point it at any git repository and any pair of commits.

Usage

mini-ork certify --base <ref> --head <ref> --issue "<what the change claims to fix>"
mini-ork certify --diff <patch> --issue-file <path>

Exactly one of --issue / --issue-file is required. Exactly one of --head / --diff supplies the change.

Options

Flag Default Meaning
--repo <path> . Git repository to certify
--base <ref> HEAD~1 Commit before the change
--head <ref> — Commit with the change; ignored when --diff is given
--diff <path> — Patch file instead of git diff base head
--issue <text> — The claim under test
--issue-file <path> — Read the claim from a file
--image <image> detected Prebuilt runtime image; /testbed is the repo at BASE
--workdir <path> /testbed Repo location inside the image
--mr-n <n> 4 Metamorphic invariants to generate
--out <path> <repo>/.mini-ork/certificates/<id>.json Certificate destination
--json off Print the certificate JSON instead of the summary

What it does

flowchart TD
    P[apply patch to BASE] --> B[build probe from the issue]
    B --> R{probe passes?}
    R -- no --> X[REFUTED]
    R -- yes --> M[generate MR-n invariants]
    M --> E[execute invariants on the patched tree]
    E --> V{pass rate >= 2/3?}
    V -- yes --> OK[PROVEN]
    V -- no --> X
    B -. cannot build .-> U[UNVERIFIED]

The oracle proposes tests; execution decides. Two passes must both hold:

  1. The reproducer works — a probe derived from the issue fails on BASE and passes on the change.
  2. The fix generalises — at least a supermajority (currently 2/3, proven_bar) of generated metamorphic invariants pass on the patched tree.

A patch that special-cases the example in the bug report can pass step 1 and still be refuted by step 2. Differential checks can veto a would-be PROVEN; they never create one.

Exit codes

Code Verdict Meaning
0 PROVEN The change fixes the claim and generalises
1 REFUTED The change is wrong: patch does not apply, probe still fails, or invariants fail
2 UNVERIFIED The oracle could not decide: no patch, no runtime, probe could not be built, too few invariants
64 — Usage error (bad flags, missing --issue)

UNVERIFIED is deliberate: an honest abstention is a valid result, not a failure to be worked around.

The certificate

--out (default <repo>/.mini-ork/certificates/<id>.json) holds a mini-ork.certificate/v1 document. Every key is load-bearing:

Key Content
schema, id, issued_at Format identity and issuance time
verdict, reason The decision and a one-line explanation
repo Path, remote, base SHA, head SHA
change sha256 of the patch and the list of changed files
claim sha256 of the issue text and its first 200 characters
method Oracle name, mr_n, proven_bar, model, image (and context_files when supplied)
evidence Probe source, MR pass rate, per-invariant results
cost USD and LLM call count
duration_s Wall-clock duration
digest SHA-256 over the canonical JSON of every other key

Because the digest covers the canonical form of every other key, changing any field changes the digest. A certificate is evidence, not a claim: the command that produced it, its base, its cost and its result are all in the document.

Examples

# Certify the last commit against its parent
mini-ork certify \
  --base HEAD~1 --head HEAD \
  --issue "median([1,2,3,4]) returns 3 but should return 2.5"

# Certify a saved patch
mini-ork certify --base main --diff candidate.patch --issue-file issue.md

# Generate more invariants and keep the JSON
mini-ork certify --base v1.2.0 --head fix --issue "fixes crash on empty input" \
  --mr-n 8 --out ./cert.json --json

# CI gate
mini-ork certify --base "$BASE_SHA" --head "$HEAD_SHA" --issue-file issue.md || exit 1

Honest limits

  • It proves the change against the claim as executed, on the runtime it built. Behaviour outside the generated inputs is not covered.
  • The invariant generator is the weak point: weak invariants make a weak certificate. --mr-n raises the sample, not the quality.
  • PROVEN means "the evidence passed", not "this is the only correct fix".

See Results and benchmarks for measured behaviour and Certifying a change for the workflow around it.