Appendix A — MAGE Engineering Stacks

A.2 Assurance

A.2.1 The Capability

State the engineering obligations, identify the population they apply to, and produce evidence strong enough for each property.

A.2.2 When This Stack Earns Its Keep

Reach for it when the important question shifts from

Did the tests pass?

to

Have we named the relevant obligations, discharged each one appropriately, and shown the population is covered?

That shift arrives whenever a property has to hold across a whole class of things — every mutator, every config field, every seam — and a green suite on a handful of examples no longer settles it.

A.2.3 The Composition

The Assurance stack: a spec becomes a census of obligations, each discharged by appropriate evidence, joined back into coverage A solid load-bearing spine runs top to bottom. SPEC states the obligations. CENSUS establishes what population must be discharged. The discharge move fans into three lanes — TEST for examples, LINT for structure, PROVE for semantics — applied as appropriate to each obligation. The three converge into COVERAGE, which joins every obligation back to its evidence so omissions become visible. Every rung is load-bearing; there is no dashed enhancement in this stack. Discharge each obligation at the semantic level where the property becomes legible — a placement rule folded into prose, not a node. SPEC state the obligations CENSUS what must be discharged? discharge with evidence appropriate to the property TEST examples LINT structure PROVE semantics COVERAGE obligation → evidence load-bearing (required) no dashed rung — every step required Solid path: the load-bearing composition. Discharge an obligation at the level where the property becomes legible.
Figure A.2-1. The assurance composition. A SPEC states the obligation; a CENSUS establishes the population it applies to; discharge fans out to the evidence each obligation deserves — TEST for examples, LINT for structure, PROVE for semantics — and all three lanes converge on COVERAGE, which joins each obligation back to its evidence so omissions show. Solid path: the load-bearing composition.

A.2.4 Constituent Moves

Table A.2-1.
MoveRole
SPECState the obligation.
CENSUSEstablish the population to which it applies.
DISCHARGEApply tests, lints, proofs, or other evidence appropriate to the property.
COVERJoin obligations back to evidence so omissions become visible.

A.2.5 Why These Travel Together

A checker establishes a property only for what it checks. A proof says nothing about obligations left out of its population; a census with no evidence attached merely enumerates debt. Assurance therefore requires both evidence for each obligation and confidence that the relevant population is covered. Use evidence suited to the property—an example test where an example suffices, a structural lint where structure is decisive, a bounded proof where semantics demand it—and map that evidence back to the full population so omissions remain visible.

One rule runs throughout: check an obligation at the semantic level where the property becomes legible. A property about a document's structure belongs in a check that reads structure, not one that scans bytes for it. This determines where the check belongs; it is not another mechanism in the stack.

Mechanisms: census-derived obligations · semantic validator · bounded proof · coverage gate

© James C. Davis, 2026–present