Skip to content

Verification stack

mini-ork's verdicts are anchored on what the code actually did, never on what a model said about it. A model may propose a check or veto a result; it may never approve one. This page describes the machinery behind that rule: the six techniques in the verification stack, the gate registry contract, and how the final verdict is computed.

The three verdict values

Verdict Meaning
PROVEN The evidence establishes the claim
REFUTED The evidence contradicts it, and the evidence is attached
UNVERIFIED The evidence could not be established — an abstention, never a pass

A green test suite alone is not proof: it may be vacuously green (the check cannot fail), inadequate (the suite cannot catch the change), or unrelated (the test does not execute the changed code). Each technique below closes one of those holes.

The six techniques

flowchart TB
  subgraph certify["certify — the Assay oracle"]
    P["reproduction test"] --> D["delta gate red→green"] --> I["metamorphic invariants"]
    I --> R["① relations — veto + rescue"]
    I --> X["② differential — collateral damage"]
  end
  subgraph codefix["run code-fix — verifier and publish"]
    T["test verifier"] --> A["③ suite adequacy — mutation kill rate"]
    A --> L["④ level vector — five independent levels"]
    L --> PUB["publisher"]
  end
  H["⑤ gate hackability audit"] --> PG["promotion gate"]
  E["⑥ equivalence operator"] --> BEH["behavioural verifier"]

① Metamorphic relations

mini_ork/certify/relations.py

The model proposes relations of the form SOURCE input → transform → FOLLOWUP input → relation between outputs (for example: reversing a list leaves its median unchanged). Each relation runs as a real test that calls the code twice. A patch that special-cases the reported input passes SOURCE and breaks FOLLOWUP.

  • Veto: a relation that held on the unpatched code and breaks on the patch turns PROVEN into REFUTED.
  • Rescue: a fix the oracle could not otherwise prove is PROVEN relative to N relations when at least two hold, at least one is repaired, and none is violated.
  • Abstention: a relation that cannot execute never counts as holding.

Knobs: MO_ASSAY_RELATIONS (on), MO_ASSAY_RELATIONS_RESCUE (on), MO_ASSAY_RELATIONS_K (3), MO_ASSAY_RELATIONS_VETO_MIN (1). Evidence is one [assay-relations] {json} stderr line per judgement, and the relations key in the verdict detail.

② Differential check

mini_ork/certify/differential.py

One shared input suite is split into bug_domain (behaviour should change) and preserve (behaviour must not). The same harness runs on base and patch, and canonical-JSON observations are compared by hash. At least two confirmed preserve divergences veto a would-be PROVEN, which prevents one mislabelled input from sinking a correct fix. No anchor means no veto.

Knobs: MO_ASSAY_DIFFERENTIAL (on), MO_ASSAY_DIFFERENTIAL_N (6), MO_ASSAY_DIFFERENTIAL_VETO_MIN (2).

③ Mutation-based suite adequacy

mini_ork/gates/suite_adequacy.py

Deterministic AST mutants are seeded into the changed files on a copy of the repo: comparison flip, arithmetic swap, boolean negation, off-by-one, return None, condition-to-constant. The suite is rerun per mutant; the score is killed / (killed + survived).

Result Effect
ADEQUATE The green stands
INADEQUATE The green is downgraded to UNVERIFIED
UNVERIFIED Baseline red, timed out, canary not detected — downgraded
NOT_APPLICABLE No Python source changed — the green stands

Knobs: MO_SUITE_ADEQUACY (on), MO_SUITE_ADEQUACY_MAX_MUTANTS (12), MO_SUITE_ADEQUACY_MIN_SCORE (0.6), MO_SUITE_ADEQUACY_TIMEOUT_S (300). The report lands as suite_adequacy.json in the run directory, including named survivors as file:line operator original -> mutated.

④ Non-nested level vector

mini_ork/verify/levels.py

Five levels are derived independently and only from execution artifacts:

Level Proven when
applies The implementer reported a non-empty file list
executes The test runner reached test outcomes
target The suite is green and replay proves it exercises the change
preserve No regression, and the suite is not adequacy-unverified
contract The behavioural verifier is PROVEN (or n/a)

Passing a shallow level does not imply a deeper one, and missing evidence makes a level UNVERIFIED, never PROVEN. The publisher acts on the vector:

  • all required levels PROVEN → publish;
  • any REFUTED → fail the run;
  • anything else → withhold the commit without rolling back the fix.

Knob: MO_LEVEL_VECTOR (on). Evidence is levels, levels_reasons, levels_required, levels_ok and levels_decision in verdict.json (or run-verdict.json when the recipe owns it).

⑤ Gate hackability audit

mini_ork/gates/hackability.py

Five fixed "hollow" operators (empty context, dangling evidence, empty document, hollow object, zero-leaf skeleton) run against each gate's real evaluator in a scratch database. hackability = passed_bad / valid_trials. The record is persisted at <db dir>/gate-hackability/<gate_id>.json, and mini-ork promote refuses a promotion that rests on a gate above the threshold.

mini-ork gate-fuzz --hackability --gate <gate_id> [--proposer-lane <lane>] --json

Knobs: MO_GATE_HACKABILITY_N (4), MO_GATE_HACKABILITY_BUDGET_USD (0.50), MO_GATE_HACKABILITY_MAX (0.25), MO_PROMOTION_GATE_HACKABILITY (on).

⑥ Declared equivalence operator

mini_ork/verify/equivalence.py

Every behavioural comparison is relative to a declared operator:

Operator Meaning
exact Byte-identical (default)
set Order-insensitive multiset
canonical Declared ignore_keys, strip_whitespace, numeric
tolerant abs_tol / rel_tol on non-boolean numbers

An unknown operator or invalid rules yield UNVERIFIED on every surface — never a silent exact, never a pass. Every verdict carries an operator stamp, and a REFUTED names the first differing key path.

Declare it in the observable: block of MO_OBSERVABLE_SPEC (equivalence:, expect_body:), or with MO_BEHAV_EQUIVALENCE / MO_BEHAV_EXPECT_BODY. Extend with mini_ork.verify.equivalence.register_operator(name, fn).

Gate registry contract

Gates are executable conditions registered with register_gate_evaluator(type, fn). A gate returns one of three outcomes:

rc Meaning
0 pass — the node may proceed
1 fail — the node is skipped or the run aborts
2 defer — the gate cannot decide; treated as advisory, not a pass

The defer outcome is what keeps an unmeasurable check from becoming a silent green. Fail-open defaults are treated as a defect: an evaluator that cannot see evidence must defer.

Gates fire in the order the workflow declares. The first failure short-circuits unless the gate sets continue_on_fail. Typical built-ins:

Gate type Checks
deterministic_verifier Script exit code and artifact shape
reviewer_gate Structured reviewer JSON (approved: true)
human_gate An operator writes APPROVE to the inbox file
budget_gate Cumulative model cost under the configured cap
scope_gate No file outside the kickoff's scope clause
deployment_gate Schema diff, rollback proof, health probe
liveness_gate Required services and providers respond

Panel and oracle gates

Recipes that judge with multi-model panels add a second layer of gates: coalition (family diversity and correlation), CW-POR (authority capture), panel stability, and synthesis-promote. They compose with the built-ins; a deterministic task class such as code_fix bypasses the LLM-judged promotion gate with reason=deterministic_class. The full wiring, context-JSON shapes and knobs are in the oracle-gates guide in the repository (docs/architecture/oracle-gates-wiring.md).

Turning a technique off

Each has an independent master knob, settable per run or in config/secrets.local.sh:

MO_ASSAY_RELATIONS=0 MO_ASSAY_DIFFERENTIAL=0 mini-ork certify --base base --head fix --issue "..."
MO_SUITE_ADEQUACY=0 MO_LEVEL_VECTOR=0 mini-ork run code-fix kickoff.md
MO_PROMOTION_GATE_HACKABILITY=0 mini-ork promote --candidate <id>

With a knob at 0, verdicts are byte-identical to the pre-feature behaviour. That is intentional: an operator can always attribute a changed verdict to a named technique.

What this does not prove

The stack proves properties of executed checks. It cannot prove a requirement that no test expresses, and it cannot tell a well-formed fabrication from a real deliverable outside a registered completion contract. Where evidence is absent the correct output is UNVERIFIED; treat a green-only claim with suspicion. See Results and benchmarks for measured coverage and failure modes.