Tutorials · Lesson 6 of 7

6 · Keep the evidence honest

You'll grade the trace, watch a proof go stale when code changes, and record counter-evidence with a defeater. You need: your governed trace.json.

Grade — the hygiene floor

Grading scores the trace on structure, rationale coverage, negative space, reproducibility, verification evidence, and lineage. Treat it as a floor to clear, not a number to game — a thin trace (no artifacts, no residuals) grades low because it's hard to review.

ponens trace grade trace.json

Freshness — evidence expires

A formal result — a proof, a state-space decomposition, a conformance check — is only as current as the model it ran on. ponens computes a dependency-closure fingerprint of the target, so it can tell you when a result no longer reflects the code:

• Fresh — the target (and everything it uses) is unchanged since the result.
• Stale — the target, or something in its dependency closure, changed after the result. The verdict no longer applies.
• Detached — the target was removed from the model entirely.

Stale/detached results surface as derived residuals, and a goal never resolves "done" over non-fresh evidence. Edit the modelled code, re-enrich, and watch a proved criterion flip to "at risk":

ponens trace enrich   trace.json          # recomputes freshness
ponens trace residuals trace.json --derived   # declared gaps + computed stale/detached proofs

The fix is simple: re-run the affected result against the current model — a fresh result heals it.

Defeaters — counter-evidence

A residual gap says "we didn't check this." A defeater is stronger: it's evidence against a claim — a counterexample, a model that doesn't match the code, a test that doesn't actually establish the property. An open defeater blocks the claim it targets: a Property over that result reads blocked, not done.

ponens trace residual add trace.json --kind defeater \
    --defeater-kind rebuts --target-id fr3-result \
    --statement "Counterexample at amount=0 violates the non-negative invariant" \
    --severity high

--defeater-kind is rebuts (contradicts the conclusion), undermines (attacks the evidence, e.g. model ≠ code), or undercuts (breaks the inference). Traces are immutable — you close a defeater in a successor trace by fixing the code and re-verifying, not by editing this one.

What you learned

• trace grade is a reviewability floor to clear.
• Results are Fresh / Stale / Detached vs. the current model; goals never resolve done over stale evidence.
• A defeater is counter-evidence that blocks a claim — stronger than a gap.