A1.05 · Correct by definition · dive 2
Proven, not asserted
A check can be a claim or a proof. Asserted, someone says it passes; proven, it ran and passed. The closure is made of the proven kind only.
“Correct by definition” follows directly: the definition of done is the set of passing checks, not a separate judgement laid on top. Switch the one check on the right between asserted and proven — only the proven state counts toward the closure.
One check · asserted or proven
A claim is not a proof
Two statements can use the same words and mean opposite things. “Enrol twice creates no duplicate” can be an assertion — someone says it holds — or a proof — a check ran with an already-enrolled learner and observed no duplicate. The closure (A1.05.1) is made of the second kind only. A check that was asserted but never executed is not a member of the closure; it is a claim about the system, and claims drift.
From this the module's title follows. Correct by definition means the definition of done is the set of passing checks. Correctness is not a separate verdict laid on top of the work and then argued about — it is the property of every check in the set having executed and passed. Change the set and you change what done means; run the set and you learn whether it is done. Nothing else is consulted.
- proven
- A check that executed and passed. It has a run behind it: real inputs, the real operation, an observed green result.
- asserted
- A claim that a check passes, with no execution behind it. It may be true; it is not yet a member of the closure.
- correct by definition
- Done is defined as the set of passing checks. There is no second, separate verdict on top.
- drift
- An assertion can fall out of step with the system silently; an execution cannot, because it is re-run against the system itself.
The Author (the Claude agent) builds to the spec; the Operator (the human) accepts against the executed check, never against the sentence. A1.03 set those roles; this dive fixes what the Operator accepts.
The trace is the spine
A proof is only useful if it is reachable from the thing it proves. That reach is the trace: requirement → user story → acceptance check → execution. Every deliverable is reachable from a passing check, and every passing check traces back to a requirement. A gap in the trace is one of two failures: a deliverable nobody proved, or a check that proves nothing required.
Step the marker along the spine to see what each node holds and whether the link to the next is intact. Then break one link — drop the check, or drop its execution — and the readout reports the gap: the requirement reaches no executed check, so the invariant is asserted, not proven.
The traceability spine · step it, then break a link
A proof must be reachable: the trace runs requirement → story → check → execution, and a break anywhere leaves the requirement asserted, not proven.
Proven, not asserted, on the Portal
Take the idempotent sad path of the rung “enrol in a course.” The spec (A1.04.2) states the invariant: an already-enrolled learner who enrols again produces no duplicate. The trace runs from that requirement, through the user story and the Given/When/Then check (A2.04), to an execution that runs the real enrol path and observes the enrolment count stay at one.
Asserted, this invariant is a sentence in a document. Proven, it is a green check with a run behind it
— and only the proven form belongs to the closure. The Author builds Portal.ID.generate/1
and the enrol path to the spec; the Operator accepts against the executed check, not the sentence.
# Asserted: a sentence in the spec. May be true; not a member of the closure. # "enrol twice creates no duplicate" # Proven: the trace ends in an execution against the real enrol path. # requirement → story → check (Given/When/Then) → execution id = Portal.ID.generate(:enrolment) :ok = enrol(learner, course) # Given an already-enrolled learner :ok = enrol(learner, course) # When they enrol again assert count_enrolments(learner, course) == 1 # Then no duplicate — proven (green)
The definition of done is the set of passing (executed, green) checks, joined to requirements by a trace — proven, never merely asserted; correctness is not a separate judgement on top.
“No duplicate enrolment” counts only as an executed Given/When/Then that traces back to the requirement — a spec sentence that was never run is asserted, not proven.
Correct by definition means the definition of done is the set of passing checks — proven, not asserted — with a trace from each requirement to its green execution.
Recap — the set is passing checks
A member of the closure is a proven check: one that executed and passed, with a run behind it, not a claim someone makes. The trace — requirement → story → check → execution — keeps each proof reachable from what it proves; a break anywhere drops the invariant back to asserted. “Correct by definition” is exactly this: done is the set of passing checks, with no separate verdict on top. The last dive shows what re-runs that set mechanically so the verdict repeats — the quality gate.
Next in A1.05: A1.05.3 · Gates — the mechanical quality gates that hold the closure and make “A+” a repeatable result rather than an opinion.
References
Primary sources for execution over assertion, and where it connects in the course.
Sources
- Adzic, G. — Specification by Example — executable specifications: the examples are run, not merely written.
- Humble & Farley — Continuous Delivery — the pipeline proves each candidate by execution before it advances.
- Beck, K. — Extreme Programming Explained — acceptance tests that execute, owned by the customer, as the verdict.
Related in this course
- A1.05 · Correct by definition — the module hub.
- A1.05.1 · The closure — the previous dive.
- A1.05.3 · Gates — the next dive.
- A2.04 · Acceptance criteria with Given/When/Then — the check the trace ends in.
- A1.04 · Two layers — the spec the checks derive from.
- A1 · Why an Agile Agent Workflow — the chapter.