Grades

Grade A is a measurement that means what it says. Grade E is an opinion. Everything in between is how far from the first you had to move to get an answer at all.

A

Exact comparison, stored state, contract conformance, or a metamorphic relation. The cropped region equals the selected region. The row exists with these values. The response conforms to the schema. Resizing twice inverts.

B

Differential or reference. BASE fails and HEAD passes on the identical plan, or the result matches an independent implementation of the same thing.

C

An invariant over generated inputs, a visual geometry check, or a performance tolerance. Balance is conserved across ten thousand cases. The layout boxes are where they should be. The 95th percentile is within ten percent.

D

Several correlated weak observations agreeing — UI text, a network response and a log line all saying the same thing.

E

A model looked at it and said it seemed right. This is the lowest grade there is and it is never the default.

A grade D is three views of one observation, not three observations. Counting sources never promotes a grade; that is the specific move the ladder exists to refuse.

An oracle fully covers an obligation when every observable the obligation names appears in that oracle's inputs and is constrained by its assertion. Oracles that cover part of the requirement still contribute evidence, but they do not set the grade.

Without that rule, one cheap exact check on a corner of a claim would launder an A onto the whole thing. Coverage is computed from the obligation's structured observables, never from the wording of its statement.

The grade of an obligation is the strongest fully covering oracle that was satisfied, then lowered by whichever caps apply. The caps come from how external dependencies were fulfilled, from the claim's type, and from how the environment was realized.

recorded external

Capped at B for new behavior: a recording proves the code did what it did against the traffic you captured. For a Preservation claim there is no cap, because the recording is the control.

stubbed external

Capped at C, and always stated on the verdict. You proved something about your stub as much as about the provider.

generated twin

Capped at C. Where Certus had to generate a stand-in rather than boot the real thing, the proof inherits that distance.

Performance claims

Capped at C. A timing measurement is a tolerance, not an equality.

runtime-only boundary

Capped at B where the boundary was observed at runtime rather than derived from the code.

Live, provider-sandbox and locally substituted dependencies carry no cap. An external with no policy assigned at all does not lower a grade — it makes the frontier unrealizable, and the run is BLOCKED rather than quietly graded down.

Caps are applied when grades are rolled up, not when the plan is written. There is no plan that can route around one.

Within one obligation, the strongest fully covering oracle wins. A weaker oracle running alongside a stronger one subtracts nothing: either the strong one established the statement or it did not.

Across obligations, the weakest wins. A claim's grade is the grade of its worst-proved obligation, and a run's grade is the grade of its worst claim. Obligations are conjunctive — a claim is exactly as well established as its weakest part.

Grades are never averaged. Averaging would let five A-grade formalities carry one E-grade judgement, which is the failure mode the whole ladder is built to prevent.

Your policy sets the minimum grade a merge requires — B by default. When a run misses it, the gate reason names both the grade and the oracle that capped it, so you can see what to improve.

A model judgement is an oracle of the lowest grade. It is admissible as evidence and it is never the default. A claim whose only support is a model judgement is a model-only claim, and by default your policy does not let one pass the merge gate. You can allow them; you have to say so.

Repeatability is handled separately from grade. When repeated runs of the same proof disagree, the obligation goes inconclusive and the count is reported as it happened — 2/3, not rounded and not folded into a lower grade.

A claim graded lower than every oracle under it

A cap applied, or another obligation on the same claim was proved more weakly. The verdict names the capping oracle.

Grade C on a change you proved exactly

Look for a stub or a generated twin in the run's externals. Moving that dependency to a local substitute usually lifts the cap.

Grade B where you expected A

Most often a recorded external on a new-behavior claim. Re-record against the real provider, or move the dependency to a sandbox the provider offers.

No grade at all on a discharged row

No oracle fully covered the obligation. Partial coverage never sets a grade; it leaves the obligation inconclusive.

A merge blocked on grade

The run is below your policy's minimum. Either strengthen the proof, or change the minimum in .certus/policy.yaml deliberately and in a diff people can see.