Skip to content

Independent verification

Independent verification is evidence produced outside the producer’s own account of the work. BMO uses that phrase for three concrete owners. They share a boundary and do not share a verdict.

Maturity: Implemented, with different entrypoints. Ordinary runs expose verdict grades. bmo synthesize exposes declared hard conditions. A provisioned controller exposes parent outcome from signed adoption plus the original predicate evidence. None of these is implied by the other.

RecordWho writes itWhat a pass means
Verdict gradeRun finalization, from judges declared before the workThe strongest declared judge that actually ran. A grade is evidence strength. It is not correctness and it is not parent acceptance.
Synthesis hard conditionbmo synthesize, from checks, constraints, and validators in the specificationThe measured candidate satisfied the conditions you declared, inside the declared scenarios. The proposal is still ready_for_human. Parent verification remains required.
Parent outcomebmo protected-admission decide-coordinator-outcome on a provisioned controllerThe App accepted one frozen originating objective, or it retained a bounded residual. An adoption signature alone cannot produce acceptance.

A model summary, a tool’s own success line, and a Quality Gate advisory are not substitutes for any row in that table.

Declare the judge before the run, with bmo run --completion-validation-command or a sub-agent validation_command. At finalize, BMO derives a grade from the transcript. A declared command that never ran grades unverified. A grade binds to the content that was judged. Later edits revert the effective grade.

The grade vocabulary, caps, and staleness rules are on Verdict Grades. Use that page to read a run. Use this page when you need to know that the grade did not accept a parent objective or apply a proposal.

A synthesis specification is invalid unless it contains an independent hard condition: a required check, a versioned constraint source, or a blocking or required-coverage validator. Checks run in a fresh scenario directory. Their failure_loss is an operator-declared penalty on an observed failure, not a probability and not a parent predicate.

The selected proposal’s validation summary states that parent verification remains required, including when read-only validators retained warnings or advisories. Applying the proposal rechecks the retained spec, report, diff, and live preimage. That recheck refuses a changed candidate. It still does not record a parent outcome.

Change synthesis is the command reference. Decision-guided software synthesis is the lifecycle, including a parent check that fails after the candidate check has passed. Mutation aftercare is the contract ingest that follows a successful apply. Aftercare is not a second verification pass.

Apply can leave the proposal applied while the parent task is still open. The session change contract owns those validation obligations. Selection and apply do not satisfy them.

Inspect the open rows with /contract-obligations. /contract-rerun and the contract_rerun tool run the pending validation commands. Until that run, verification is pending and the task stays unresolved.

A failed command marks that obligation failed. The task stays unresolved. BMO does not undo the applied files and does not change the proposal back from applied. Rerunning validations does not start a new attempt for an obligation that already failed. A passing command satisfies that obligation. Other unresolved obligations can still block completion.

Review flags written by mutation aftercare are a different pending row. They say a path changed. They are not a parent pass.

For a coordinator objective, the parent decision reads a frozen snapshot: root completion, child coverage, signed adoption, and the original independent predicate evidence. The proof source is the isolated verifier and the preserved image, not the child run’s grade and not the worker’s summary.

Missing, unverifiable, or incomplete evidence becomes a residual on the receipt. The command still stores that receipt and returns a non-zero status. The decision procedure, required pins, and residual names are on Parent outcome.

  • A verdict grade of proof or constructed_check on a child run.
  • A synthesis disposition of candidate_ready.
  • A Patch Proposal status of accepted or applied.
  • A Quality Gate pass.
  • An auto-checkpoint commit.
  • A conceptual diagram on the proof gallery.

Each of those can be true while parent verification is still required, still residual, or still unavailable because the controller is not provisioned.

Synthesis selection leaves parent completion untouched. Proposal acceptance and application do not discharge an existing parent validation obligation; its own validation command can still fail after the candidate check passes. The exact proposal and parent-validation fixtures are in the maintainer evidence mapping. The rerun entrypoints are /contract-rerun and contract_rerun. The parent receipt’s proof source is evaluateCoordinatorParentOutcomeInTx in internal/app/coordinator_parent_outcome.go. Grade derivation is the verdict-grade page and the graded-verdict custody fixtures it cites.

Limits:

  • A hard condition proves only the command, constraint, or validator that ran, against the bytes that were measured.
  • Coverage mapped from a predicate’s prose is a declaration. It does not prove that the command tests that prose.
  • Historical assemblies without a parent-obligation mapping keep their original structural validation and establish no mapped parent coverage.
  • Ordinary bmo run does not call decide-coordinator-outcome.