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.
Three records
Section titled “Three records”| Record | Who writes it | What a pass means |
|---|---|---|
| Verdict grade | Run finalization, from judges declared before the work | The strongest declared judge that actually ran. A grade is evidence strength. It is not correctness and it is not parent acceptance. |
| Synthesis hard condition | bmo synthesize, from checks, constraints, and validators in the specification | The measured candidate satisfied the conditions you declared, inside the declared scenarios. The proposal is still ready_for_human. Parent verification remains required. |
| Parent outcome | bmo protected-admission decide-coordinator-outcome on a provisioned controller | The 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.
Verdict grades stay on the run
Section titled “Verdict grades stay on the run”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.
Synthesis checks stay on the candidate
Section titled “Synthesis checks stay on the candidate”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.
After apply, completion stays pending
Section titled “After apply, completion stays pending”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.
Parent evidence stays on the controller
Section titled “Parent evidence stays on the controller”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.
What does not count
Section titled “What does not count”- A verdict grade of
prooforconstructed_checkon a child run. - A synthesis disposition of
candidate_ready. - A Patch Proposal status of
acceptedorapplied. - 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.
Evidence and limitations
Section titled “Evidence and limitations”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 rundoes not calldecide-coordinator-outcome.