Obligations

A claim says what changed. Its obligations say what has to be shown for that to stand. A NewCapability claim, for example, carries four: the capability works at the frontier, it is absent on BASE, its side effect is observable, and its neighbours are unaffected.

Obligations are attached by the engine from the claim's type. The planner may add obligations; it can never remove one. That is checked before a plan runs and again against the evidence afterwards, so a plan cannot quietly drop the requirement it finds hardest.

An obligation is the row that carries a grade and an evidence root. It is also the thing that survives a merge: an obligation raised by one run can be discharged by another.

pending

Planned for this run, not yet judged.

discharged

Proved, at a stated grade, against a named evidence root.

deferred

Cannot be attempted yet — no realizable frontier reaches it. This is what proof debt is made of.

failed

Attempted, and the evidence contradicts it.

waived

A person overrode it. A waiver always records who waived it and why; neither is optional.

inconclusive

It ran and established nothing — the proof was vacuous against BASE, coverage missed the changed code, or repeated runs disagreed.

Movement between them is constrained. Every obligation is created pending. deferred, inconclusive and failed can all go back to pending when a later run attempts them again, and a discharged obligation can become failed if a later run refutes it — that is how Certus reports a regression against something it previously proved. A waiver is final: un-waiving means writing a new waiver, not erasing the old one.

discharged and failed always carry an evidence root and the run that produced it. waived always carries an actor and a reason. The other three carry neither, and the console shows them as such rather than inventing a placeholder.

Proof debt is the set of obligations that are pending or deferred for a feature. It is indexed by feature key, not by pull request, which is what lets it cross branches.

A partial pull request is the ordinary case. Certus verifies what it can at the highest frontier that is realizable today, defers the rest under the feature key with the frontier each is expected to be discharged at, and returns VERIFIED_WITH_DEBT. That is an honest status, not a failure, and it does not block a merge.

When a later change makes that work reachable — the code stops dangling and becomes reachable from a boundary — Certus pulls every deferred obligation for the key back to pending and discharges them at the full frontier. That happens regardless of how small the completing change is. A three-line pull request that wires up a feature inherits the whole proof burden of that feature.

Debt does not expire. There is no timer that converts an open obligation into an accepted one, because an expiry would manufacture consent nobody gave. It is repaid by proving it, or waived by a named person with a stated reason.

The feature key is resolved from a linked issue, a certus:feature= label, a section of .certus/spec.md, or the branch name — in that order. Failing all four, Certus will attach the work to existing open debt if the change graph overlaps it, and flags that inference as correctable. It never invents a key.

Obligations appear under their claim in the Claims view: the requirement, its status, its grade, the oracle that decided it, and the frontier it was proved at. Deferred rows name the frontier they are waiting for. The run's total open debt appears with the claim.

An obligation is only discharged when an oracle was satisfied, the oracle fully covered the requirement, and repeated runs agreed. A satisfied oracle that only covers part of the requirement leaves the obligation inconclusive — partial evidence is reported as partial, not rounded up.

Debt appeared on a pull request that only touched a few lines

Those lines made previously unreachable work reachable, so the feature's deferred obligations came due. The debt is the feature's, not the diff's.

An obligation you never saw planned

Obligations come from the claim type, not from the plan. Change the claim's type if it is wrong; otherwise the requirement is real.

inconclusive on something that looks like it passed

The oracle was satisfied but did not fully cover the requirement, or the run did not execute the changed code, or repeated runs disagreed. The remedy is a better proof, not a code change.

A discharged obligation that is now failed

A later run refuted something an earlier run proved. This is a regression report against your own history.

Debt that will not clear

Check the feature key. Work under a different key is different debt; relink the issue or add the certus:feature= label so the runs join up.