Claims

A claim says one thing that could be shown false: “the crop endpoint returns the selected region”, “the balance migration preserves row counts”. It is the unit Certus verifies. A pull request usually raises several.

Each claim carries a type, the statement itself, where it came from, a feature key, the frontier it was proved at, a status and a grade. It also carries a set of obligations — the individual things that must hold for the claim to stand. Obligations are what actually get proved, and what a run can leave undone.

A claim outlives the pull request that raised it. Its feature key is what links it to later work, so an obligation raised on one branch can be discharged by a run on another.

Every claim is typed. The type is not a label — it decides which obligations are attached by default and which proofs are admissible. The set is closed at nine.

NewCapability

Something the system could not do before, it can do now.

BehaviorChange

Existing behavior now does something different.

BugFix

A specific defect no longer reproduces.

Preservation

A refactor: BASE and HEAD are equivalent at the nearest stable boundary.

Compatibility

A schema or contract change is backward compatible; old clients still work.

DataMigration

A migration applies, its invariants hold, and rows reconcile and round-trip.

Removal

A capability is gone, and nothing in the impact set still reaches it.

Performance

A metric stays within a declared tolerance against BASE, under identical load.

Security

A sink is unreachable, or an input is demonstrably rejected, on HEAD.

When a change does not fit cleanly, Certus types it to the nearest member and records how well it fit. A low fit is worth correcting by hand: the type governs the obligations, so a mistyped claim gets proved against the wrong requirements.

Certus derives claims from two independent sources and treats the comparison between them as a result in its own right.

declared

From the intent you stated: the pull request body, the linked issue, .certus/spec.md.

observed

From the change graph: what the code actually does differently between BASE and HEAD.

user

Added or corrected by a person in the console.

Matching the two lists produces one of three outcomes, and all three are reported.

declared_and_observed

You said it and the code evidences it. The ordinary case: the claim is proved at the chosen frontier, differentially against BASE.

observed_not_declared

The code changes behavior nobody mentioned. Certus raises the claim anyway and attaches a regression obligation. This is the case that catches a change you did not intend to make.

declared_not_observed

You claimed it and no code evidences it. Either the work is genuinely incomplete — in which case the obligation is deferred as proof debt — or the claim is wrong.

A declared claim is subordinate to an observed one. It only produces obligations if it anchors to real nodes in the change graph, and it can never remove an obligation the change graph created. The pull request body cannot talk Certus out of a proof.

The Claims view is scoped to the run in focus. Each row is one claim: its type, its statement, its status, its grade, and how many of its obligations are still open. Selecting a claim opens its obligations, the oracle results behind each one, and any debt the claim is carrying.

A claim's status uses the same vocabulary as an obligation's, and its grade is the grade of its weakest-proved obligation. A claim is exactly as well established as its worst conjunct.

A claim nobody wrote

It came from the change graph, not from your description. Read the statement. If the behavior is intended, the claim is correct and should be proved; if it is not, you have found an unintended change before it merged.

A claim with nothing proved under it

Check the frontier it was assigned. If no realizable frontier reached it, its obligations are deferred rather than failed and the run is carrying debt — see obligations.

The wrong claim type

Correct it in the console. Default obligations are derived from the type, so the correction changes what the next run tries to prove.

Declared, but not observed

Nothing in the diff supports what you said. Check that the work is actually on this branch before treating the run as broken.