diff --git a/.github/workflows/standards-build.yml b/.github/workflows/standards-build.yml
index 94350aab6..9dcb3717d 100644
--- a/.github/workflows/standards-build.yml
+++ b/.github/workflows/standards-build.yml
@@ -99,6 +99,15 @@ jobs:
           # it found a test whose assertion could not fail and a branch that
           # could not change a verdict.
           - { name: joulespec-rs,     dir: joulespec/joulespec-rs,                runner: linux, clippy: true, harvest: true }
+          # The same workspace again on a host that has a model checker, to
+          # gate the proof path. The `linux` leg above cannot: with no prover
+          # installed the harvest reports the proof entries as not run, which
+          # is the right behaviour and no gate at all. `proofs: true` runs the
+          # harnesses live and, more importantly, checks that a
+          # counter-artifact still refutes one -- a proof that survives
+          # breaking the thing it proves is a proof of nothing, and that can
+          # decay silently in a way the parser's unit tests cannot see.
+          - { name: joulespec-proofs, dir: joulespec/joulespec-rs,                runner: macos, proofs: true }
           - { name: openpay,          dir: openpay,                               runner: linux-arm64 }
           - { name: joule-code-rs,    dir: joule-code/joule-code-rs,              runner: linux-arm64, z3: true }
           - { name: map-rs,           dir: map/map-rs,                            runner: linux-arm64, conformance: map-conformance }
@@ -330,6 +339,61 @@ jobs:
             exit 1
           fi
 
+      # Both directions of the proof path, live.
+      #
+      # The first run must verify with every declared reachability cover
+      # satisfied -- a checker reports success for an over-constrained harness
+      # in the same words it uses for one that examined everything, so the
+      # cover line is what distinguishes them and is asserted here directly.
+      #
+      # The second run is the one that matters. It narrows the ratio rule's
+      # arithmetic from 128 bits to 64 and requires the prover to FAIL. The
+      # entire test suite passes under that same mutation, so this step is the
+      # only place in CI where the rung above `E3` is shown to be doing
+      # anything.
+      - name: Proof harnesses verify, with every cover reached
+        if: matrix.proofs
+        working-directory: ${{ matrix.dir }}
+        run: |
+          set -euo pipefail
+          export PATH="$HOME/.cargo/bin:$PATH"
+          cargo kani --version
+          for h in the_ratio_rule_is_total_over_every_input \
+                   widening_a_set_can_only_lower_its_cap; do
+            echo "== $h =="
+            out="$(cargo kani -p joulespec-core --harness "$h" 2>&1)"
+            echo "$out" | grep -E '^ \*\* |^VERIFICATION'
+            echo "$out" | grep -q '^VERIFICATION:- SUCCESSFUL' \
+              || { echo "$h did not verify"; exit 1; }
+            # "N of M cover properties satisfied". Both numbers are read with
+            # their own expression rather than by splitting one capture, so
+            # the gate does not depend on the shell's word-splitting rules.
+            line="$(echo "$out" | grep -E '^ \*\* [0-9]+ of [0-9]+ cover properties satisfied$' || true)"
+            [ -n "$line" ] || { echo "$h declared no cover"; exit 1; }
+            got="$(echo "$line" | sed -E 's/^ \*\* ([0-9]+) of ([0-9]+) .*$/\1/')"
+            want="$(echo "$line" | sed -E 's/^ \*\* ([0-9]+) of ([0-9]+) .*$/\2/')"
+            [ "$got" = "$want" ] \
+              || { echo "$h: only $got of $want covers reached -- proved over an empty domain"; exit 1; }
+          done
+      - name: A counter-artifact still refutes a proof
+        if: matrix.proofs
+        working-directory: ${{ matrix.dir }}
+        run: |
+          set -euo pipefail
+          export PATH="$HOME/.cargo/bin:$PATH"
+          f=crates/joulespec-core/src/conform.rs
+          before="$(grep -c 'u128::from(part)' "$f")"
+          [ "$before" = "1" ] || { echo "expected one anchor, found $before"; exit 1; }
+          trap 'git checkout -- "$f"' EXIT
+          sed -i.ci -e 's|^    Some(((u128::from(part).*$|    Some((part * 1_000_000) / total)|' "$f"
+          rm -f "$f.ci"
+          grep -q 'u128::from(part)' "$f" && { echo "the mutation did not apply"; exit 1; }
+          echo "mutation applied: the scale is now computed in 64 bits"
+          out="$(cargo kani -p joulespec-core --harness the_ratio_rule_is_total_over_every_input 2>&1 || true)"
+          echo "$out" | grep -E '^ \*\* |^VERIFICATION'
+          echo "$out" | grep -q '^VERIFICATION:- FAILED' \
+            || { echo "the prover did not refute an overflowing ratio rule"; exit 1; }
+
       # The NVML backends sit behind features no workspace member enables
       # (jcp-energy `nvml`, eoc-meter `cuda`, jouleclaw-energy `nvml`), so the
       # step above never compiles them, let alone runs their tests. Here they
diff --git a/README.md b/README.md
index e2f0444a9..aff50bc8d 100644
--- a/README.md
+++ b/README.md
@@ -185,7 +185,7 @@ derived from the evidence and never from a verdict handed in, so every claim in
 one is reproducible by anyone holding the same inputs.
 
 - **Licence:** Apache-2.0 for reference code (see [`joulespec/LICENSE`](joulespec/LICENSE)); CC-BY-4.0 for specification text (see [`joulespec/LICENSE-SPEC`](joulespec/LICENSE-SPEC)).
-- **Status:** v0.2.0-draft.1. `SPEC.md` published, with §9 setting out what it takes from assurance-case structure, certified-airborne traceability, supply-chain provenance levels, mutation testing and carbon-intensity accounting, and what it adds to each; reference workspace `joulespec-rs/` — `joulespec-core` carries obligation-addressed clauses and signed revisions, the graded evidence ladder with oracle anchoring, vacuity and independence computed from key disjointness, the deterministic two-axis evaluator with both minima, the four flag conditions and footprint-aware staleness, the revision partition, and the `joulespec/1` JCR-1 receipt with its per-clause audit. `joulespec-cli` is the reference **producer**: it reads clauses from the published specification document, runs each declared check, runs it again against a declared counter-artifact, and emits a signed witness only at the rung the observations support — distinguishing a check that failed from one that did not compile from one that should not have passed. Two conformance packs: byte-stable wire vectors carrying one witness of every rung plus one bound to a superseded state, and the standard **applied to its own implementation**, where every conformance item of §7 reaches `E3` against a counter-artifact that made its check fail. That exercise found a test whose assertion could not fail and a branch that could not change a verdict, both now fixed; CI gates on it. `cargo test --workspace` green, `cargo clippy --workspace --all-targets` zero warnings and gated in CI.
+- **Status:** v0.3.0-draft.1. `SPEC.md` published, with §9 setting out what it takes from requirements-traceability tooling, assurance-case structure, certified-airborne traceability, supply-chain provenance levels, mutation testing and carbon-intensity accounting, and what it adds to each. The traceability family is the nearest prior art and narrows the claim honestly: it already binds evidence to a requirement by identifier and revision, and its strongest member already requires the covering check to have *run* — so `E2` is independent convergence rather than a contribution. What it leaves open is what this standard closes: the revision is bumped by hand, where an obligation address is computed; and a passing check that asserts nothing still satisfies such a gate, with test quality deferred to human review, where `E3` makes it mechanical. Reference workspace `joulespec-rs/` — `joulespec-core` carries obligation-addressed clauses and signed revisions, the graded evidence ladder with oracle anchoring, vacuity and independence computed from key disjointness, the deterministic two-axis evaluator with both minima, the four flag conditions and footprint-aware staleness, the revision partition, and the `joulespec/1` JCR-1 receipt with its per-clause audit. `joulespec-cli` is the reference **producer**: it reads clauses from the published specification document, runs each declared check, runs it again against a declared counter-artifact, and emits a signed witness only at the rung the observations support — distinguishing a check that failed from one that did not compile from one that should not have passed. It also drives a **model checker** for the `E4` path, where it parses the property table rather than the verdict line: a checker reports success for a harness whose assumptions emptied the domain in the same words it uses for one that examined all of it, so a gate reading the verdict passes vacuous proofs. A budget per harness makes an undecided run a finding instead of a hang. Two conformance packs: byte-stable wire vectors carrying one witness of every rung plus one bound to a superseded state, and the standard **applied to its own implementation**, where every conformance item of §7 reaches `E3` against a counter-artifact that made its check fail, and two items also carry a proof discharged over their whole input domain. That exercise keeps finding real defects inspection missed — a test whose assertion could not fail, a branch that could not change a verdict, and two counter-artifacts silently aimed at text a refactor had moved, which now fails closed before anything runs. It also measured why the top rung exists: the counter-artifact that narrows the ratio rule's arithmetic to 64 bits is invisible to the whole test suite and refuted by the prover at once. `cargo test --workspace` green, `cargo clippy --workspace --all-targets` zero warnings, both gated in CI alongside the harvest and a live proof leg.
 
 ## How this is organised
 
diff --git a/joulespec/README.md b/joulespec/README.md
index a0a9959a6..11618ca99 100644
--- a/joulespec/README.md
+++ b/joulespec/README.md
@@ -289,6 +289,27 @@ and **passed** is a finding: the check cannot see the thing it is about. The
 harvester exits non-zero on findings, so a pipeline can gate on them, and CI
 gates on this one.
 
+It reads **someone else's specification**, not only this one. Requirements
+live in a few conventional shapes — a numbered conformance list, a bulleted
+requirement list, a heading per requirement carrying its identifier — and
+which one a document uses is a fact about that document, so the manifest
+declares it:
+
+```toml
+[spec]
+document = "docs/requirements.md"
+section  = "2. Requirements"
+shape    = "heading-label"     # or bulleted-bold-label; omitted = numbered
+expect_at_least = 14           # the floor still fails closed
+```
+
+Nothing else about the extraction varies, and a heading that states no
+requirement is not read as one — addressing the empty string would create an
+obligation nobody wrote and then grade it. Changing the declared shape moves
+every obligation address, which is correct rather than unfortunate: a
+different extraction describes different obligations. It does mean the shape
+is part of what an auditor needs in order to recompute them.
+
 Three things in the manifest are declared because they are human judgements the
 standard refuses to guess: which check stands for which obligation (the same
 act as formalizing a clause, SPEC §2.6), each check's anchor, and each check's
@@ -306,13 +327,24 @@ single member, and on a one-element footprint `all` and `any` are the same
 function — so mutating the conjunction left the test green, and the conjunction
 was never actually checked. And a guard in `applies_at` could not change a
 single verdict: an `all` over a non-empty footprint against no enumerable parts
-is already false. The guard looked like care. Both are recorded in
+is already false. The guard looked like care.
+
+Extending the standard found a third. Pulling two rules out into named
+functions — so a prover could be asked about them over their whole input
+domain — moved the text two existing counter-artifacts were aimed at, by a
+single indentation level in one case, and both silently stopped describing any
+edit at all. The harvester refused to run, which was right but late, so it now
+validates every anchor before running anything. Tolerating a missing anchor
+would have been the real failure: two clauses would have gone on looking
+falsifiably evidenced while nothing was being mutated.
+
+All of it is recorded in
 [`conformance/v1/README.md`](conformance/v1/README.md), and that is the `E3`
 rung doing the only thing it claims to do.
 
 ## Conformance packs
 
-Two, answering different questions:
+Three, answering different questions:
 
 - [`conformance/v1/vectors/`](conformance/v1/vectors/) — **the certifiable
   surface.** Fixed keys, clauses, witnesses and energy, byte-stable, carrying
@@ -321,10 +353,20 @@ Two, answering different questions:
   Its verdict is the doctrine in miniature: two obligations well evidenced, one
   carrying only the implementer's citation, and the specification therefore
   graded `E0` at `A0`.
-- The self-conformance receipt beside it — **a measurement, not a vector.** Its
-  energy comes from a wall clock, so re-running the harvest produces different
-  bytes. A pack that held measured energy fixed would be publishing a figure
-  nobody measured.
+- [`conformance/v1/evaluation/`](conformance/v1/evaluation/) — **the verdicts,
+  not the bytes.** Round-tripping a receipt says nothing about whether an
+  implementation graded correctly, because the vectors carry one scenario. Each
+  case here is a complete set of evaluation inputs plus the verdict §3
+  requires, chosen so that a plausible but generous implementation disagrees: a
+  mean where a minimum is required, `E3` awarded on a killed counter-artifact
+  whose anchor is unstated, `E4` awarded because a prover succeeded, a witness
+  for a clause's previous wording discarded instead of flagged. Most cases
+  catch over-grading; at least one catches under-grading, because an
+  implementation that graded nothing would pass all the others.
+- The self-conformance receipt beside them — **a measurement, not a vector.**
+  Its energy comes from a wall clock, so re-running the harvest produces
+  different bytes. A pack that held measured energy fixed would be publishing a
+  figure nobody measured.
 
 ## Relation to existing work
 
diff --git a/joulespec/SPEC.md b/joulespec/SPEC.md
index 9e98d4844..2175f6483 100644
--- a/joulespec/SPEC.md
+++ b/joulespec/SPEC.md
@@ -3,7 +3,7 @@
 | | |
 |---|---|
 | **Standard** | joulespec |
-| **Status** | v0.2.0 draft for review |
+| **Status** | v0.3.0 draft for review |
 | **Profile** | `joulespec/1` |
 | **Licence** | Specification text CC-BY-4.0 ([`LICENSE-SPEC`](LICENSE-SPEC)); reference code Apache-2.0 ([`LICENSE`](LICENSE)) |
 | **Reference** | [`joulespec-rs/`](joulespec-rs/) |
@@ -229,6 +229,26 @@ So `E4` requires the statement to have been **refuted** against a named
 counter-model (§2.6), exactly as `E3` requires a check to have failed against
 a counter-artifact. Nothing reaches either rung on a passing run alone.
 
+#### A counter-artifact that does not build has demonstrated nothing
+
+A check that "fails" because the artifact no longer compiles has not shown
+that it can notice the obligation being violated. It has shown that the
+toolchain can notice a broken edit, which was never in doubt. A conforming
+producer MUST distinguish a check that **ran and failed** from one that could
+not run, and MUST NOT credit the second toward `E3`.
+
+The same applies to the absence of a run at all: a check harness that reports
+success having executed no checks is indistinguishable, from its exit status
+alone, from one that executed all of them. A conforming producer MUST observe
+that at least one check ran, and not infer it from a successful exit.
+
+Mutation tooling draws the first line already, reporting mutants that fail to
+compile separately from its results rather than counting them: such a mutant
+is inconclusive about the checks rather than evidence about them. This
+standard needs the distinction for a different reason — not to keep a score
+honest, but because crediting a failed build as a demonstrated failure would
+manufacture falsifiability out of a syntax error.
+
 #### Where the expectation comes from
 
 A check's ability to fail is not only an empirical question. An oracle whose
@@ -307,6 +327,32 @@ discarding it would lose evidence that exists.
 This is the same boundary the family's verification standard draws from the
 other side when it records that a proof is not a specification.
 
+#### What refutes vacuity, for a machine-checked statement
+
+A prover's success verdict does not refute vacuity, and a conforming producer
+MUST NOT treat it as though it had. A verifier reports success for a harness
+whose assumptions have eliminated the states the statement was about, and it
+reports that in the same words it uses for a harness that examined all of
+them. The verdict is therefore the same shape of silence as a test binary that
+runs no tests and exits zero (§2.5).
+
+Refutation requires two observations the verdict does not contain:
+
+1. every reachability cover the harness declares is **satisfied** — each names
+   a state the statement is supposed to be about, and a satisfied cover is a
+   concrete path reaching it; and
+2. a counter-artifact applied to the proved code makes the verification
+   **fail**, with the counterexample standing as the named counter-model.
+
+A harness declaring no cover is `unchecked`, never `refuted`: it has offered
+nothing that distinguishes an examined domain from an empty one. A conforming
+producer MUST raise a flag (§3.4) on such a harness rather than grading it
+quietly — something is wrong with the evidence set, not merely weak about one
+obligation.
+
+The first observation is what the prover was asked; the second is what the
+ladder asks of every rung above `E2`.
+
 ### 2.7 Work
 
 Work is a unit of effort performed against a specification — a coding
@@ -667,6 +713,14 @@ figure nobody measured.
 
 ## 8. The honest limit
 
+**An obligation address depends on how the clause was extracted.** The
+address covers the clause's kind and text, and the text is whatever a producer
+captured from the document. Two producers reading one document under different
+conventions — a numbered list versus a heading per requirement — state
+different obligations about the same prose, and both are behaving correctly. A
+conforming producer MUST therefore disclose the convention it applied, because
+the document alone is not enough to recompute the addresses.
+
 **JouleSpec cannot tell whether a clause says what its author meant.** An
 obligation is addressed, signed and tracked, and it may still be the wrong
 requirement, badly worded, or quietly contradicted by another clause. This
@@ -710,6 +764,30 @@ in the check. Reproduction of a vacuous check reproduces the vacuity.
 cross-specification comparison of microjoules per obligation is not a weaker
 measurement; it is not a measurement.
 
+**`E4` is not uniformly affordable, and the ladder does not say so.** The
+rungs are ordered by what they establish, which says nothing about what they
+cost to reach. Measured on this standard's own implementation, over one
+function and one input domain: the statement that its arithmetic is total was
+discharged in under a tenth of a second, and the statement that its quotient
+is bounded by the scale — which requires reasoning about the output bits of a
+wide division — did not converge in twenty-four minutes.
+
+Changing the *method* moved that wall without removing it. Re-run under a
+solver reasoning with a bitvector theory rather than bit-blasting to a
+propositional problem, the same statement settled most of its conditions
+almost at once and then spent over fifty minutes on one. So the cost is not
+simply a property of the engine either, and an operator cannot expect to buy
+convergence by choosing a different one.
+
+An operator should read two things into that. A budget belongs to a harness
+rather than to a workspace, because one figure cannot be both large enough for
+the statements worth proving and small enough to gate on. And a statement
+reshaped until the prover converges has not become cheaper to prove — it has
+become a different and usually smaller claim, reported in the same words. The
+standard can require the budget to be declared and an overrun to be reported
+as undecided. It cannot tell that a converging statement is the one that
+mattered.
+
 **Two of the results this standard builds on are thinly evidenced.** The
 vacuity rate quoted in §2.5 comes from one industrial verification setting, and
 the oracle-anchoring effect it reports comes from a single-system study by a
@@ -751,10 +829,68 @@ requires both is stating two different things, and should.
 deployment can carry provenance levels for its artifacts and attestation grades
 for its evidence, and they answer different questions.
 
-**Mutation testing** supplies the counter-artifact. §2.5 records why the
-equivalent-mutant problem that makes mutation *scores* contested cannot
-inflate a grade here, and why one killed mutant per obligation is a
-deliberately cheap bar rather than an attempt at a score.
+**Requirements-traceability tooling** is the nearest existing implementation
+of the evaluation in §3, and the closest thing to prior art this standard has.
+Tools in that family address a requirement by an identifier carrying a
+**revision**, and a covering test cites that identifier and revision together.
+Rewording a requirement bumps its revision, at which point citations of the
+old revision stop counting toward coverage. The strongest member of the family
+goes further and reads the test *runner's results*, not the sources: a
+citation on a test that never ran binds nothing, and an obligation counts as
+covered only once a bound test has run and passed.
+
+That is this standard's `E2`, reached independently and from a different
+direction, and it is the best evidence available that the rung is real. `E2`
+is therefore not a contribution here. Two things the family leaves open are:
+
+- **The revision is bumped by hand.** Drift detection depends on an author
+  recognizing that an edit changed a requirement's meaning and incrementing a
+  number. A reworded clause whose revision was not bumped keeps its old
+  evidence, and nothing notices — which is the failure §2.1's computed address
+  exists to remove from human hands. The field identified the right binding and
+  left its trigger to discipline.
+- **The family documents its own limit.** A passing test that asserts nothing
+  still satisfies such a gate, and judging whether a test is worth anything is
+  deferred to a separate human review. §2.5's counter-artifact is that review
+  step, mechanized. This is where this standard departs, and it is the only
+  place at `E2`/`E3` where it does.
+
+**Enforced spec-first agent frameworks** supply discipline the agent cannot
+edit around: a deterministic orchestrator, human approval gates, and tests
+held immutable through the build. Immutability is not falsifiability. An
+immutable test that asserts nothing is immutably vacuous, and preventing an
+agent from weakening a check says nothing about whether that check could ever
+have failed. The two compose cleanly and answer different questions: a
+conforming deployment can hold its checks immutable *and* grade them, and
+should.
+
+**The field states this gap about itself.** Comparative assessments of the
+spec-driven frameworks find none covering the full span of a process taxonomy,
+name excessive trust in generated artifacts as a standing risk, and report an
+absence of benchmarks for evaluating the process as a whole. Requirements
+engineering work on the same shift records that the field lacks evaluation
+frameworks for verifying requirements satisfaction and traceability. Current
+tool comparisons list verification as absent in the leading frameworks,
+enforcement as convention, and every drift reconciliation as a manual command
+someone has to remember to run. This standard does not supply the missing
+benchmark. It supplies the quantity a benchmark would have to measure.
+
+**Mutation testing** supplies the counter-artifact, and mature engines exist
+for generating mutants automatically. §2.5 records why the equivalent-mutant
+problem that makes mutation *scores* contested cannot inflate a grade here,
+and why one killed mutant per obligation is a deliberately cheap bar rather
+than an attempt at a score.
+
+A **declared** counter-artifact is preferred here to a generated score, for
+reasons of addressing rather than quality. A score is an aggregate over
+mutants no particular obligation is about, so it cannot say which clause is
+falsifiably evidenced; its denominator moves when unrelated code changes; and
+a surviving equivalent mutant is indistinguishable from a genuine gap. A
+counter-artifact named against one obligation answers one question — can this
+check notice this clause being violated — and answers it per clause, which is
+the granularity everything downstream of §3 needs. The two are compatible: an
+engine is a good way to *find* a candidate counter-artifact that a manifest
+then names.
 
 **Carbon-intensity accounting for software** is an international standard
 expressing emissions as a rate per functional unit of work. §5.3 has the same
@@ -764,11 +900,23 @@ outside its scope, which is the quantity measured here. The two are
 complementary rather than competing, and a deployment reporting both is
 reporting a system's operation and its construction.
 
-What is new here is the conjunction: an obligation address that survives
-renaming and breaks on rewording, a grade that requires a demonstrated
-failure above `E2`, a footprint that keeps evidence alive across unrelated
-change, and a per-obligation energy figure. Each part has precedent; the
-combination is what makes conformance a measured quantity rather than a claim.
+So the claim worth making is narrow. Binding evidence to a requirement is
+established practice; requiring that the bound check actually ran is too. What
+is left, once the nearest neighbours are given their due, is four things and
+their conjunction:
+
+- an obligation **address** rather than a hand-maintained revision, so that
+  rewording invalidates evidence whether or not anyone noticed the rewording;
+- a **demonstrated failure** required above `E2`, replacing the human review
+  step that the traceability family explicitly defers;
+- a **footprint**, so that evidence survives change it did not depend on and
+  the previous point stays affordable; and
+- a **per-obligation energy figure**, which nothing in either family reports.
+
+Each part has precedent except the last. The combination is what makes
+conformance a measured quantity rather than a claim, and the measurement is
+the point: the field's own assessments say it lacks the means to evaluate
+whether a specification was satisfied, not that it lacks opinions about it.
 
 ---
 
diff --git a/joulespec/conformance/v1/README.md b/joulespec/conformance/v1/README.md
index 8ca7c5615..7fe7837f2 100644
--- a/joulespec/conformance/v1/README.md
+++ b/joulespec/conformance/v1/README.md
@@ -33,6 +33,18 @@ JOULESPEC_GEN_VECTORS=1 cargo test -p joulespec-core --test vectors
 Without that variable the test asserts the committed bytes, so a change to the
 wire format fails in CI rather than shipping.
 
+## `evaluation/` — the verdicts, not the bytes
+
+The vectors certify that an implementation round-trips a receipt's **bytes**.
+They say nothing about whether it reaches the right **verdict**, because they
+carry one scenario. [`evaluation/`](evaluation) is the other half: cases whose
+correct answer a too-generous implementation gets wrong, each with the inputs
+to evaluate and the verdict §3 requires. Its
+[README](evaluation/README.md) says what each trap is and why the expectations
+are written by hand rather than read back out of this implementation — a
+distinction that caught seven authoring errors of mine while it was being
+built.
+
 ## The self-conformance record
 
 `spec.json`, `witnesses.json`, `state.json`, `receipt.cbor` and `receipt.json`
@@ -54,6 +66,82 @@ declares a **counter-artifact**: a one-occurrence edit that should make that
 check fail. The harvester applies it, runs the check, requires a *failure*,
 and reverts. Only then does the witness reach `E3`.
 
+### Proofs, beside the checks
+
+Two obligations also carry a **proof**, discharged by a bit-precise model
+checker over the whole input domain rather than at sampled points. A proof
+entry is distinguished in the manifest by carrying a `formalization` — the
+binding from clause prose to formal statement — because §2.6 forbids a
+producer formalizing a clause itself, and making the binding the thing that
+selects the prover enforces that structurally rather than by a check someone
+could forget.
+
+The prover path refuses the same way the check path does, one rung up:
+
+| Observed | Read as |
+|---|---|
+| verified, every declared cover satisfied | the statement holds over a non-empty domain |
+| verified, a cover never reached | **a finding** — proved over a domain the harness's own assumptions emptied |
+| a property violated | the refutation a counter-artifact is applied to obtain |
+| undecided, or killed by the budget | **a finding** — neither verdict, and never credited as either |
+
+The second row is why the producer parses the property table instead of the
+verdict line. A model checker reports success for an over-constrained harness
+in the same words it uses for one that examined everything, so a gate reading
+the verdict alone passes vacuous proofs. The fourth row is why each harness
+carries a wall-clock budget: a solver asked a question it cannot settle does
+not say so, it keeps going.
+
+Both proofs sit at **`E2`, not `E4`**, and the report says so in those words.
+Their statements were refuted against a counter-artifact, so the vacuity axis
+is satisfied; what is missing is an independently cross-checked formalization.
+Nobody but the author has confirmed that either statement says what its clause
+says, and §2.6 caps that at `E2`. The rung is reachable by this producer — it
+needs a second party, not more code.
+
+### What the proofs cost, and what they caught
+
+The reason the ladder has a rung above `E3` is visible here as a measurement
+rather than an argument. The counter-artifact on C7 narrows the ratio rule's
+arithmetic from 128 to 64 bits, where a large input overflows the
+parts-per-million scale:
+
+- the **entire test suite passes** under that mutation — 85 tests, none of
+  which reaches an input above roughly `u64::MAX / 1_000_000`;
+- the **prover refutes it** in a fraction of a second.
+
+That is `E3` and `E4` disagreeing on our own code, in the direction the ladder
+predicts.
+
+The cost is not uniform, and that matters more for budgeting than it might
+seem. The same function, the same input domain and the same solver gave:
+
+- **the statement that its arithmetic is total** — no overflow, no division by
+  zero — discharged in under a tenth of a second;
+- **the statement that its quotient is bounded by the scale** — which requires
+  reasoning about the output bits of a 128-bit division — *did not converge*
+  in twenty-four minutes.
+
+Naming a solver that reasons with a bitvector theory instead of bit-blasting
+moved that wall without removing it: it settled four of the statement's
+conditions in about eight seconds and then spent over fifty minutes on the
+fifth. The harness is kept, behind a `cfg` nobody sets so an ordinary run does
+not hang on it, as the reproducible record of a negative result.
+
+Only the first is claimed. The second is named in the harness's own
+documentation as deliberately unstated, because a harness that quietly
+narrowed its domain until it converged would report exactly the same success
+over a much smaller claim. The lesson for an operator is that the top rung's
+affordability is a property of the statement and of the method together,
+neither of which the ladder mentions — which is why the budget is declared per
+harness and not once for a workspace.
+
+A second lesson, from the same run: a wall-clock wrapper around the prover is
+not enough. Both abandoned runs outlived the `timeout` that was supposed to
+bound them, because the prover is a driver that spawns the checker and a
+timeout reaches only the driver. The producer kills the **process group**,
+which is why its budget works where the shell's did not.
+
 **These receipts are not reproducible, by construction.** Their energy figures
 come from a wall clock, graded `Estimator`, because no meter is wired to this
 harness yet. Re-running the harvest produces different microjoules and
@@ -80,5 +168,18 @@ correctly reported as a check that cannot see its subject. The distinction
 between those two readings is the operator's to make, and the harvester
 reports what it observed rather than guessing which it is.
 
+A fourth finding came from extending this standard rather than from running
+it. Extracting two rules into named functions — so a prover could be asked
+about them — moved the text that two existing counter-artifacts were aimed at,
+by one indentation level in one case. Both mutations silently stopped
+describing any edit at all. The harvester refused to run, which is the correct
+outcome but a late one, so it now validates every counter-artifact's anchor
+**before** running anything. Tolerating a missing anchor would have been the
+real failure: two clauses would have gone on looking falsifiably evidenced
+while nothing was being mutated.
+
 The harvester exits non-zero on a finding, so a pipeline can gate on it. CI
-runs it on every change to this standard.
+runs it on every change to this standard. Where no model checker is installed
+the proof entries are reported as not run — an absence, not a pass — and the
+clauses fall back to their check evidence. The prover's own output parsing is
+covered by tests in CI regardless, including both traps above.
diff --git a/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/expect.json b/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/expect.json
new file mode 100644
index 000000000..6d6594e1c
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/expect.json
@@ -0,0 +1,21 @@
+{
+  "intent": "One obligation at E3, one at E0.",
+  "trap": "Averaging the rungs, or reporting the best, gives E3 or E1 where §3.2 requires the minimum.",
+  "direction": "over-grading",
+  "grade": "cited",
+  "attestation": "self-attested",
+  "flags": [],
+  "clauses": [
+    {
+      "label": "C1",
+      "grade": "falsifiable",
+      "stale": 0
+    },
+    {
+      "label": "C2",
+      "grade": "cited",
+      "stale": 0
+    }
+  ],
+  "conformant_at_e3": false
+}
diff --git a/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/spec.json b/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/spec.json
new file mode 100644
index 000000000..af12c7500
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/spec.json
@@ -0,0 +1,120 @@
+{
+  "spec": {
+    "profile": "joulespec/1",
+    "alg": 1,
+    "intent": "A corpus case: the clauses exist to be graded, not to be implemented.",
+    "clauses": [
+      {
+        "label": "C1",
+        "kind": "requirement",
+        "text": "The first obligation is well evidenced."
+      },
+      {
+        "label": "C2",
+        "kind": "requirement",
+        "text": "The second obligation is only claimed."
+      }
+    ],
+    "parent": null,
+    "author": [
+      138,
+      136,
+      227,
+      221,
+      116,
+      9,
+      241,
+      149,
+      253,
+      82,
+      219,
+      45,
+      60,
+      186,
+      93,
+      114,
+      202,
+      103,
+      9,
+      191,
+      29,
+      148,
+      18,
+      27,
+      243,
+      116,
+      136,
+      1,
+      180,
+      15,
+      111,
+      92
+    ]
+  },
+  "sig": [
+    43,
+    42,
+    11,
+    171,
+    119,
+    207,
+    160,
+    61,
+    162,
+    144,
+    245,
+    20,
+    230,
+    204,
+    135,
+    222,
+    27,
+    198,
+    221,
+    151,
+    150,
+    139,
+    70,
+    10,
+    15,
+    59,
+    131,
+    156,
+    246,
+    73,
+    96,
+    74,
+    147,
+    64,
+    46,
+    226,
+    82,
+    95,
+    82,
+    156,
+    208,
+    5,
+    42,
+    73,
+    137,
+    132,
+    140,
+    67,
+    141,
+    40,
+    141,
+    18,
+    4,
+    208,
+    243,
+    54,
+    220,
+    199,
+    96,
+    189,
+    176,
+    84,
+    127,
+    9
+  ]
+}
diff --git a/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/state.json b/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/state.json
new file mode 100644
index 000000000..206d47bb2
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/state.json
@@ -0,0 +1,7 @@
+{
+  "address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
+  "parts": [
+    "b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b",
+    "b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e"
+  ]
+}
diff --git a/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/witnesses.json b/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/witnesses.json
new file mode 100644
index 000000000..a80a163ee
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/witnesses.json
@@ -0,0 +1,239 @@
+[
+  {
+    "witness": {
+      "profile": "joulespec-witness/1",
+      "alg": 1,
+      "spec_id": "b3:cef4d60f560ca59fa02f71adc7c734f9a84f3f69278c629aec9d912d6a5ffab1",
+      "obligation": "b3:d35a2f3ff28be1718133d7457d98466bebd16f5ee260fab64d4482ca33c5176d",
+      "artifact": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
+      "footprint": [],
+      "evidence": {
+        "kind": "falsifiable",
+        "check": "a_named_check",
+        "anchor": "specification",
+        "counter": "b3:e34e236da4740e55ec1aaabd0d1bcfe74529fa93cde433c07966669601d72eb5"
+      },
+      "energy": {
+        "uj": 1000,
+        "provenance": "estimator"
+      },
+      "author": [
+        129,
+        57,
+        119,
+        14,
+        168,
+        125,
+        23,
+        95,
+        86,
+        163,
+        84,
+        102,
+        195,
+        76,
+        126,
+        204,
+        203,
+        141,
+        138,
+        145,
+        180,
+        238,
+        55,
+        162,
+        93,
+        246,
+        15,
+        91,
+        143,
+        201,
+        179,
+        148
+      ]
+    },
+    "sig": [
+      229,
+      32,
+      61,
+      59,
+      203,
+      181,
+      133,
+      53,
+      241,
+      40,
+      78,
+      229,
+      150,
+      186,
+      241,
+      117,
+      143,
+      128,
+      227,
+      64,
+      75,
+      163,
+      95,
+      205,
+      36,
+      126,
+      169,
+      34,
+      103,
+      10,
+      36,
+      35,
+      230,
+      154,
+      132,
+      78,
+      97,
+      217,
+      194,
+      209,
+      117,
+      213,
+      48,
+      254,
+      92,
+      117,
+      217,
+      242,
+      207,
+      228,
+      41,
+      161,
+      153,
+      169,
+      92,
+      104,
+      85,
+      94,
+      59,
+      249,
+      116,
+      220,
+      163,
+      0
+    ]
+  },
+  {
+    "witness": {
+      "profile": "joulespec-witness/1",
+      "alg": 1,
+      "spec_id": "b3:cef4d60f560ca59fa02f71adc7c734f9a84f3f69278c629aec9d912d6a5ffab1",
+      "obligation": "b3:03ad09e8fb25c85b62516d1d12ad26d9674b06713e215790fff2fc4a91e85ec5",
+      "artifact": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
+      "footprint": [],
+      "evidence": {
+        "kind": "cited"
+      },
+      "energy": {
+        "uj": 1000,
+        "provenance": "estimator"
+      },
+      "author": [
+        202,
+        147,
+        172,
+        23,
+        5,
+        24,
+        112,
+        113,
+        214,
+        123,
+        131,
+        199,
+        255,
+        14,
+        254,
+        129,
+        8,
+        232,
+        236,
+        69,
+        48,
+        87,
+        93,
+        119,
+        38,
+        135,
+        147,
+        51,
+        219,
+        218,
+        190,
+        124
+      ]
+    },
+    "sig": [
+      226,
+      48,
+      153,
+      132,
+      46,
+      194,
+      110,
+      25,
+      109,
+      194,
+      27,
+      217,
+      139,
+      66,
+      55,
+      44,
+      152,
+      188,
+      42,
+      27,
+      147,
+      187,
+      97,
+      244,
+      73,
+      234,
+      205,
+      195,
+      138,
+      100,
+      51,
+      62,
+      84,
+      123,
+      198,
+      111,
+      243,
+      234,
+      41,
+      163,
+      114,
+      94,
+      156,
+      250,
+      146,
+      1,
+      43,
+      183,
+      202,
+      107,
+      44,
+      123,
+      226,
+      54,
+      17,
+      42,
+      106,
+      218,
+      127,
+      124,
+      202,
+      0,
+      94,
+      7
+    ]
+  }
+]
diff --git a/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/work.json b/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/work.json
new file mode 100644
index 000000000..07c240e2e
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/work.json
@@ -0,0 +1,46 @@
+[
+  {
+    "id": "b3:78ec055c7256fd5dfc25ab756441f9895afef0dc4a35e15c05dd8a07ae8e0e35",
+    "cites": [
+      "b3:d35a2f3ff28be1718133d7457d98466bebd16f5ee260fab64d4482ca33c5176d"
+    ],
+    "energy": {
+      "uj": 500000,
+      "provenance": "estimator"
+    },
+    "author": [
+      202,
+      147,
+      172,
+      23,
+      5,
+      24,
+      112,
+      113,
+      214,
+      123,
+      131,
+      199,
+      255,
+      14,
+      254,
+      129,
+      8,
+      232,
+      236,
+      69,
+      48,
+      87,
+      93,
+      119,
+      38,
+      135,
+      147,
+      51,
+      219,
+      218,
+      190,
+      124
+    ]
+  }
+]
diff --git a/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/expect.json b/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/expect.json
new file mode 100644
index 000000000..6bbda26a6
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/expect.json
@@ -0,0 +1,21 @@
+{
+  "intent": "One obligation at E3; the other has no witness.",
+  "trap": "Skipping the unevidenced clause and grading the rest gives E3. Absence orders below every rung, so the grade is absent — not E0, which would claim a citation nobody made.",
+  "direction": "over-grading",
+  "grade": null,
+  "attestation": null,
+  "flags": [],
+  "clauses": [
+    {
+      "label": "C1",
+      "grade": "falsifiable",
+      "stale": 0
+    },
+    {
+      "label": "C2",
+      "grade": null,
+      "stale": 0
+    }
+  ],
+  "conformant_at_e3": false
+}
diff --git a/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/spec.json b/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/spec.json
new file mode 100644
index 000000000..eae7fed2c
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/spec.json
@@ -0,0 +1,120 @@
+{
+  "spec": {
+    "profile": "joulespec/1",
+    "alg": 1,
+    "intent": "A corpus case: the clauses exist to be graded, not to be implemented.",
+    "clauses": [
+      {
+        "label": "C1",
+        "kind": "requirement",
+        "text": "The first obligation is well evidenced."
+      },
+      {
+        "label": "C2",
+        "kind": "requirement",
+        "text": "The second obligation has no evidence at all."
+      }
+    ],
+    "parent": null,
+    "author": [
+      138,
+      136,
+      227,
+      221,
+      116,
+      9,
+      241,
+      149,
+      253,
+      82,
+      219,
+      45,
+      60,
+      186,
+      93,
+      114,
+      202,
+      103,
+      9,
+      191,
+      29,
+      148,
+      18,
+      27,
+      243,
+      116,
+      136,
+      1,
+      180,
+      15,
+      111,
+      92
+    ]
+  },
+  "sig": [
+    24,
+    240,
+    18,
+    59,
+    164,
+    67,
+    152,
+    178,
+    106,
+    233,
+    237,
+    196,
+    133,
+    34,
+    134,
+    161,
+    102,
+    182,
+    221,
+    82,
+    197,
+    127,
+    60,
+    87,
+    223,
+    174,
+    33,
+    158,
+    103,
+    38,
+    226,
+    108,
+    133,
+    29,
+    212,
+    31,
+    117,
+    225,
+    176,
+    28,
+    94,
+    209,
+    209,
+    122,
+    27,
+    98,
+    133,
+    254,
+    159,
+    181,
+    235,
+    242,
+    120,
+    166,
+    81,
+    90,
+    146,
+    230,
+    106,
+    126,
+    60,
+    212,
+    181,
+    0
+  ]
+}
diff --git a/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/state.json b/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/state.json
new file mode 100644
index 000000000..206d47bb2
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/state.json
@@ -0,0 +1,7 @@
+{
+  "address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
+  "parts": [
+    "b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b",
+    "b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e"
+  ]
+}
diff --git a/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/witnesses.json b/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/witnesses.json
new file mode 100644
index 000000000..290e08dc5
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/witnesses.json
@@ -0,0 +1,122 @@
+[
+  {
+    "witness": {
+      "profile": "joulespec-witness/1",
+      "alg": 1,
+      "spec_id": "b3:0641fe3157ee1e83e6db71a32d9d4134609f2d758b5d09dbe06943ae61faa8fb",
+      "obligation": "b3:d35a2f3ff28be1718133d7457d98466bebd16f5ee260fab64d4482ca33c5176d",
+      "artifact": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
+      "footprint": [],
+      "evidence": {
+        "kind": "falsifiable",
+        "check": "a_named_check",
+        "anchor": "specification",
+        "counter": "b3:e34e236da4740e55ec1aaabd0d1bcfe74529fa93cde433c07966669601d72eb5"
+      },
+      "energy": {
+        "uj": 1000,
+        "provenance": "estimator"
+      },
+      "author": [
+        129,
+        57,
+        119,
+        14,
+        168,
+        125,
+        23,
+        95,
+        86,
+        163,
+        84,
+        102,
+        195,
+        76,
+        126,
+        204,
+        203,
+        141,
+        138,
+        145,
+        180,
+        238,
+        55,
+        162,
+        93,
+        246,
+        15,
+        91,
+        143,
+        201,
+        179,
+        148
+      ]
+    },
+    "sig": [
+      119,
+      170,
+      207,
+      159,
+      41,
+      140,
+      205,
+      144,
+      124,
+      120,
+      97,
+      19,
+      237,
+      207,
+      111,
+      218,
+      98,
+      85,
+      158,
+      181,
+      94,
+      228,
+      228,
+      93,
+      6,
+      32,
+      116,
+      189,
+      206,
+      250,
+      228,
+      147,
+      19,
+      218,
+      111,
+      207,
+      136,
+      160,
+      146,
+      166,
+      8,
+      90,
+      217,
+      151,
+      133,
+      237,
+      49,
+      222,
+      97,
+      197,
+      2,
+      216,
+      122,
+      203,
+      137,
+      191,
+      26,
+      140,
+      153,
+      191,
+      96,
+      234,
+      244,
+      3
+    ]
+  }
+]
diff --git a/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/work.json b/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/work.json
new file mode 100644
index 000000000..07c240e2e
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/work.json
@@ -0,0 +1,46 @@
+[
+  {
+    "id": "b3:78ec055c7256fd5dfc25ab756441f9895afef0dc4a35e15c05dd8a07ae8e0e35",
+    "cites": [
+      "b3:d35a2f3ff28be1718133d7457d98466bebd16f5ee260fab64d4482ca33c5176d"
+    ],
+    "energy": {
+      "uj": 500000,
+      "provenance": "estimator"
+    },
+    "author": [
+      202,
+      147,
+      172,
+      23,
+      5,
+      24,
+      112,
+      113,
+      214,
+      123,
+      131,
+      199,
+      255,
+      14,
+      254,
+      129,
+      8,
+      232,
+      236,
+      69,
+      48,
+      87,
+      93,
+      119,
+      38,
+      135,
+      147,
+      51,
+      219,
+      218,
+      190,
+      124
+    ]
+  }
+]
diff --git a/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/expect.json b/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/expect.json
new file mode 100644
index 000000000..725dfc91a
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/expect.json
@@ -0,0 +1,21 @@
+{
+  "intent": "A requirement at E3 beside an unwitnessed non-goal.",
+  "trap": "Treating the non-goal as an owed obligation with no evidence empties the grade. A non-goal is owed nothing, so its absence of evidence is the correct state and caps nothing.",
+  "direction": "under-grading",
+  "grade": "falsifiable",
+  "attestation": "independent",
+  "flags": [],
+  "clauses": [
+    {
+      "label": "C1",
+      "grade": "falsifiable",
+      "stale": 0
+    },
+    {
+      "label": "C2",
+      "grade": null,
+      "stale": 0
+    }
+  ],
+  "conformant_at_e3": true
+}
diff --git a/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/spec.json b/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/spec.json
new file mode 100644
index 000000000..4ab949dbe
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/spec.json
@@ -0,0 +1,120 @@
+{
+  "spec": {
+    "profile": "joulespec/1",
+    "alg": 1,
+    "intent": "A corpus case: the clauses exist to be graded, not to be implemented.",
+    "clauses": [
+      {
+        "label": "C1",
+        "kind": "requirement",
+        "text": "The obligation is well evidenced."
+      },
+      {
+        "label": "C2",
+        "kind": "non-goal",
+        "text": "This is deliberately not built."
+      }
+    ],
+    "parent": null,
+    "author": [
+      138,
+      136,
+      227,
+      221,
+      116,
+      9,
+      241,
+      149,
+      253,
+      82,
+      219,
+      45,
+      60,
+      186,
+      93,
+      114,
+      202,
+      103,
+      9,
+      191,
+      29,
+      148,
+      18,
+      27,
+      243,
+      116,
+      136,
+      1,
+      180,
+      15,
+      111,
+      92
+    ]
+  },
+  "sig": [
+    148,
+    34,
+    18,
+    119,
+    136,
+    194,
+    111,
+    179,
+    250,
+    200,
+    72,
+    216,
+    47,
+    65,
+    201,
+    173,
+    111,
+    205,
+    137,
+    157,
+    48,
+    136,
+    202,
+    31,
+    192,
+    213,
+    202,
+    244,
+    238,
+    224,
+    159,
+    203,
+    69,
+    144,
+    72,
+    131,
+    31,
+    192,
+    235,
+    61,
+    246,
+    47,
+    78,
+    143,
+    63,
+    240,
+    126,
+    85,
+    162,
+    221,
+    46,
+    196,
+    85,
+    63,
+    54,
+    129,
+    42,
+    251,
+    227,
+    224,
+    114,
+    191,
+    90,
+    9
+  ]
+}
diff --git a/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/state.json b/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/state.json
new file mode 100644
index 000000000..206d47bb2
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/state.json
@@ -0,0 +1,7 @@
+{
+  "address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
+  "parts": [
+    "b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b",
+    "b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e"
+  ]
+}
diff --git a/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/witnesses.json b/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/witnesses.json
new file mode 100644
index 000000000..6825c93a0
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/witnesses.json
@@ -0,0 +1,122 @@
+[
+  {
+    "witness": {
+      "profile": "joulespec-witness/1",
+      "alg": 1,
+      "spec_id": "b3:ffdfffcba2e4f36037ca82c0a47700a4e564c6c4a10c46c4f8d0206f0437edcd",
+      "obligation": "b3:67e5769e5089a2c5457c2e0ff5f7d3305974debf4daf2d86e89c9be91529aa52",
+      "artifact": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
+      "footprint": [],
+      "evidence": {
+        "kind": "falsifiable",
+        "check": "a_named_check",
+        "anchor": "specification",
+        "counter": "b3:e34e236da4740e55ec1aaabd0d1bcfe74529fa93cde433c07966669601d72eb5"
+      },
+      "energy": {
+        "uj": 1000,
+        "provenance": "estimator"
+      },
+      "author": [
+        129,
+        57,
+        119,
+        14,
+        168,
+        125,
+        23,
+        95,
+        86,
+        163,
+        84,
+        102,
+        195,
+        76,
+        126,
+        204,
+        203,
+        141,
+        138,
+        145,
+        180,
+        238,
+        55,
+        162,
+        93,
+        246,
+        15,
+        91,
+        143,
+        201,
+        179,
+        148
+      ]
+    },
+    "sig": [
+      231,
+      240,
+      3,
+      175,
+      92,
+      232,
+      84,
+      168,
+      214,
+      242,
+      128,
+      109,
+      55,
+      113,
+      41,
+      32,
+      125,
+      124,
+      161,
+      115,
+      248,
+      255,
+      49,
+      84,
+      61,
+      33,
+      230,
+      6,
+      254,
+      112,
+      111,
+      13,
+      5,
+      194,
+      177,
+      86,
+      151,
+      156,
+      151,
+      92,
+      52,
+      187,
+      238,
+      41,
+      186,
+      181,
+      53,
+      164,
+      87,
+      23,
+      3,
+      65,
+      59,
+      200,
+      84,
+      224,
+      210,
+      72,
+      139,
+      166,
+      102,
+      155,
+      236,
+      10
+    ]
+  }
+]
diff --git a/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/work.json b/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/work.json
new file mode 100644
index 000000000..a63ffa498
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/work.json
@@ -0,0 +1,46 @@
+[
+  {
+    "id": "b3:78ec055c7256fd5dfc25ab756441f9895afef0dc4a35e15c05dd8a07ae8e0e35",
+    "cites": [
+      "b3:67e5769e5089a2c5457c2e0ff5f7d3305974debf4daf2d86e89c9be91529aa52"
+    ],
+    "energy": {
+      "uj": 500000,
+      "provenance": "estimator"
+    },
+    "author": [
+      202,
+      147,
+      172,
+      23,
+      5,
+      24,
+      112,
+      113,
+      214,
+      123,
+      131,
+      199,
+      255,
+      14,
+      254,
+      129,
+      8,
+      232,
+      236,
+      69,
+      48,
+      87,
+      93,
+      119,
+      38,
+      135,
+      147,
+      51,
+      219,
+      218,
+      190,
+      124
+    ]
+  }
+]
diff --git a/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/expect.json b/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/expect.json
new file mode 100644
index 000000000..84723c383
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/expect.json
@@ -0,0 +1,23 @@
+{
+  "intent": "Something implements the clause that says not to.",
+  "trap": "Counting the non-goal's evidence as a rung, or discarding it quietly. It is a flag, and §3.4 makes any flag block conformance even where every grade is satisfied.",
+  "direction": "over-grading",
+  "grade": "falsifiable",
+  "attestation": "independent",
+  "flags": [
+    "NonGoalWitnessed"
+  ],
+  "clauses": [
+    {
+      "label": "C1",
+      "grade": "falsifiable",
+      "stale": 0
+    },
+    {
+      "label": "C2",
+      "grade": null,
+      "stale": 0
+    }
+  ],
+  "conformant_at_e3": false
+}
diff --git a/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/spec.json b/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/spec.json
new file mode 100644
index 000000000..4ab949dbe
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/spec.json
@@ -0,0 +1,120 @@
+{
+  "spec": {
+    "profile": "joulespec/1",
+    "alg": 1,
+    "intent": "A corpus case: the clauses exist to be graded, not to be implemented.",
+    "clauses": [
+      {
+        "label": "C1",
+        "kind": "requirement",
+        "text": "The obligation is well evidenced."
+      },
+      {
+        "label": "C2",
+        "kind": "non-goal",
+        "text": "This is deliberately not built."
+      }
+    ],
+    "parent": null,
+    "author": [
+      138,
+      136,
+      227,
+      221,
+      116,
+      9,
+      241,
+      149,
+      253,
+      82,
+      219,
+      45,
+      60,
+      186,
+      93,
+      114,
+      202,
+      103,
+      9,
+      191,
+      29,
+      148,
+      18,
+      27,
+      243,
+      116,
+      136,
+      1,
+      180,
+      15,
+      111,
+      92
+    ]
+  },
+  "sig": [
+    148,
+    34,
+    18,
+    119,
+    136,
+    194,
+    111,
+    179,
+    250,
+    200,
+    72,
+    216,
+    47,
+    65,
+    201,
+    173,
+    111,
+    205,
+    137,
+    157,
+    48,
+    136,
+    202,
+    31,
+    192,
+    213,
+    202,
+    244,
+    238,
+    224,
+    159,
+    203,
+    69,
+    144,
+    72,
+    131,
+    31,
+    192,
+    235,
+    61,
+    246,
+    47,
+    78,
+    143,
+    63,
+    240,
+    126,
+    85,
+    162,
+    221,
+    46,
+    196,
+    85,
+    63,
+    54,
+    129,
+    42,
+    251,
+    227,
+    224,
+    114,
+    191,
+    90,
+    9
+  ]
+}
diff --git a/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/state.json b/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/state.json
new file mode 100644
index 000000000..206d47bb2
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/state.json
@@ -0,0 +1,7 @@
+{
+  "address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
+  "parts": [
+    "b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b",
+    "b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e"
+  ]
+}
diff --git a/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/witnesses.json b/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/witnesses.json
new file mode 100644
index 000000000..c258e4633
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/witnesses.json
@@ -0,0 +1,242 @@
+[
+  {
+    "witness": {
+      "profile": "joulespec-witness/1",
+      "alg": 1,
+      "spec_id": "b3:ffdfffcba2e4f36037ca82c0a47700a4e564c6c4a10c46c4f8d0206f0437edcd",
+      "obligation": "b3:67e5769e5089a2c5457c2e0ff5f7d3305974debf4daf2d86e89c9be91529aa52",
+      "artifact": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
+      "footprint": [],
+      "evidence": {
+        "kind": "falsifiable",
+        "check": "a_named_check",
+        "anchor": "specification",
+        "counter": "b3:e34e236da4740e55ec1aaabd0d1bcfe74529fa93cde433c07966669601d72eb5"
+      },
+      "energy": {
+        "uj": 1000,
+        "provenance": "estimator"
+      },
+      "author": [
+        129,
+        57,
+        119,
+        14,
+        168,
+        125,
+        23,
+        95,
+        86,
+        163,
+        84,
+        102,
+        195,
+        76,
+        126,
+        204,
+        203,
+        141,
+        138,
+        145,
+        180,
+        238,
+        55,
+        162,
+        93,
+        246,
+        15,
+        91,
+        143,
+        201,
+        179,
+        148
+      ]
+    },
+    "sig": [
+      231,
+      240,
+      3,
+      175,
+      92,
+      232,
+      84,
+      168,
+      214,
+      242,
+      128,
+      109,
+      55,
+      113,
+      41,
+      32,
+      125,
+      124,
+      161,
+      115,
+      248,
+      255,
+      49,
+      84,
+      61,
+      33,
+      230,
+      6,
+      254,
+      112,
+      111,
+      13,
+      5,
+      194,
+      177,
+      86,
+      151,
+      156,
+      151,
+      92,
+      52,
+      187,
+      238,
+      41,
+      186,
+      181,
+      53,
+      164,
+      87,
+      23,
+      3,
+      65,
+      59,
+      200,
+      84,
+      224,
+      210,
+      72,
+      139,
+      166,
+      102,
+      155,
+      236,
+      10
+    ]
+  },
+  {
+    "witness": {
+      "profile": "joulespec-witness/1",
+      "alg": 1,
+      "spec_id": "b3:ffdfffcba2e4f36037ca82c0a47700a4e564c6c4a10c46c4f8d0206f0437edcd",
+      "obligation": "b3:8aeed8e56271b17bb7fbb1a5a8bc814ad581e580baed6b01f8c5ff8edac61482",
+      "artifact": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
+      "footprint": [],
+      "evidence": {
+        "kind": "falsifiable",
+        "check": "a_named_check",
+        "anchor": "specification",
+        "counter": "b3:e34e236da4740e55ec1aaabd0d1bcfe74529fa93cde433c07966669601d72eb5"
+      },
+      "energy": {
+        "uj": 1000,
+        "provenance": "estimator"
+      },
+      "author": [
+        129,
+        57,
+        119,
+        14,
+        168,
+        125,
+        23,
+        95,
+        86,
+        163,
+        84,
+        102,
+        195,
+        76,
+        126,
+        204,
+        203,
+        141,
+        138,
+        145,
+        180,
+        238,
+        55,
+        162,
+        93,
+        246,
+        15,
+        91,
+        143,
+        201,
+        179,
+        148
+      ]
+    },
+    "sig": [
+      1,
+      144,
+      245,
+      9,
+      32,
+      177,
+      171,
+      158,
+      34,
+      33,
+      244,
+      100,
+      186,
+      237,
+      109,
+      60,
+      206,
+      17,
+      235,
+      80,
+      252,
+      249,
+      14,
+      164,
+      29,
+      150,
+      109,
+      57,
+      0,
+      82,
+      57,
+      0,
+      62,
+      235,
+      236,
+      149,
+      209,
+      92,
+      104,
+      135,
+      221,
+      67,
+      177,
+      172,
+      96,
+      246,
+      161,
+      152,
+      189,
+      54,
+      151,
+      50,
+      227,
+      237,
+      252,
+      7,
+      226,
+      2,
+      170,
+      13,
+      230,
+      177,
+      22,
+      7
+    ]
+  }
+]
diff --git a/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/work.json b/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/work.json
new file mode 100644
index 000000000..a63ffa498
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/work.json
@@ -0,0 +1,46 @@
+[
+  {
+    "id": "b3:78ec055c7256fd5dfc25ab756441f9895afef0dc4a35e15c05dd8a07ae8e0e35",
+    "cites": [
+      "b3:67e5769e5089a2c5457c2e0ff5f7d3305974debf4daf2d86e89c9be91529aa52"
+    ],
+    "energy": {
+      "uj": 500000,
+      "provenance": "estimator"
+    },
+    "author": [
+      202,
+      147,
+      172,
+      23,
+      5,
+      24,
+      112,
+      113,
+      214,
+      123,
+      131,
+      199,
+      255,
+      14,
+      254,
+      129,
+      8,
+      232,
+      236,
+      69,
+      48,
+      87,
+      93,
+      119,
+      38,
+      135,
+      147,
+      51,
+      219,
+      218,
+      190,
+      124
+    ]
+  }
+]
diff --git a/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/expect.json b/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/expect.json
new file mode 100644
index 000000000..d668cb527
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/expect.json
@@ -0,0 +1,16 @@
+{
+  "intent": "A check with a killed counter-artifact but no stated anchor.",
+  "trap": "Reading the counter-artifact alone and awarding E3. An oracle derived from the system under test cannot disagree with it, so §2.5 caps an unstated anchor at E2 however the check behaved.",
+  "direction": "over-grading",
+  "grade": "exercised",
+  "attestation": "independent",
+  "flags": [],
+  "clauses": [
+    {
+      "label": "C1",
+      "grade": "exercised",
+      "stale": 0
+    }
+  ],
+  "conformant_at_e3": false
+}
diff --git a/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/spec.json b/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/spec.json
new file mode 100644
index 000000000..9b802235c
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/spec.json
@@ -0,0 +1,115 @@
+{
+  "spec": {
+    "profile": "joulespec/1",
+    "alg": 1,
+    "intent": "A corpus case: the clauses exist to be graded, not to be implemented.",
+    "clauses": [
+      {
+        "label": "C1",
+        "kind": "requirement",
+        "text": "The obligation is checked by something whose expectation is unstated."
+      }
+    ],
+    "parent": null,
+    "author": [
+      138,
+      136,
+      227,
+      221,
+      116,
+      9,
+      241,
+      149,
+      253,
+      82,
+      219,
+      45,
+      60,
+      186,
+      93,
+      114,
+      202,
+      103,
+      9,
+      191,
+      29,
+      148,
+      18,
+      27,
+      243,
+      116,
+      136,
+      1,
+      180,
+      15,
+      111,
+      92
+    ]
+  },
+  "sig": [
+    232,
+    129,
+    54,
+    56,
+    154,
+    252,
+    10,
+    27,
+    228,
+    77,
+    131,
+    255,
+    86,
+    208,
+    193,
+    211,
+    51,
+    101,
+    191,
+    130,
+    245,
+    173,
+    127,
+    222,
+    86,
+    185,
+    33,
+    142,
+    97,
+    29,
+    87,
+    128,
+    121,
+    59,
+    48,
+    83,
+    240,
+    192,
+    143,
+    134,
+    2,
+    201,
+    119,
+    57,
+    60,
+    187,
+    47,
+    173,
+    252,
+    12,
+    254,
+    177,
+    128,
+    243,
+    41,
+    150,
+    140,
+    229,
+    214,
+    167,
+    69,
+    16,
+    17,
+    11
+  ]
+}
diff --git a/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/state.json b/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/state.json
new file mode 100644
index 000000000..206d47bb2
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/state.json
@@ -0,0 +1,7 @@
+{
+  "address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
+  "parts": [
+    "b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b",
+    "b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e"
+  ]
+}
diff --git a/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/witnesses.json b/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/witnesses.json
new file mode 100644
index 000000000..9aac3ff6c
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/witnesses.json
@@ -0,0 +1,122 @@
+[
+  {
+    "witness": {
+      "profile": "joulespec-witness/1",
+      "alg": 1,
+      "spec_id": "b3:dce42be27effefc874f8a4d8736726214fa4083f63a8b09f31de75bfdb2ecfac",
+      "obligation": "b3:1428edd294ce74bde484645da000d51e306b9461352d65d15af70d4edd1097e4",
+      "artifact": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
+      "footprint": [],
+      "evidence": {
+        "kind": "falsifiable",
+        "check": "a_named_check",
+        "anchor": "unstated",
+        "counter": "b3:e34e236da4740e55ec1aaabd0d1bcfe74529fa93cde433c07966669601d72eb5"
+      },
+      "energy": {
+        "uj": 1000,
+        "provenance": "estimator"
+      },
+      "author": [
+        129,
+        57,
+        119,
+        14,
+        168,
+        125,
+        23,
+        95,
+        86,
+        163,
+        84,
+        102,
+        195,
+        76,
+        126,
+        204,
+        203,
+        141,
+        138,
+        145,
+        180,
+        238,
+        55,
+        162,
+        93,
+        246,
+        15,
+        91,
+        143,
+        201,
+        179,
+        148
+      ]
+    },
+    "sig": [
+      30,
+      26,
+      52,
+      122,
+      153,
+      151,
+      227,
+      74,
+      32,
+      83,
+      224,
+      192,
+      214,
+      151,
+      134,
+      108,
+      196,
+      18,
+      254,
+      63,
+      94,
+      178,
+      168,
+      112,
+      217,
+      229,
+      36,
+      2,
+      89,
+      13,
+      160,
+      87,
+      58,
+      111,
+      130,
+      90,
+      18,
+      202,
+      228,
+      56,
+      156,
+      20,
+      200,
+      92,
+      8,
+      3,
+      15,
+      183,
+      239,
+      38,
+      28,
+      120,
+      212,
+      183,
+      188,
+      187,
+      255,
+      3,
+      245,
+      189,
+      28,
+      58,
+      186,
+      11
+    ]
+  }
+]
diff --git a/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/work.json b/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/work.json
new file mode 100644
index 000000000..7d5ae9465
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/work.json
@@ -0,0 +1,46 @@
+[
+  {
+    "id": "b3:78ec055c7256fd5dfc25ab756441f9895afef0dc4a35e15c05dd8a07ae8e0e35",
+    "cites": [
+      "b3:1428edd294ce74bde484645da000d51e306b9461352d65d15af70d4edd1097e4"
+    ],
+    "energy": {
+      "uj": 500000,
+      "provenance": "estimator"
+    },
+    "author": [
+      202,
+      147,
+      172,
+      23,
+      5,
+      24,
+      112,
+      113,
+      214,
+      123,
+      131,
+      199,
+      255,
+      14,
+      254,
+      129,
+      8,
+      232,
+      236,
+      69,
+      48,
+      87,
+      93,
+      119,
+      38,
+      135,
+      147,
+      51,
+      219,
+      218,
+      190,
+      124
+    ]
+  }
+]
diff --git a/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/expect.json b/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/expect.json
new file mode 100644
index 000000000..7e3e68529
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/expect.json
@@ -0,0 +1,16 @@
+{
+  "intent": "A non-vacuous proof whose binding to the clause is the prover's own word.",
+  "trap": "Awarding E4 because a prover succeeded. The proof is real machine-checked evidence about something — E2 — and that the something is this clause is unconfirmed (§2.6).",
+  "direction": "over-grading",
+  "grade": "exercised",
+  "attestation": "independent",
+  "flags": [],
+  "clauses": [
+    {
+      "label": "C1",
+      "grade": "exercised",
+      "stale": 0
+    }
+  ],
+  "conformant_at_e3": false
+}
diff --git a/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/spec.json b/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/spec.json
new file mode 100644
index 000000000..1a23877d7
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/spec.json
@@ -0,0 +1,115 @@
+{
+  "spec": {
+    "profile": "joulespec/1",
+    "alg": 1,
+    "intent": "A corpus case: the clauses exist to be graded, not to be implemented.",
+    "clauses": [
+      {
+        "label": "C1",
+        "kind": "requirement",
+        "text": "The obligation is discharged as a proof under the prover's own formalization."
+      }
+    ],
+    "parent": null,
+    "author": [
+      138,
+      136,
+      227,
+      221,
+      116,
+      9,
+      241,
+      149,
+      253,
+      82,
+      219,
+      45,
+      60,
+      186,
+      93,
+      114,
+      202,
+      103,
+      9,
+      191,
+      29,
+      148,
+      18,
+      27,
+      243,
+      116,
+      136,
+      1,
+      180,
+      15,
+      111,
+      92
+    ]
+  },
+  "sig": [
+    230,
+    223,
+    192,
+    92,
+    86,
+    73,
+    29,
+    122,
+    19,
+    51,
+    241,
+    40,
+    231,
+    16,
+    76,
+    150,
+    148,
+    103,
+    16,
+    62,
+    242,
+    129,
+    100,
+    44,
+    166,
+    222,
+    27,
+    231,
+    71,
+    35,
+    103,
+    15,
+    120,
+    141,
+    76,
+    15,
+    72,
+    148,
+    166,
+    177,
+    220,
+    220,
+    140,
+    43,
+    144,
+    170,
+    178,
+    240,
+    14,
+    79,
+    146,
+    87,
+    125,
+    29,
+    218,
+    36,
+    240,
+    91,
+    137,
+    161,
+    25,
+    30,
+    227,
+    4
+  ]
+}
diff --git a/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/state.json b/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/state.json
new file mode 100644
index 000000000..206d47bb2
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/state.json
@@ -0,0 +1,7 @@
+{
+  "address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
+  "parts": [
+    "b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b",
+    "b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e"
+  ]
+}
diff --git a/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/witnesses.json b/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/witnesses.json
new file mode 100644
index 000000000..1daa9eddb
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/witnesses.json
@@ -0,0 +1,129 @@
+[
+  {
+    "witness": {
+      "profile": "joulespec-witness/1",
+      "alg": 1,
+      "spec_id": "b3:60e5ec581d01948a179d8fd98bac59e7061fa8fc15098e0f1a6b8af76883ef99",
+      "obligation": "b3:e535081843369fb6415f4c0c13e6568c3757123ca4e0147fdd9b905929045d69",
+      "artifact": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
+      "footprint": [],
+      "evidence": {
+        "kind": "proved",
+        "goal": "b3:bbc98522dfcf0bb13e1772dcecc655fa0c92eabacbc7a226e38ff74e5f0606ce",
+        "tier": "corpus",
+        "formalization": {
+          "statement": "forall x. p(x)",
+          "grounding": "declared"
+        },
+        "vacuity": {
+          "kind": "refuted",
+          "counter": "b3:def80a6779418b717f5b005941967d6597889e965986d59b2c55b6c0e0c5b5ae"
+        }
+      },
+      "energy": {
+        "uj": 1000,
+        "provenance": "estimator"
+      },
+      "author": [
+        129,
+        57,
+        119,
+        14,
+        168,
+        125,
+        23,
+        95,
+        86,
+        163,
+        84,
+        102,
+        195,
+        76,
+        126,
+        204,
+        203,
+        141,
+        138,
+        145,
+        180,
+        238,
+        55,
+        162,
+        93,
+        246,
+        15,
+        91,
+        143,
+        201,
+        179,
+        148
+      ]
+    },
+    "sig": [
+      0,
+      230,
+      197,
+      84,
+      90,
+      168,
+      192,
+      148,
+      227,
+      30,
+      136,
+      67,
+      160,
+      127,
+      227,
+      253,
+      245,
+      182,
+      63,
+      145,
+      154,
+      33,
+      23,
+      38,
+      191,
+      193,
+      141,
+      169,
+      115,
+      236,
+      54,
+      145,
+      85,
+      249,
+      15,
+      173,
+      58,
+      191,
+      25,
+      146,
+      88,
+      138,
+      85,
+      208,
+      164,
+      12,
+      143,
+      101,
+      244,
+      241,
+      40,
+      119,
+      18,
+      105,
+      207,
+      239,
+      48,
+      65,
+      190,
+      21,
+      164,
+      98,
+      52,
+      15
+    ]
+  }
+]
diff --git a/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/work.json b/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/work.json
new file mode 100644
index 000000000..323ba35af
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/work.json
@@ -0,0 +1,46 @@
+[
+  {
+    "id": "b3:78ec055c7256fd5dfc25ab756441f9895afef0dc4a35e15c05dd8a07ae8e0e35",
+    "cites": [
+      "b3:e535081843369fb6415f4c0c13e6568c3757123ca4e0147fdd9b905929045d69"
+    ],
+    "energy": {
+      "uj": 500000,
+      "provenance": "estimator"
+    },
+    "author": [
+      202,
+      147,
+      172,
+      23,
+      5,
+      24,
+      112,
+      113,
+      214,
+      123,
+      131,
+      199,
+      255,
+      14,
+      254,
+      129,
+      8,
+      232,
+      236,
+      69,
+      48,
+      87,
+      93,
+      119,
+      38,
+      135,
+      147,
+      51,
+      219,
+      218,
+      190,
+      124
+    ]
+  }
+]
diff --git a/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/expect.json b/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/expect.json
new file mode 100644
index 000000000..6e6463450
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/expect.json
@@ -0,0 +1,16 @@
+{
+  "intent": "A proof with an independently cross-checked formalization, never shown capable of failing.",
+  "trap": "Awarding E4 because the formalization was cross-checked. A property can hold because nothing reaches the condition it guards; every rung above E2 rests on a demonstrated failure.",
+  "direction": "over-grading",
+  "grade": "exercised",
+  "attestation": "independent",
+  "flags": [],
+  "clauses": [
+    {
+      "label": "C1",
+      "grade": "exercised",
+      "stale": 0
+    }
+  ],
+  "conformant_at_e3": false
+}
diff --git a/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/spec.json b/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/spec.json
new file mode 100644
index 000000000..868d617e6
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/spec.json
@@ -0,0 +1,115 @@
+{
+  "spec": {
+    "profile": "joulespec/1",
+    "alg": 1,
+    "intent": "A corpus case: the clauses exist to be graded, not to be implemented.",
+    "clauses": [
+      {
+        "label": "C1",
+        "kind": "requirement",
+        "text": "The obligation is discharged as a proof nobody checked for vacuity."
+      }
+    ],
+    "parent": null,
+    "author": [
+      138,
+      136,
+      227,
+      221,
+      116,
+      9,
+      241,
+      149,
+      253,
+      82,
+      219,
+      45,
+      60,
+      186,
+      93,
+      114,
+      202,
+      103,
+      9,
+      191,
+      29,
+      148,
+      18,
+      27,
+      243,
+      116,
+      136,
+      1,
+      180,
+      15,
+      111,
+      92
+    ]
+  },
+  "sig": [
+    113,
+    95,
+    117,
+    58,
+    54,
+    173,
+    175,
+    188,
+    219,
+    96,
+    201,
+    130,
+    85,
+    193,
+    40,
+    235,
+    114,
+    127,
+    56,
+    130,
+    232,
+    129,
+    196,
+    116,
+    222,
+    78,
+    28,
+    230,
+    187,
+    100,
+    191,
+    84,
+    73,
+    174,
+    219,
+    166,
+    138,
+    218,
+    9,
+    209,
+    167,
+    43,
+    243,
+    124,
+    36,
+    53,
+    115,
+    129,
+    203,
+    95,
+    97,
+    140,
+    147,
+    238,
+    49,
+    226,
+    96,
+    172,
+    32,
+    217,
+    198,
+    126,
+    81,
+    0
+  ]
+}
diff --git a/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/state.json b/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/state.json
new file mode 100644
index 000000000..206d47bb2
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/state.json
@@ -0,0 +1,7 @@
+{
+  "address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
+  "parts": [
+    "b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b",
+    "b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e"
+  ]
+}
diff --git a/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/witnesses.json b/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/witnesses.json
new file mode 100644
index 000000000..64a9a1532
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/witnesses.json
@@ -0,0 +1,165 @@
+[
+  {
+    "witness": {
+      "profile": "joulespec-witness/1",
+      "alg": 1,
+      "spec_id": "b3:0684fbbba22698b8874acd5de02e14d60e571595ed5667001b1eac2c65712112",
+      "obligation": "b3:8c38bdd6981befcc0b784b8b2861b77682fa66493ec48e80e6815e5b063940f6",
+      "artifact": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
+      "footprint": [],
+      "evidence": {
+        "kind": "proved",
+        "goal": "b3:bbc98522dfcf0bb13e1772dcecc655fa0c92eabacbc7a226e38ff74e5f0606ce",
+        "tier": "corpus",
+        "formalization": {
+          "statement": "forall x. p(x)",
+          "grounding": {
+            "cross-checked": {
+              "by": [
+                237,
+                73,
+                40,
+                198,
+                40,
+                209,
+                194,
+                198,
+                234,
+                233,
+                3,
+                56,
+                144,
+                89,
+                149,
+                97,
+                41,
+                89,
+                39,
+                58,
+                92,
+                99,
+                249,
+                54,
+                54,
+                193,
+                70,
+                20,
+                172,
+                135,
+                55,
+                209
+              ]
+            }
+          }
+        },
+        "vacuity": {
+          "kind": "unchecked"
+        }
+      },
+      "energy": {
+        "uj": 1000,
+        "provenance": "estimator"
+      },
+      "author": [
+        129,
+        57,
+        119,
+        14,
+        168,
+        125,
+        23,
+        95,
+        86,
+        163,
+        84,
+        102,
+        195,
+        76,
+        126,
+        204,
+        203,
+        141,
+        138,
+        145,
+        180,
+        238,
+        55,
+        162,
+        93,
+        246,
+        15,
+        91,
+        143,
+        201,
+        179,
+        148
+      ]
+    },
+    "sig": [
+      219,
+      188,
+      206,
+      146,
+      168,
+      110,
+      89,
+      117,
+      145,
+      154,
+      6,
+      148,
+      185,
+      190,
+      229,
+      110,
+      164,
+      234,
+      106,
+      100,
+      135,
+      158,
+      55,
+      114,
+      107,
+      7,
+      8,
+      66,
+      186,
+      255,
+      210,
+      171,
+      150,
+      88,
+      119,
+      148,
+      246,
+      243,
+      196,
+      37,
+      217,
+      70,
+      36,
+      113,
+      200,
+      248,
+      159,
+      141,
+      36,
+      116,
+      167,
+      96,
+      105,
+      40,
+      228,
+      228,
+      44,
+      169,
+      239,
+      32,
+      115,
+      127,
+      96,
+      2
+    ]
+  }
+]
diff --git a/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/work.json b/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/work.json
new file mode 100644
index 000000000..dcea7b37f
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/work.json
@@ -0,0 +1,46 @@
+[
+  {
+    "id": "b3:78ec055c7256fd5dfc25ab756441f9895afef0dc4a35e15c05dd8a07ae8e0e35",
+    "cites": [
+      "b3:8c38bdd6981befcc0b784b8b2861b77682fa66493ec48e80e6815e5b063940f6"
+    ],
+    "energy": {
+      "uj": 500000,
+      "provenance": "estimator"
+    },
+    "author": [
+      202,
+      147,
+      172,
+      23,
+      5,
+      24,
+      112,
+      113,
+      214,
+      123,
+      131,
+      199,
+      255,
+      14,
+      254,
+      129,
+      8,
+      232,
+      236,
+      69,
+      48,
+      87,
+      93,
+      119,
+      38,
+      135,
+      147,
+      51,
+      219,
+      218,
+      190,
+      124
+    ]
+  }
+]
diff --git a/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/expect.json b/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/expect.json
new file mode 100644
index 000000000..feabc2ea1
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/expect.json
@@ -0,0 +1,16 @@
+{
+  "intent": "The only witness observed a tree that is no longer the artifact, and declared no footprint.",
+  "trap": "Counting it because it verifies and names a stated obligation. An empty footprint means the whole artifact, so any change to the artifact invalidates it — and the clause is then unevidenced, which empties the grade rather than lowering it.",
+  "direction": "over-grading",
+  "grade": null,
+  "attestation": null,
+  "flags": [],
+  "clauses": [
+    {
+      "label": "C1",
+      "grade": null,
+      "stale": 1
+    }
+  ],
+  "conformant_at_e3": false
+}
diff --git a/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/spec.json b/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/spec.json
new file mode 100644
index 000000000..d2cff9b2e
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/spec.json
@@ -0,0 +1,115 @@
+{
+  "spec": {
+    "profile": "joulespec/1",
+    "alg": 1,
+    "intent": "A corpus case: the clauses exist to be graded, not to be implemented.",
+    "clauses": [
+      {
+        "label": "C1",
+        "kind": "requirement",
+        "text": "The obligation was checked against an earlier tree."
+      }
+    ],
+    "parent": null,
+    "author": [
+      138,
+      136,
+      227,
+      221,
+      116,
+      9,
+      241,
+      149,
+      253,
+      82,
+      219,
+      45,
+      60,
+      186,
+      93,
+      114,
+      202,
+      103,
+      9,
+      191,
+      29,
+      148,
+      18,
+      27,
+      243,
+      116,
+      136,
+      1,
+      180,
+      15,
+      111,
+      92
+    ]
+  },
+  "sig": [
+    233,
+    92,
+    69,
+    171,
+    34,
+    163,
+    70,
+    150,
+    25,
+    3,
+    254,
+    136,
+    169,
+    113,
+    237,
+    212,
+    179,
+    102,
+    141,
+    221,
+    76,
+    98,
+    204,
+    56,
+    23,
+    67,
+    244,
+    77,
+    114,
+    140,
+    145,
+    1,
+    81,
+    54,
+    196,
+    231,
+    89,
+    85,
+    11,
+    58,
+    34,
+    37,
+    157,
+    85,
+    135,
+    96,
+    234,
+    24,
+    143,
+    122,
+    193,
+    175,
+    116,
+    93,
+    18,
+    180,
+    69,
+    20,
+    91,
+    116,
+    51,
+    130,
+    32,
+    5
+  ]
+}
diff --git a/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/state.json b/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/state.json
new file mode 100644
index 000000000..206d47bb2
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/state.json
@@ -0,0 +1,7 @@
+{
+  "address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
+  "parts": [
+    "b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b",
+    "b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e"
+  ]
+}
diff --git a/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/witnesses.json b/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/witnesses.json
new file mode 100644
index 000000000..46f2f8891
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/witnesses.json
@@ -0,0 +1,122 @@
+[
+  {
+    "witness": {
+      "profile": "joulespec-witness/1",
+      "alg": 1,
+      "spec_id": "b3:aa55f1c89f6918a7a8f4f232d7d0fb5676ad97109bece106eb4cf71f656cb5fd",
+      "obligation": "b3:077b78197459d69d43a714aab09a4fd557e64344c5d8fcf04fe3e4b18e800a2b",
+      "artifact": "b3:c24c4acaeac144d5ae9a9569b55cd6aec79c38f91ded00e1e6029057aa1d1201",
+      "footprint": [],
+      "evidence": {
+        "kind": "falsifiable",
+        "check": "a_named_check",
+        "anchor": "specification",
+        "counter": "b3:e34e236da4740e55ec1aaabd0d1bcfe74529fa93cde433c07966669601d72eb5"
+      },
+      "energy": {
+        "uj": 1000,
+        "provenance": "estimator"
+      },
+      "author": [
+        129,
+        57,
+        119,
+        14,
+        168,
+        125,
+        23,
+        95,
+        86,
+        163,
+        84,
+        102,
+        195,
+        76,
+        126,
+        204,
+        203,
+        141,
+        138,
+        145,
+        180,
+        238,
+        55,
+        162,
+        93,
+        246,
+        15,
+        91,
+        143,
+        201,
+        179,
+        148
+      ]
+    },
+    "sig": [
+      29,
+      184,
+      206,
+      104,
+      136,
+      141,
+      196,
+      48,
+      217,
+      48,
+      196,
+      223,
+      113,
+      75,
+      50,
+      181,
+      206,
+      7,
+      153,
+      31,
+      216,
+      110,
+      57,
+      166,
+      18,
+      47,
+      186,
+      123,
+      205,
+      241,
+      251,
+      101,
+      252,
+      176,
+      232,
+      38,
+      145,
+      49,
+      25,
+      178,
+      112,
+      219,
+      11,
+      92,
+      153,
+      199,
+      171,
+      33,
+      112,
+      227,
+      207,
+      62,
+      202,
+      236,
+      135,
+      97,
+      121,
+      246,
+      51,
+      62,
+      212,
+      128,
+      142,
+      3
+    ]
+  }
+]
diff --git a/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/work.json b/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/work.json
new file mode 100644
index 000000000..482b65a11
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/work.json
@@ -0,0 +1,46 @@
+[
+  {
+    "id": "b3:78ec055c7256fd5dfc25ab756441f9895afef0dc4a35e15c05dd8a07ae8e0e35",
+    "cites": [
+      "b3:077b78197459d69d43a714aab09a4fd557e64344c5d8fcf04fe3e4b18e800a2b"
+    ],
+    "energy": {
+      "uj": 500000,
+      "provenance": "estimator"
+    },
+    "author": [
+      202,
+      147,
+      172,
+      23,
+      5,
+      24,
+      112,
+      113,
+      214,
+      123,
+      131,
+      199,
+      255,
+      14,
+      254,
+      129,
+      8,
+      232,
+      236,
+      69,
+      48,
+      87,
+      93,
+      119,
+      38,
+      135,
+      147,
+      51,
+      219,
+      218,
+      190,
+      124
+    ]
+  }
+]
diff --git a/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/expect.json b/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/expect.json
new file mode 100644
index 000000000..45bcdd07f
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/expect.json
@@ -0,0 +1,18 @@
+{
+  "intent": "A verifying witness whose obligation address is the clause's previous wording.",
+  "trap": "Discarding it silently, which is how drift stops being visible. It is reported as unbound, and the clause it used to evidence is now unevidenced.",
+  "direction": "over-grading",
+  "grade": null,
+  "attestation": null,
+  "flags": [
+    "Unbound"
+  ],
+  "clauses": [
+    {
+      "label": "C1",
+      "grade": null,
+      "stale": 0
+    }
+  ],
+  "conformant_at_e3": false
+}
diff --git a/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/spec.json b/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/spec.json
new file mode 100644
index 000000000..638a992ea
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/spec.json
@@ -0,0 +1,115 @@
+{
+  "spec": {
+    "profile": "joulespec/1",
+    "alg": 1,
+    "intent": "A corpus case: the clauses exist to be graded, not to be implemented.",
+    "clauses": [
+      {
+        "label": "C1",
+        "kind": "requirement",
+        "text": "The obligation as the specification now words it."
+      }
+    ],
+    "parent": null,
+    "author": [
+      138,
+      136,
+      227,
+      221,
+      116,
+      9,
+      241,
+      149,
+      253,
+      82,
+      219,
+      45,
+      60,
+      186,
+      93,
+      114,
+      202,
+      103,
+      9,
+      191,
+      29,
+      148,
+      18,
+      27,
+      243,
+      116,
+      136,
+      1,
+      180,
+      15,
+      111,
+      92
+    ]
+  },
+  "sig": [
+    242,
+    243,
+    44,
+    1,
+    85,
+    35,
+    61,
+    244,
+    218,
+    15,
+    227,
+    86,
+    204,
+    185,
+    9,
+    206,
+    216,
+    76,
+    212,
+    251,
+    249,
+    121,
+    202,
+    69,
+    95,
+    183,
+    126,
+    128,
+    141,
+    20,
+    184,
+    253,
+    108,
+    233,
+    173,
+    88,
+    220,
+    92,
+    49,
+    15,
+    87,
+    155,
+    245,
+    210,
+    117,
+    73,
+    95,
+    236,
+    117,
+    233,
+    0,
+    161,
+    251,
+    72,
+    41,
+    174,
+    141,
+    57,
+    227,
+    210,
+    47,
+    23,
+    173,
+    7
+  ]
+}
diff --git a/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/state.json b/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/state.json
new file mode 100644
index 000000000..206d47bb2
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/state.json
@@ -0,0 +1,7 @@
+{
+  "address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
+  "parts": [
+    "b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b",
+    "b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e"
+  ]
+}
diff --git a/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/witnesses.json b/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/witnesses.json
new file mode 100644
index 000000000..0ee024825
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/witnesses.json
@@ -0,0 +1,122 @@
+[
+  {
+    "witness": {
+      "profile": "joulespec-witness/1",
+      "alg": 1,
+      "spec_id": "b3:63d4bd9c7d506a65fbe39e73c89ebe3a8791e7ebf1e67de1b400d1823fea7469",
+      "obligation": "b3:ed83074359c0815f20d3525c083da01ad661b06926caa583449c3ef15bb7c737",
+      "artifact": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
+      "footprint": [],
+      "evidence": {
+        "kind": "falsifiable",
+        "check": "a_named_check",
+        "anchor": "specification",
+        "counter": "b3:e34e236da4740e55ec1aaabd0d1bcfe74529fa93cde433c07966669601d72eb5"
+      },
+      "energy": {
+        "uj": 1000,
+        "provenance": "estimator"
+      },
+      "author": [
+        129,
+        57,
+        119,
+        14,
+        168,
+        125,
+        23,
+        95,
+        86,
+        163,
+        84,
+        102,
+        195,
+        76,
+        126,
+        204,
+        203,
+        141,
+        138,
+        145,
+        180,
+        238,
+        55,
+        162,
+        93,
+        246,
+        15,
+        91,
+        143,
+        201,
+        179,
+        148
+      ]
+    },
+    "sig": [
+      60,
+      248,
+      235,
+      218,
+      51,
+      26,
+      146,
+      5,
+      100,
+      146,
+      36,
+      215,
+      41,
+      171,
+      236,
+      21,
+      50,
+      168,
+      249,
+      111,
+      64,
+      215,
+      214,
+      18,
+      212,
+      37,
+      203,
+      136,
+      220,
+      181,
+      250,
+      79,
+      154,
+      206,
+      224,
+      26,
+      227,
+      82,
+      100,
+      102,
+      81,
+      115,
+      226,
+      201,
+      80,
+      103,
+      90,
+      222,
+      176,
+      69,
+      200,
+      235,
+      148,
+      102,
+      190,
+      11,
+      89,
+      8,
+      200,
+      241,
+      186,
+      18,
+      217,
+      5
+    ]
+  }
+]
diff --git a/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/work.json b/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/work.json
new file mode 100644
index 000000000..09846be9d
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/work.json
@@ -0,0 +1,46 @@
+[
+  {
+    "id": "b3:78ec055c7256fd5dfc25ab756441f9895afef0dc4a35e15c05dd8a07ae8e0e35",
+    "cites": [
+      "b3:483ce5d0da7b89444fa282cf20196353ad87e422968355db94657869789bd48c"
+    ],
+    "energy": {
+      "uj": 500000,
+      "provenance": "estimator"
+    },
+    "author": [
+      202,
+      147,
+      172,
+      23,
+      5,
+      24,
+      112,
+      113,
+      214,
+      123,
+      131,
+      199,
+      255,
+      14,
+      254,
+      129,
+      8,
+      232,
+      236,
+      69,
+      48,
+      87,
+      93,
+      119,
+      38,
+      135,
+      147,
+      51,
+      219,
+      218,
+      190,
+      124
+    ]
+  }
+]
diff --git a/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/expect.json b/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/expect.json
new file mode 100644
index 000000000..b12d364bd
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/expect.json
@@ -0,0 +1,16 @@
+{
+  "intent": "The reviewer and the specification's author are one key.",
+  "trap": "Awarding E1 because the evidence says `reviewed`. E1 requires a second party, and independence is computed from the keys rather than taken from the label.",
+  "direction": "over-grading",
+  "grade": "cited",
+  "attestation": "self-attested",
+  "flags": [],
+  "clauses": [
+    {
+      "label": "C1",
+      "grade": "cited",
+      "stale": 0
+    }
+  ],
+  "conformant_at_e3": false
+}
diff --git a/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/spec.json b/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/spec.json
new file mode 100644
index 000000000..f8053c14e
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/spec.json
@@ -0,0 +1,115 @@
+{
+  "spec": {
+    "profile": "joulespec/1",
+    "alg": 1,
+    "intent": "A corpus case: the clauses exist to be graded, not to be implemented.",
+    "clauses": [
+      {
+        "label": "C1",
+        "kind": "requirement",
+        "text": "The obligation was reviewed by the party that wrote the specification."
+      }
+    ],
+    "parent": null,
+    "author": [
+      138,
+      136,
+      227,
+      221,
+      116,
+      9,
+      241,
+      149,
+      253,
+      82,
+      219,
+      45,
+      60,
+      186,
+      93,
+      114,
+      202,
+      103,
+      9,
+      191,
+      29,
+      148,
+      18,
+      27,
+      243,
+      116,
+      136,
+      1,
+      180,
+      15,
+      111,
+      92
+    ]
+  },
+  "sig": [
+    22,
+    25,
+    146,
+    110,
+    125,
+    175,
+    67,
+    93,
+    121,
+    173,
+    183,
+    240,
+    187,
+    20,
+    158,
+    240,
+    234,
+    215,
+    207,
+    191,
+    34,
+    212,
+    54,
+    243,
+    70,
+    176,
+    53,
+    163,
+    4,
+    198,
+    1,
+    172,
+    185,
+    230,
+    168,
+    59,
+    242,
+    139,
+    251,
+    94,
+    165,
+    165,
+    160,
+    39,
+    73,
+    180,
+    177,
+    119,
+    168,
+    203,
+    196,
+    41,
+    100,
+    247,
+    132,
+    54,
+    94,
+    66,
+    65,
+    41,
+    168,
+    96,
+    99,
+    8
+  ]
+}
diff --git a/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/state.json b/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/state.json
new file mode 100644
index 000000000..206d47bb2
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/state.json
@@ -0,0 +1,7 @@
+{
+  "address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
+  "parts": [
+    "b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b",
+    "b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e"
+  ]
+}
diff --git a/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/witnesses.json b/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/witnesses.json
new file mode 100644
index 000000000..a50bea0fa
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/witnesses.json
@@ -0,0 +1,153 @@
+[
+  {
+    "witness": {
+      "profile": "joulespec-witness/1",
+      "alg": 1,
+      "spec_id": "b3:5d33c00c7f19db758ce990bdfdeb777fb700d05965cf1708ccf2c411c5bacce4",
+      "obligation": "b3:fadbf5bf4219d3004b998eee6e2d4b77049554a2be7c5ab804a681f6ecffbe7c",
+      "artifact": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
+      "footprint": [],
+      "evidence": {
+        "kind": "reviewed",
+        "reviewer": [
+          138,
+          136,
+          227,
+          221,
+          116,
+          9,
+          241,
+          149,
+          253,
+          82,
+          219,
+          45,
+          60,
+          186,
+          93,
+          114,
+          202,
+          103,
+          9,
+          191,
+          29,
+          148,
+          18,
+          27,
+          243,
+          116,
+          136,
+          1,
+          180,
+          15,
+          111,
+          92
+        ]
+      },
+      "energy": {
+        "uj": 1000,
+        "provenance": "estimator"
+      },
+      "author": [
+        138,
+        136,
+        227,
+        221,
+        116,
+        9,
+        241,
+        149,
+        253,
+        82,
+        219,
+        45,
+        60,
+        186,
+        93,
+        114,
+        202,
+        103,
+        9,
+        191,
+        29,
+        148,
+        18,
+        27,
+        243,
+        116,
+        136,
+        1,
+        180,
+        15,
+        111,
+        92
+      ]
+    },
+    "sig": [
+      6,
+      174,
+      38,
+      158,
+      207,
+      238,
+      36,
+      163,
+      130,
+      113,
+      167,
+      65,
+      163,
+      195,
+      243,
+      17,
+      72,
+      83,
+      233,
+      98,
+      9,
+      19,
+      172,
+      179,
+      63,
+      97,
+      132,
+      67,
+      84,
+      141,
+      99,
+      6,
+      135,
+      67,
+      191,
+      206,
+      94,
+      142,
+      107,
+      222,
+      117,
+      161,
+      254,
+      221,
+      213,
+      29,
+      212,
+      9,
+      215,
+      10,
+      188,
+      39,
+      151,
+      11,
+      63,
+      217,
+      192,
+      24,
+      108,
+      107,
+      20,
+      114,
+      190,
+      10
+    ]
+  }
+]
diff --git a/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/work.json b/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/work.json
new file mode 100644
index 000000000..15609ff72
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/work.json
@@ -0,0 +1,46 @@
+[
+  {
+    "id": "b3:78ec055c7256fd5dfc25ab756441f9895afef0dc4a35e15c05dd8a07ae8e0e35",
+    "cites": [
+      "b3:fadbf5bf4219d3004b998eee6e2d4b77049554a2be7c5ab804a681f6ecffbe7c"
+    ],
+    "energy": {
+      "uj": 500000,
+      "provenance": "estimator"
+    },
+    "author": [
+      138,
+      136,
+      227,
+      221,
+      116,
+      9,
+      241,
+      149,
+      253,
+      82,
+      219,
+      45,
+      60,
+      186,
+      93,
+      114,
+      202,
+      103,
+      9,
+      191,
+      29,
+      148,
+      18,
+      27,
+      243,
+      116,
+      136,
+      1,
+      180,
+      15,
+      111,
+      92
+    ]
+  }
+]
diff --git a/joulespec/conformance/v1/evaluation/README.md b/joulespec/conformance/v1/evaluation/README.md
new file mode 100644
index 000000000..46a4747a4
--- /dev/null
+++ b/joulespec/conformance/v1/evaluation/README.md
@@ -0,0 +1,85 @@
+# The evaluation corpus
+
+Cases a too-generous implementation passes incorrectly.
+
+The wire vectors in [`../vectors/`](../vectors) certify that an
+implementation round-trips a receipt's **bytes**. They say nothing about
+whether it reaches the right **verdict**, because they carry one scenario.
+This corpus is the other half.
+
+Each case directory holds five files. Read the first four, evaluate, and
+compare against the fifth:
+
+| File | What it is |
+|---|---|
+| `spec.json` | the signed specification |
+| `state.json` | the artifact state the witnesses were observed at |
+| `witnesses.json` | the signed witnesses |
+| `work.json` | the declared work, which is what the attestation axis is computed from |
+| `expect.json` | the verdict §3 requires, with the trap it sets |
+
+`expect.json` carries its own `intent` and `trap` in prose, so a failing case
+says what it was for rather than only which field differed.
+
+## Why the cases are shaped the way they are
+
+Every case states a **direction**. Most are `over-grading`: an
+implementation that reports conformance never established, which is the
+failure this standard exists to stop. At least one is `under-grading`,
+because an implementation that graded nothing at all would pass every
+over-grading case — a corpus with only one direction rewards a rule that
+refuses everything. A test asserts that both directions are present, that
+every over-grading case's correct verdict falls short of the bar or is
+blocked by a flag, and that every under-grading case's correct verdict
+reaches it.
+
+The traps are the ones that are reachable by accident rather than by
+carelessness:
+
+- a **mean** instead of a minimum, which lets well-evidenced obligations
+  conceal one nobody looked at;
+- **skipping** an unevidenced obligation rather than letting its absence
+  empty the grade — and reporting `E0` there, which would claim a citation
+  nobody made;
+- treating an **unwitnessed non-goal** as an owed obligation with no
+  evidence, which is the under-grading case;
+- grading a **witnessed non-goal**'s evidence, or discarding it quietly,
+  instead of raising the flag that blocks conformance;
+- awarding `E3` on a killed counter-artifact alone, where the check's
+  **anchor is unstated**;
+- awarding `E4` because a prover succeeded, where the **formalization is the
+  prover's own word** or its **vacuity was never checked** — two independent
+  ways a proof establishes nothing about a clause;
+- counting a witness bound to a **superseded state**, which an empty
+  footprint makes stale on any change at all;
+- silently discarding a witness whose obligation address is a clause's
+  **previous wording**, which is exactly how drift stops being visible;
+- reading `reviewed` off the evidence label when the **reviewer is the
+  clause's own author**.
+
+## Where the expected verdicts come from
+
+They are written by hand from §3 of the specification. They are **not**
+read back out of this implementation: a corpus whose expectations are
+whatever the code produced would certify agreement with itself and nothing
+else.
+
+That distinction earned its keep while this corpus was being written. Seven
+of the ten expectations were wrong on first authoring — all the same mistake,
+and the author's rather than the evaluator's. They assumed the attestation
+axis was computed from who signed a *witness*, when §2.8 computes it from who
+authored the *work*; with no work declared, attestation is absent. The fix was
+not to copy the observed value into the expectation, which would have hidden
+the misunderstanding, but to declare work in every case so that the axis is
+actually exercised.
+
+## Regenerating
+
+```
+JOULESPEC_GEN_EVALUATION=1 cargo test -p joulespec-core --test evaluation
+```
+
+That republishes the input files and the expectations **as the test states
+them**. Without the variable the test reads the published expectation back and
+asserts it still agrees with the test's own, so an expectation edited in one
+place and not the other fails rather than drifting.
diff --git a/joulespec/conformance/v1/harvest.toml b/joulespec/conformance/v1/harvest.toml
index fe57f532d..00e726d43 100644
--- a/joulespec/conformance/v1/harvest.toml
+++ b/joulespec/conformance/v1/harvest.toml
@@ -29,6 +29,10 @@ steward = "did:key:joulespec-reference-steward"
 document = "../../SPEC.md"
 section = "7. Conformance"
 expect_at_least = 11
+# `shape` is deliberately not declared here. Omitting it selects the numbered
+# conformance list this family's specifications use, which is what this
+# manifest was written against -- so this file also stands as the check that a
+# manifest predating the declared shape keeps every obligation address it had.
 intent = """
 The joulespec/1 reference implementation does what SPEC.md §7 says it does, \
 and each claim is evidenced by a check demonstrated capable of failing.\
@@ -125,12 +129,8 @@ anchor = "specification"
 footprint = ["crates/joulespec-core/src/conform.rs"]
 [evidence.counter]
 file = "crates/joulespec-core/src/conform.rs"
-find = """        .map(|c| c.grade)
-        .min()
-        .unwrap_or(None);"""
-replace = """        .map(|c| c.grade)
-        .max()
-        .unwrap_or(None);"""
+find = "    graded.into_iter().min().unwrap_or(None)"
+replace = "    graded.into_iter().max().unwrap_or(None)"
 breaks = "takes the strongest owed obligation instead of the weakest"
 
 [[evidence]]
@@ -189,12 +189,12 @@ anchor = "specification"
 footprint = ["crates/joulespec-core/src/conform.rs"]
 [evidence.counter]
 file = "crates/joulespec-core/src/conform.rs"
-find = """        if total == 0 {
-            return None;
-        }"""
-replace = """        if total == 0 {
-            return Some(0);
-        }"""
+find = """    if total == 0 {
+        return None;
+    }"""
+replace = """    if total == 0 {
+        return Some(0);
+    }"""
 breaks = "reports a ratio of nothing as zero rather than absent"
 
 # ── C8 — Receipts ─────────────────────────────────────────────────────────
@@ -320,3 +320,78 @@ find = """        let any_independent =
 replace = """        let any_independent = !implementers.is_empty();
         if any_independent {"""
 breaks = "calls agreement among implementers reproduction"
+
+# A proof, not a check. C7 says ratios are integer parts-per-million; the two
+# checks above cover the provenance rule and the absent-not-zero rule, and
+# neither covers whether the arithmetic on the way to the ratio is defined at
+# all. That is the half sampling cannot reach: the inputs that break it are a
+# `part` above roughly u64::MAX / 1_000_000, which no hand-written case picks.
+#
+# Measured on this workspace: the mutation below is invisible to the entire
+# test suite and refuted by the prover in a fraction of a second. That gap is
+# the reason the ladder has a rung above E3.
+#
+# The grounding is `declared`, so this witness is graded `E2` and not `E4`
+# (SPEC §2.6). Nobody independent of its author has confirmed that the
+# statement below says what C7 says, and recording the proof at its real rung
+# is the point of having the axis.
+[[evidence]]
+clause = "C7"
+check = "proofs::the_ratio_rule_is_total_over_every_input"
+anchor = "specification"
+footprint = [
+  "crates/joulespec-core/src/conform.rs",
+  "crates/joulespec-core/src/proofs.rs",
+]
+[evidence.formalization]
+package = "joulespec-core"
+grounding = "declared"
+budget_seconds = 300
+statement = """
+For all part, rest : u64 --- every arithmetic operation performed by
+conform::ppm(part, rest) is defined: none overflows and none divides by zero.
+Discharged over the whole input domain by the checker's arithmetic checks,
+with reachability covers for the absent case, the computed case, the
+overflowing-whole case, and a part large enough to overflow the scale in 64
+bits.
+
+The companion statement --- that the quotient is bounded by the scale --- is
+deliberately not made here. It requires the solver to reason about the output
+bits of a 128-bit division and did not converge; see the README.
+"""
+[evidence.counter]
+file = "crates/joulespec-core/src/conform.rs"
+find = "    Some(((u128::from(part) * 1_000_000) / u128::from(total)) as u64)"
+replace = "    Some((part * 1_000_000) / total)"
+breaks = "computes the scale in 64 bits, where a large part overflows it"
+
+# A second proof, on the property an adversary has the clearest incentive to
+# break. The statement is about `cap` itself -- the function the evaluator
+# calls -- so the counter-artifact below is an edit to the artifact, not to a
+# copy of the rule living inside the harness.
+[[evidence]]
+clause = "C5"
+check = "proofs::widening_a_set_can_only_lower_its_cap"
+anchor = "specification"
+footprint = [
+  "crates/joulespec-core/src/conform.rs",
+  "crates/joulespec-core/src/proofs.rs",
+]
+[evidence.formalization]
+package = "joulespec-core"
+grounding = "declared"
+budget_seconds = 300
+statement = """
+For every set of at most four graded figures and one added figure ---
+conform::cap(set) is None whenever any member is None; otherwise it is Some(b)
+for some b belonging to the set, and cap(set + extra) <= b; and cap can empty
+only because the added figure was itself absent. Discharged over every
+combination of ladder rungs and absences a set of that size admits, with
+reachability covers for the strictly-lower, unchanged, emptied and
+already-empty cases.
+"""
+[evidence.counter]
+file = "crates/joulespec-core/src/conform.rs"
+find = "    graded.into_iter().min().unwrap_or(None)"
+replace = "    graded.into_iter().max().unwrap_or(None)"
+breaks = "caps a set by its best figure instead of its worst"
diff --git a/joulespec/joulespec-rs/Cargo.lock b/joulespec/joulespec-rs/Cargo.lock
index e45e4385e..4f158e798 100644
--- a/joulespec/joulespec-rs/Cargo.lock
+++ b/joulespec/joulespec-rs/Cargo.lock
@@ -227,7 +227,7 @@ checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682"
 
 [[package]]
 name = "joulespec-cli"
-version = "0.2.0"
+version = "0.3.0"
 dependencies = [
  "blake3",
  "ed25519-dalek",
@@ -240,7 +240,7 @@ dependencies = [
 
 [[package]]
 name = "joulespec-core"
-version = "0.2.0"
+version = "0.3.0"
 dependencies = [
  "blake3",
  "ed25519-dalek",
diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/Cargo.toml b/joulespec/joulespec-rs/crates/joulespec-cli/Cargo.toml
index 955107c7a..dc398796e 100644
--- a/joulespec/joulespec-rs/crates/joulespec-cli/Cargo.toml
+++ b/joulespec/joulespec-rs/crates/joulespec-cli/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "joulespec-cli"
-version = "0.2.0"
+version = "0.3.0"
 description = "JouleSpec reference producer and checker: harvests signed witnesses from a project's own test suite, demonstrates each check against a counter-artifact, and seals a joulespec/1 receipt."
 edition.workspace = true
 license.workspace = true
diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/src/harvest.rs b/joulespec/joulespec-rs/crates/joulespec-cli/src/harvest.rs
index c89ba5af7..691ab1dae 100644
--- a/joulespec/joulespec-rs/crates/joulespec-cli/src/harvest.rs
+++ b/joulespec/joulespec-rs/crates/joulespec-cli/src/harvest.rs
@@ -29,11 +29,14 @@ use std::path::Path;
 
 use ed25519_dalek::SigningKey;
 use joulespec_core::conform::ArtifactState;
-use joulespec_core::evidence::{Anchor, Evidence, SignedWitness, Witness};
+use joulespec_core::evidence::{
+    Anchor, Evidence, Formalization, Grounding, SignedWitness, Vacuity, Witness,
+};
 use joulespec_core::spec::{Obligation, SignedSpec, Spec};
-use joulespec_core::{Energy, Provenance};
+use joulespec_core::{Address, Energy, Provenance};
 
 use crate::manifest::{Manifest, ManifestError};
+use crate::prover::{self, ProveError};
 use crate::runner::{self, RunError};
 use crate::specdoc::{self, SpecDocError};
 use crate::tree::{Tree, TreeError};
@@ -78,6 +81,12 @@ pub enum HarvestError {
     /// support.
     #[error("provenance {0:?} is not available to a harness with no meter")]
     BadProvenance(String),
+    /// The prover could not be run.
+    #[error(transparent)]
+    Prove(#[from] ProveError),
+    /// A cross-checking key is not 32 bytes of hex.
+    #[error("cross-checking key {0:?} is not 32 bytes of hex")]
+    BadKey(String),
 }
 
 /// What happened to one declared mapping.
@@ -135,13 +144,71 @@ pub enum Note {
         /// The check.
         check: String,
     },
+    /// No model checker is installed, so a declared proof could not be run.
+    ///
+    /// Recorded rather than skipped: an absent prover is why an obligation
+    /// has no proof evidence, and a report that omitted it would read like a
+    /// manifest that never declared one.
+    ProverAbsent {
+        /// The clause.
+        clause: String,
+        /// The harness.
+        check: String,
+    },
+    /// **A finding.** The harness declares no reachability cover, so its
+    /// success distinguishes an examined domain from an empty one (SPEC §2.6).
+    ProofDeclaresNoCover {
+        /// The clause.
+        clause: String,
+        /// The harness.
+        check: String,
+    },
+    /// **A finding.** The prover did not decide, so the declared evidence
+    /// does not exist — whatever the reason, the operator must either fix the
+    /// harness or stop claiming it.
+    ProofInconclusive {
+        /// The clause.
+        clause: String,
+        /// The harness.
+        check: String,
+        /// What was observed.
+        detail: String,
+    },
+    /// **A finding.** The statement holds, but over an empty domain: a cover
+    /// the harness declared names states that never occur.
+    ProofVacuous {
+        /// The clause.
+        clause: String,
+        /// The harness.
+        check: String,
+        /// How many declared covers were never reached.
+        unreached: usize,
+    },
+    /// The prover found the statement false. Either the artifact violates the
+    /// clause or the statement is not the clause; both need a human.
+    ProofDidNotHold {
+        /// The clause.
+        clause: String,
+        /// The harness.
+        check: String,
+        /// What was observed.
+        detail: String,
+    },
 }
 
 impl Note {
     /// Whether this note reports something the operator must act on.
     #[must_use]
     pub const fn is_finding(&self) -> bool {
-        matches!(self, Self::CounterDidNotFail { .. } | Self::CheckDidNotRun { .. })
+        matches!(
+            self,
+            Self::CounterDidNotFail { .. }
+                | Self::CheckDidNotRun { .. }
+                | Self::ProofDeclaresNoCover { .. }
+                | Self::ProofInconclusive { .. }
+                | Self::ProofVacuous { .. }
+                | Self::ProofDidNotHold { .. }
+        )
     }
 
     /// A line for the report.
@@ -167,6 +234,23 @@ impl Note {
             Self::NoCounterDeclared { clause, check } => {
                 format!("{clause:<5} E2  {check}: no counter-artifact declared")
             }
+            Self::ProverAbsent { clause, check } => {
+                format!("{clause:<5} --  {check}: no model checker installed; proof not run")
+            }
+            Self::ProofDeclaresNoCover { clause, check } => format!(
+                "{clause:<5} --  {check}: FINDING -- the harness declares no cover, so \
+                 its success shows nothing was examined"
+            ),
+            Self::ProofInconclusive { clause, check, detail } => format!(
+                "{clause:<5} --  {check}: FINDING -- the prover did not decide ({detail})"
+            ),
+            Self::ProofVacuous { clause, check, unreached } => format!(
+                "{clause:<5} --  {check}: FINDING -- proved over an empty domain; \
+                 {unreached} declared cover(s) never reached"
+            ),
+            Self::ProofDidNotHold { clause, check, detail } => format!(
+                "{clause:<5} --  {check}: FINDING -- the statement does not hold ({detail})"
+            ),
         }
     }
 }
@@ -200,6 +284,29 @@ fn anchor_of(name: &str) -> Result<Anchor, HarvestError> {
     }
 }
 
+/// Read a declared grounding, with the key it names.
+///
+/// The manifest schema has already refused an unknown grounding and a
+/// cross-check with no key, so the only work left is decoding the key.
+fn grounding_of(f: &crate::manifest::Formalization) -> Result<Grounding, HarvestError> {
+    match f.grounding.as_str() {
+        "cross-checked" => {
+            let hex = f.by.as_deref().unwrap_or_default();
+            let raw = (0..hex.len())
+                .step_by(2)
+                .map(|i| u8::from_str_radix(hex.get(i..i + 2).unwrap_or("zz"), 16))
+                .collect::<Result<Vec<u8>, _>>()
+                .map_err(|_| HarvestError::BadKey(hex.to_string()))?;
+            let by: [u8; 32] = raw
+                .try_into()
+                .map_err(|_| HarvestError::BadKey(hex.to_string()))?;
+            Ok(Grounding::CrossChecked { by })
+        }
+        // `declared` is the only other value the schema admits.
+        _ => Ok(Grounding::Declared),
+    }
+}
+
 fn provenance_of(name: &str) -> Result<Provenance, HarvestError> {
     match name {
         "estimator" => Ok(Provenance::Estimator),
@@ -233,13 +340,19 @@ pub fn harvest(
         path: doc_path.to_string_lossy().into_owned(),
         source,
     })?;
+    let shape = match manifest.spec.shape.as_deref() {
+        Some(name) => specdoc::Shape::parse(name)?,
+        None => specdoc::Shape::default(),
+    };
     let items = specdoc::items(
         &document,
         &manifest.spec.section,
         manifest.spec.expect_at_least,
+        shape,
     )?;
     let labels: Vec<String> = items.iter().map(|i| i.label.clone()).collect();
     manifest.check_clauses(&labels)?;
+    manifest.check_counters(&workspace)?;
 
     let spec = Spec::new(
         manifest.spec.intent.clone(),
@@ -281,6 +394,160 @@ pub fn harvest(
         let anchor = anchor_of(&entry.anchor)?;
         let footprint = tree.footprint(&entry.footprint)?;
 
+        // ── a declared proof takes the prover, not the test harness ──────
+        //
+        // The two paths stay separate rather than sharing a "run it" step,
+        // because what counts as having established something differs: a
+        // test must have run, a proof must have examined a non-empty domain.
+        // Collapsing them would lose exactly that distinction.
+        if let Some(f) = &entry.formalization {
+            if !prover::available(&workspace) {
+                notes.push(Note::ProverAbsent {
+                    clause: entry.clause.clone(),
+                    check: entry.check.clone(),
+                });
+                continue;
+            }
+            let budget = std::time::Duration::from_secs(f.budget_seconds.unwrap_or(1800));
+            let baseline = prover::prove(&workspace, &f.package, &entry.check, &[], budget)?;
+            let mut uj = microjoules(baseline.seconds, manifest.energy.watts);
+
+            if baseline.declares_no_cover() {
+                notes.push(Note::ProofDeclaresNoCover {
+                    clause: entry.clause.clone(),
+                    check: entry.check.clone(),
+                });
+                continue;
+            }
+            if baseline.is_inconclusive() {
+                notes.push(Note::ProofInconclusive {
+                    clause: entry.clause.clone(),
+                    check: entry.check.clone(),
+                    detail: format!(
+                        "{} undecided, verdict {}, budget {}s",
+                        baseline.undetermined,
+                        baseline.verdict.map_or("none", |v| if v { "success" } else { "failure" }),
+                        budget.as_secs()
+                    ),
+                });
+                continue;
+            }
+            if baseline.covers_unreached() > 0 {
+                notes.push(Note::ProofVacuous {
+                    clause: entry.clause.clone(),
+                    check: entry.check.clone(),
+                    unreached: baseline.covers_unreached(),
+                });
+                continue;
+            }
+            if !baseline.demonstrates_proof() {
+                notes.push(Note::ProofDidNotHold {
+                    clause: entry.clause.clone(),
+                    check: entry.check.clone(),
+                    detail: format!("{} assertion(s) violated", baseline.assertions_failed),
+                });
+                continue;
+            }
+
+            // The goal the prover decided. Addressing the harness identity
+            // together with the statement names what was actually decided —
+            // it is not a stand-in for a decision that did not happen, and
+            // the artifact state the witness carries pins the code it ran on.
+            let goal = Address::of(&serde_json::json!({
+                "package": f.package,
+                "harness": entry.check,
+                "statement": f.statement,
+            }))?;
+            let grounding = grounding_of(f)?;
+            let mut vacuity = Vacuity::Unchecked;
+            let mut note = Note::NoCounterDeclared {
+                clause: entry.clause.clone(),
+                check: entry.check.clone(),
+            };
+
+            if let Some(counter) = &entry.counter {
+                let (run, counter_address) = {
+                    let _mutation = runner::Mutation::apply(
+                        &workspace,
+                        &counter.file,
+                        &counter.find,
+                        &counter.replace,
+                    )?;
+                    let mutated = tree.reread(
+                        &manifest.artifact.dirs,
+                        &manifest.artifact.files,
+                        &manifest.artifact.extensions,
+                    )?;
+                    (
+                        prover::prove(&workspace, &f.package, &entry.check, &[], budget)?,
+                        mutated.address(),
+                    )
+                };
+                uj = uj.saturating_add(microjoules(run.seconds, manifest.energy.watts));
+
+                if run.demonstrates_refutation() {
+                    vacuity = Vacuity::Refuted { counter: counter_address };
+                    note = Note::Witnessed {
+                        clause: entry.clause.clone(),
+                        check: entry.check.clone(),
+                        grade: if matches!(grounding, Grounding::CrossChecked { .. }) {
+                            "E4"
+                        } else {
+                            // §2.6: a formalization nobody independent read
+                            // leaves machine-checked evidence about something,
+                            // which is `E2`. Reported here so the demotion is
+                            // visible rather than surprising in the receipt.
+                            "E2 (proof, declared grounding)"
+                        },
+                        detail: format!("refuted when {}", counter.breaks),
+                    };
+                } else if run.is_inconclusive() {
+                    note = Note::CounterInconclusive {
+                        clause: entry.clause.clone(),
+                        check: entry.check.clone(),
+                        detail: "the prover did not decide the mutated statement".to_string(),
+                    };
+                } else {
+                    note = Note::CounterDidNotFail {
+                        clause: entry.clause.clone(),
+                        check: entry.check.clone(),
+                        breaks: counter.breaks.clone(),
+                    };
+                }
+            }
+
+            if matches!(note, Note::NoCounterDeclared { .. }) {
+                note = Note::Witnessed {
+                    clause: entry.clause.clone(),
+                    check: entry.check.clone(),
+                    grade: "E2 (proof, vacuity unchecked)",
+                    detail: "no counter-artifact declared".to_string(),
+                };
+            }
+
+            let witness = Witness::new(
+                spec_id.clone(),
+                obligation,
+                state.address.clone(),
+                Evidence::Proved {
+                    goal,
+                    tier: "bit-precise-model-check".to_string(),
+                    formalization: Formalization {
+                        statement: f.statement.clone(),
+                        grounding,
+                    },
+                    vacuity,
+                },
+                Energy::new(uj, provenance),
+                witness_key.verifying_key().to_bytes(),
+            )
+            .with_footprint(footprint)
+            .sign(witness_key)?;
+            witnesses.push(witness);
+            notes.push(note);
+            continue;
+        }
+
         let baseline = runner::run_check(&workspace, &entry.check)?;
         if baseline.compiled && baseline.ran == 0 {
             notes.push(Note::CheckDidNotRun {
diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/src/main.rs b/joulespec/joulespec-rs/crates/joulespec-cli/src/main.rs
index a70c60ce0..4f38250ac 100644
--- a/joulespec/joulespec-rs/crates/joulespec-cli/src/main.rs
+++ b/joulespec/joulespec-rs/crates/joulespec-cli/src/main.rs
@@ -22,6 +22,7 @@
 
 mod harvest;
 mod manifest;
+mod prover;
 mod runner;
 mod specdoc;
 mod tree;
diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/src/manifest.rs b/joulespec/joulespec-rs/crates/joulespec-cli/src/manifest.rs
index e612e7c89..817a44c62 100644
--- a/joulespec/joulespec-rs/crates/joulespec-cli/src/manifest.rs
+++ b/joulespec/joulespec-rs/crates/joulespec-cli/src/manifest.rs
@@ -46,6 +46,38 @@ pub enum ManifestError {
     /// failure this standard exists to surface.
     #[error("the manifest declares no evidence")]
     NoEvidence,
+    /// A formalization declares a grounding this standard does not define.
+    #[error("clause {clause:?} declares grounding {grounding:?}, which is neither `declared` nor `cross-checked`")]
+    UnknownGrounding {
+        /// The clause.
+        clause: String,
+        /// The grounding as written.
+        grounding: String,
+    },
+    /// A counter-artifact's anchor text is not in the file exactly once, so
+    /// the mutation it describes cannot be applied where it was meant to go.
+    #[error(
+        "clause {clause:?} check {check:?}: the counter-artifact anchor occurs \
+         {found} times in {file}, not once"
+    )]
+    CounterAnchorMissing {
+        /// The clause.
+        clause: String,
+        /// The check.
+        check: String,
+        /// The file.
+        file: String,
+        /// How many times the anchor was found.
+        found: usize,
+    },
+    /// A cross-checked formalization names no confirming key, so there is
+    /// nothing to compare against the witness author and no way to tell
+    /// independent confirmation from self-assertion.
+    #[error("clause {clause:?} is cross-checked but names no confirming key")]
+    UnnamedCrossCheck {
+        /// The clause.
+        clause: String,
+    },
 }
 
 /// Where the clauses come from.
@@ -58,6 +90,13 @@ pub struct SpecSource {
     /// The floor on item count. A parser that matched nothing would otherwise
     /// report success having checked nothing.
     pub expect_at_least: usize,
+    /// Which conventional shape the document writes its requirements in.
+    ///
+    /// Declared because it is a fact about the document, not about this
+    /// producer. Omitted means a numbered list of bolded, labelled items —
+    /// what this family's own specifications use — so an existing manifest
+    /// keeps its obligation addresses unchanged.
+    pub shape: Option<String>,
     /// The specification's intent, in the operator's words.
     pub intent: String,
 }
@@ -100,6 +139,37 @@ pub struct Counter {
     pub breaks: String,
 }
 
+/// The binding from clause prose to a formal statement.
+///
+/// Supplied by the operator, never derived: SPEC §2.6 forbids a producer
+/// formalizing a clause on its own initiative, because the binding between
+/// prose and a formal statement is a human act and the weakest link in any
+/// claim of proved conformance.
+///
+/// Its **presence is what makes an entry a proof**. The schema offers no way
+/// to declare a proof without one, which is how the §2.6 rule is enforced
+/// structurally rather than by a check that could be forgotten.
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub struct Formalization {
+    /// The statement the harness discharges, in the operator's words.
+    pub statement: String,
+    /// `declared`, or `cross-checked` when an independent party confirmed the
+    /// statement says what the clause says.
+    pub grounding: String,
+    /// The confirming party's verifying key, hex, when cross-checked.
+    pub by: Option<String>,
+    /// The package holding the harness.
+    pub package: String,
+    /// The wall-clock budget for the prover, in seconds.
+    ///
+    /// Per harness, because the cost of discharging a statement varies by
+    /// orders of magnitude with what it quantifies over, and a single
+    /// workspace-wide figure would be either too small for the statements
+    /// worth proving or too large to be a gate. Exceeding it is reported as
+    /// an undecided run, never as a pass or a refutation.
+    pub budget_seconds: Option<u64>,
+}
+
 /// One declared mapping from an obligation to a check.
 #[derive(Debug, Clone, Serialize, Deserialize)]
 pub struct Evidence {
@@ -116,6 +186,9 @@ pub struct Evidence {
     /// The counter-artifact that should make it fail. Without one the check
     /// cannot exceed `E2` however carefully it was written.
     pub counter: Option<Counter>,
+    /// When present, `check` names a proof harness rather than a test, and
+    /// this is its binding to the clause.
+    pub formalization: Option<Formalization>,
 }
 
 /// The whole manifest.
@@ -153,10 +226,59 @@ impl Manifest {
                     check: e.check.clone(),
                 });
             }
+            if let Some(f) = &e.formalization {
+                match f.grounding.as_str() {
+                    "declared" => {}
+                    "cross-checked" => {
+                        if f.by.is_none() {
+                            return Err(ManifestError::UnnamedCrossCheck {
+                                clause: e.clause.clone(),
+                            });
+                        }
+                    }
+                    other => {
+                        return Err(ManifestError::UnknownGrounding {
+                            clause: e.clause.clone(),
+                            grounding: other.to_string(),
+                        });
+                    }
+                }
+            }
         }
         Ok(manifest)
     }
 
+    /// Check every counter-artifact's anchor text is present exactly once,
+    /// before anything is run.
+    ///
+    /// A refactor can move the code a mutation was aimed at without touching
+    /// the manifest, which leaves the counter-artifact pointing at text that
+    /// no longer exists. Discovering that part-way through a harvest wastes
+    /// the runs already done; discovering it by *tolerating* it would be
+    /// worse, because a clause would quietly stop being falsifiably evidenced
+    /// while its entry still looked present. This has happened once in this
+    /// repository, to two entries, from one extraction of a function.
+    pub fn check_counters(&self, workspace: &std::path::Path) -> Result<(), ManifestError> {
+        for e in &self.evidence {
+            let Some(counter) = &e.counter else { continue };
+            let path = workspace.join(&counter.file);
+            let text = std::fs::read_to_string(&path).map_err(|source| ManifestError::Io {
+                path: path.to_string_lossy().into_owned(),
+                source,
+            })?;
+            let found = text.matches(&counter.find).count();
+            if found != 1 {
+                return Err(ManifestError::CounterAnchorMissing {
+                    clause: e.clause.clone(),
+                    check: e.check.clone(),
+                    file: counter.file.clone(),
+                    found,
+                });
+            }
+        }
+        Ok(())
+    }
+
     /// Check every evidence entry names a clause the specification states.
     ///
     /// An entry for an unknown clause would otherwise become an `unbound`
@@ -244,6 +366,36 @@ breaks = "puts the label back into the obligation address"
         ));
     }
 
+    /// The incident this guards against: a refactor moves the code a
+    /// mutation was aimed at, and the manifest still names the old text.
+    #[test]
+    fn a_counter_artifact_aimed_at_vanished_text_is_caught_before_anything_runs() {
+        let (dir, path) = write(MANIFEST);
+        let m = Manifest::read(&path).unwrap();
+        let src = dir.path().join("crates/joulespec-core/src");
+        std::fs::create_dir_all(&src).unwrap();
+        let file = src.join("spec.rs");
+
+        std::fs::write(&file, "x\n\"kind\": self.kind.label(), \"text\": self.text\ny\n").unwrap();
+        assert!(m.check_counters(dir.path()).is_ok(), "the anchor is present once");
+
+        // The same edit a refactor would make: the text moves or changes.
+        std::fs::write(&file, "x\nthe anchor is gone\ny\n").unwrap();
+        assert!(matches!(
+            m.check_counters(dir.path()),
+            Err(ManifestError::CounterAnchorMissing { found: 0, .. })
+        ));
+
+        // Two copies are refused too: a mutation that could land in either
+        // place has not described one artifact state.
+        let twice = "\"kind\": self.kind.label(), \"text\": self.text";
+        std::fs::write(&file, format!("{twice}\n{twice}\n")).unwrap();
+        assert!(matches!(
+            m.check_counters(dir.path()),
+            Err(ManifestError::CounterAnchorMissing { found: 2, .. })
+        ));
+    }
+
     #[test]
     fn evidence_for_an_unstated_clause_is_caught_before_sealing() {
         let (_d, path) = write(MANIFEST);
diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/src/prover.rs b/joulespec/joulespec-rs/crates/joulespec-cli/src/prover.rs
new file mode 100644
index 000000000..aefb43c76
--- /dev/null
+++ b/joulespec/joulespec-rs/crates/joulespec-cli/src/prover.rs
@@ -0,0 +1,456 @@
+//! Running a proof harness, and running it against a counter-artifact.
+//!
+//! This is [`runner`](crate::runner) one rung up, and the reasoning is
+//! deliberately the same shape — because the failure it guards against is the
+//! same one.
+//!
+//! ## Why a success verdict is not enough
+//!
+//! A model checker reports success for a harness whose assumptions have
+//! eliminated the states the statement was about, in the same words it uses
+//! for a harness that examined all of them. An over-constrained harness is
+//! the proof-level equivalent of `running 0 tests`: the tool is not lying,
+//! it is answering a question nobody meant to ask.
+//!
+//! A reachability **cover** is how a harness says which states its statement
+//! is supposed to be about. Covers are reported per property as `SATISFIED`,
+//! `UNSATISFIABLE`, `UNREACHABLE` or `UNDETERMINED` — and an unreachable
+//! cover does *not* fail the run. A gate reading only the final verdict line
+//! therefore passes vacuous proofs, which is why this module parses the
+//! property table and requires every declared cover to be satisfied.
+//!
+//! ## The four outcomes
+//!
+//! | Outcome | Meaning |
+//! |---|---|
+//! | verified, every cover satisfied | The statement holds over the examined domain, and the domain is not empty. |
+//! | verified, a cover unsatisfied | **A flag**: the harness proved something about nothing. |
+//! | a property failed | The statement does not hold. Against a counter-artifact, this is the refutation. |
+//! | undetermined, or no verdict | **A flag**: the prover did not decide. Neither success nor failure, and never credited as either. |
+//!
+//! The fourth row is the one a tested-against-success-only parser gets wrong.
+//! A solver that runs out of time or meets an unsupported construct has
+//! established nothing, and treating it as a refutation would hand out `E4`
+//! for a timeout.
+
+use std::io::Read;
+use std::os::unix::process::CommandExt;
+use std::path::PathBuf;
+use std::process::Command;
+use std::time::{Duration, Instant};
+
+/// Why a proof could not be run.
+#[derive(Debug, thiserror::Error)]
+pub enum ProveError {
+    /// The prover could not be launched.
+    #[error("cannot run the prover in {dir}: {source}")]
+    Spawn {
+        /// The working directory.
+        dir: PathBuf,
+        /// The underlying error.
+        source: std::io::Error,
+    },
+}
+
+/// How one property was decided.
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+enum Status {
+    /// An assertion held, or a cover was satisfied.
+    Good,
+    /// An assertion was violated.
+    Failed,
+    /// A cover could not be reached, so the states it names never occur.
+    Unreached,
+    /// The prover did not decide.
+    Undetermined,
+}
+
+/// The observed outcome of one proof run.
+#[derive(Debug, Clone, PartialEq)]
+pub struct Proof {
+    /// Assertions the prover decided favourably.
+    pub assertions_held: usize,
+    /// Assertions the prover found violated.
+    pub assertions_failed: usize,
+    /// Properties of either kind the prover could not decide.
+    pub undetermined: usize,
+    /// Reachability covers the harness declared.
+    pub covers: usize,
+    /// Covers shown to be reachable.
+    pub covers_satisfied: usize,
+    /// The final verdict line, when the prover printed one.
+    pub verdict: Option<bool>,
+    /// Wall-clock seconds for the run.
+    pub seconds: f64,
+}
+
+impl Proof {
+    /// Whether this run establishes the statement over a non-empty domain.
+    ///
+    /// Every condition is load-bearing. Dropping the cover conditions admits
+    /// an over-constrained harness; dropping the undetermined condition
+    /// admits a partial decision; dropping the verdict condition trusts a
+    /// property table that may have been truncated by a crash.
+    #[must_use]
+    pub fn demonstrates_proof(&self) -> bool {
+        self.verdict == Some(true)
+            && self.assertions_failed == 0
+            && self.undetermined == 0
+            && self.assertions_held >= 1
+            && self.covers >= 1
+            && self.covers_satisfied == self.covers
+    }
+
+    /// Whether this run refutes the statement — the signal a counter-artifact
+    /// is applied to obtain.
+    ///
+    /// A violated assertion, not merely the absence of success: a prover that
+    /// timed out has demonstrated nothing, and crediting that as a refutation
+    /// would award `E4` for running out of time.
+    #[must_use]
+    pub fn demonstrates_refutation(&self) -> bool {
+        self.assertions_failed >= 1 && self.verdict == Some(false)
+    }
+
+    /// Whether the harness declared no cover, and so offered nothing to
+    /// distinguish an examined domain from an empty one.
+    #[must_use]
+    pub fn declares_no_cover(&self) -> bool {
+        self.covers == 0
+    }
+
+    /// Whether the prover failed to decide, by any of the ways it can.
+    #[must_use]
+    pub fn is_inconclusive(&self) -> bool {
+        self.verdict.is_none() || self.undetermined >= 1
+    }
+
+    /// Covers the harness declared that name states which never occur.
+    #[must_use]
+    pub fn covers_unreached(&self) -> usize {
+        self.covers.saturating_sub(self.covers_satisfied)
+    }
+}
+
+/// Parse a prover's property table and verdict out of its output.
+///
+/// Written against the documented table rather than the verdict line, for the
+/// reason in the module header. Unknown statuses count as undetermined: a
+/// status this parser does not recognize is a property it cannot vouch for,
+/// and the conservative reading is the one that refuses to grade.
+#[must_use]
+pub fn parse(output: &str) -> Proof {
+    let mut p = Proof {
+        assertions_held: 0,
+        assertions_failed: 0,
+        undetermined: 0,
+        covers: 0,
+        covers_satisfied: 0,
+        verdict: None,
+        seconds: 0.0,
+    };
+    // Which kind of property the next `Status:` line belongs to. The check
+    // line names it; the status arrives on a later line.
+    let mut pending_cover = false;
+
+    for line in output.lines() {
+        let t = line.trim();
+        if let Some(rest) = t.strip_prefix("Check ") {
+            // `Check 3: harness.cover.2`, `...assertion.1`,
+            // `...arithmetic_overflow.1`, and others.
+            //
+            // Only covers are identified positively. Every other property
+            // class is read as a check, because the classes are open-ended
+            // and the interesting failures do not all arrive as assertions:
+            // a counter-artifact that introduces an integer overflow is
+            // reported as `arithmetic_overflow`, and a parser matching only
+            // `assertion` would see a clean table and call the mutated run
+            // inconclusive — or worse, proved.
+            pending_cover = rest.contains(".cover.");
+            if pending_cover {
+                p.covers += 1;
+            }
+            continue;
+        }
+        if let Some(status) = t.strip_prefix("- Status: ") {
+            let s = match status.trim() {
+                "SUCCESS" | "SATISFIED" => Status::Good,
+                "FAILURE" => Status::Failed,
+                "UNREACHABLE" | "UNSATISFIABLE" => Status::Unreached,
+                _ => Status::Undetermined,
+            };
+            match (pending_cover, s) {
+                (true, Status::Good) => p.covers_satisfied += 1,
+                // An unreachable cover is the vacuity signal, not a failure:
+                // it is counted by its absence from `covers_satisfied`.
+                (true, Status::Unreached) => {}
+                (true, Status::Undetermined | Status::Failed) => p.undetermined += 1,
+                (false, Status::Good) => p.assertions_held += 1,
+                (false, Status::Failed) => p.assertions_failed += 1,
+                // An unreachable *assertion* is dead code under the harness's
+                // assumptions, not a decision about the statement.
+                (false, Status::Unreached) => {}
+                (false, Status::Undetermined) => p.undetermined += 1,
+            }
+            continue;
+        }
+        if let Some(v) = t.strip_prefix("VERIFICATION:- ") {
+            p.verdict = Some(v.trim() == "SUCCESSFUL");
+        }
+    }
+    p
+}
+
+/// Run one proof harness in `dir` under a wall-clock budget, and parse what
+/// the prover decided.
+///
+/// The budget is not a convenience. A solver asked a question it cannot
+/// settle does not report that — it keeps going, and an unbounded producer
+/// stops being a gate and becomes a hang. Exceeding the budget leaves no
+/// verdict line, so the run reads as inconclusive, which is the honest
+/// answer: nothing was established, within this budget, about this statement.
+///
+/// Output is drained by a thread per stream rather than written to a file. A
+/// prover emits a great deal on its way to a verdict, so a pipe nobody reads
+/// fills and blocks the child — which looks exactly like the hang the budget
+/// exists to prevent. A temporary file would do as well until the host it
+/// runs on has no space for one, and then it would fail in a way that reads
+/// like the prover declining to answer.
+pub fn prove(
+    dir: &std::path::Path,
+    package: &str,
+    harness: &str,
+    extra: &[String],
+    budget: Duration,
+) -> Result<Proof, ProveError> {
+    let started = Instant::now();
+    let spawned = |source| ProveError::Spawn {
+        dir: dir.to_path_buf(),
+        source,
+    };
+    let mut child = Command::new("cargo")
+        .current_dir(dir)
+        .arg("kani")
+        .args(["-p", package, "--harness", harness])
+        .args(extra)
+        .stdout(std::process::Stdio::piped())
+        .stderr(std::process::Stdio::piped())
+        // Its own group, so the budget can reach the solver. The prover is a
+        // driver that spawns the checker, and killing only the driver leaves
+        // the expensive process running — observed, not hypothesized.
+        .process_group(0)
+        .spawn()
+        .map_err(spawned)?;
+
+    let drain = |stream: Option<Box<dyn std::io::Read + Send>>| {
+        std::thread::spawn(move || {
+            let mut buf = String::new();
+            if let Some(mut s) = stream {
+                let _ = s.read_to_string(&mut buf);
+            }
+            buf
+        })
+    };
+    let out = drain(child.stdout.take().map(|s| Box::new(s) as Box<dyn std::io::Read + Send>));
+    let err = drain(child.stderr.take().map(|s| Box::new(s) as Box<dyn std::io::Read + Send>));
+
+    let mut over_budget = false;
+    loop {
+        if child.try_wait().map_err(spawned)?.is_some() {
+            break;
+        }
+        if started.elapsed() > budget {
+            let _ = Command::new("kill")
+                .arg("-9")
+                .arg(format!("-{}", child.id()))
+                .status();
+            let _ = child.wait();
+            over_budget = true;
+            break;
+        }
+        std::thread::sleep(Duration::from_millis(250));
+    }
+
+    let mut text = out.join().unwrap_or_default();
+    text.push_str(&err.join().unwrap_or_default());
+    let mut p = parse(&text);
+    p.seconds = started.elapsed().as_secs_f64();
+    if over_budget {
+        // A killed run can leave a property table that looks healthy as far
+        // as it got. Clearing the verdict is what makes `is_inconclusive`
+        // true, and the budget is the reason there is no verdict to report.
+        p.verdict = None;
+    }
+    Ok(p)
+}
+
+/// Whether a model checker is available to run at all.
+#[must_use]
+pub fn available(dir: &std::path::Path) -> bool {
+    Command::new("cargo")
+        .current_dir(dir)
+        .args(["kani", "--version"])
+        .output()
+        .is_ok_and(|o| o.status.success())
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    /// A harness that examined its domain and held.
+    const HELD: &str = "\
+RESULTS:
+Check 1: ppm.assertion.1
+         - Status: SUCCESS
+         - Description: \"a share of a whole cannot exceed the whole\"
+
+Check 2: ppm.cover.1
+         - Status: SATISFIED
+         - Description: \"cover condition: the whole-scale case\"
+         - Location: src/proofs.rs:40:5
+
+Check 3: ppm.cover.2
+         - Status: SATISFIED
+         - Description: \"cover condition: the none-of-it case\"
+         - Location: src/proofs.rs:41:5
+
+SUMMARY:
+ ** 0 of 3 failed
+
+ ** 2 of 2 cover properties satisfied
+
+VERIFICATION:- SUCCESSFUL
+";
+
+    #[test]
+    fn a_harness_that_examined_its_domain_and_held_is_usable() {
+        let p = parse(HELD);
+        assert_eq!(p.covers, 2);
+        assert_eq!(p.covers_satisfied, 2);
+        assert_eq!(p.assertions_held, 1);
+        assert!(p.demonstrates_proof());
+        assert!(!p.demonstrates_refutation());
+        assert!(!p.is_inconclusive());
+        assert!(!p.declares_no_cover());
+    }
+
+    /// The trap this module exists for: the verdict line says success while a
+    /// declared cover was never reached, so the statement holds over a domain
+    /// the harness's own assumptions emptied.
+    #[test]
+    fn a_successful_verdict_with_an_unreachable_cover_proves_nothing() {
+        let log = HELD.replace(
+            "Check 3: ppm.cover.2\n         - Status: SATISFIED",
+            "Check 3: ppm.cover.2\n         - Status: UNREACHABLE",
+        );
+        let p = parse(&log);
+        assert_eq!(p.verdict, Some(true), "the prover still reports success");
+        assert_eq!(p.covers, 2);
+        assert_eq!(p.covers_satisfied, 1);
+        assert_eq!(p.covers_unreached(), 1);
+        assert!(
+            !p.demonstrates_proof(),
+            "a vacuous harness must not be usable as evidence"
+        );
+    }
+
+    /// An unsatisfiable cover is the same failure wearing a different word.
+    #[test]
+    fn an_unsatisfiable_cover_is_treated_as_unreached() {
+        let log = HELD.replace("- Status: SATISFIED", "- Status: UNSATISFIABLE");
+        let p = parse(&log);
+        assert_eq!(p.covers_satisfied, 0);
+        assert!(!p.demonstrates_proof());
+    }
+
+    #[test]
+    fn a_violated_assertion_is_the_refutation_a_counter_artifact_seeks() {
+        let log = HELD
+            .replace("- Status: SUCCESS", "- Status: FAILURE")
+            .replace("VERIFICATION:- SUCCESSFUL", "VERIFICATION:- FAILED");
+        let p = parse(&log);
+        assert_eq!(p.assertions_failed, 1);
+        assert!(p.demonstrates_refutation());
+        assert!(!p.demonstrates_proof());
+    }
+
+    /// Not every refutation arrives as an assertion. A counter-artifact that
+    /// narrows an integer type is refuted by an overflow check, which is a
+    /// different property class — and a parser that matched only `assertion`
+    /// would read this table as clean.
+    #[test]
+    fn a_refutation_in_another_property_class_is_still_a_refutation() {
+        let log = "\
+RESULTS:
+Check 1: ppm.arithmetic_overflow.1
+         - Status: FAILURE
+         - Description: \"attempt to multiply with overflow\"
+
+Check 2: ppm.cover.1
+         - Status: SATISFIED
+         - Description: \"cover condition: the whole-scale case\"
+
+VERIFICATION:- FAILED
+";
+        let p = parse(log);
+        assert_eq!(p.assertions_failed, 1, "the overflow check must be counted");
+        assert!(p.demonstrates_refutation());
+        assert!(!p.demonstrates_proof());
+    }
+
+    /// The costliest confusion available: a prover that ran out of resources
+    /// has established nothing, and crediting it as a refutation would hand
+    /// out the top rung for a timeout.
+    #[test]
+    fn an_undecided_property_is_neither_a_proof_nor_a_refutation() {
+        let log = HELD.replace("- Status: SUCCESS", "- Status: UNDETERMINED");
+        let p = parse(&log);
+        assert_eq!(p.undetermined, 1);
+        assert!(p.is_inconclusive());
+        assert!(!p.demonstrates_proof());
+        assert!(
+            !p.demonstrates_refutation(),
+            "an undecided property is not a refutation"
+        );
+    }
+
+    /// A prover killed mid-run leaves a property table with no verdict. The
+    /// table may look entirely healthy, which is why the verdict is required
+    /// rather than inferred from the checks that did print.
+    #[test]
+    fn a_run_with_no_verdict_line_is_inconclusive() {
+        let truncated = HELD.split("SUMMARY:").next().unwrap();
+        let p = parse(truncated);
+        assert_eq!(p.verdict, None);
+        assert_eq!(p.covers_satisfied, 2, "the table itself looks healthy");
+        assert!(p.is_inconclusive());
+        assert!(!p.demonstrates_proof());
+        assert!(!p.demonstrates_refutation());
+    }
+
+    #[test]
+    fn a_harness_declaring_no_cover_is_caught_before_it_is_graded() {
+        let log = "\
+RESULTS:
+Check 1: ppm.assertion.1
+         - Status: SUCCESS
+         - Description: \"holds\"
+
+VERIFICATION:- SUCCESSFUL
+";
+        let p = parse(log);
+        assert!(p.declares_no_cover());
+        assert!(!p.demonstrates_proof());
+    }
+
+    /// A status this parser does not know is a property it cannot vouch for.
+    #[test]
+    fn an_unrecognized_status_is_read_conservatively() {
+        let log = HELD.replace("- Status: SUCCESS", "- Status: SOMETHING_NEW");
+        let p = parse(&log);
+        assert_eq!(p.undetermined, 1);
+        assert!(p.is_inconclusive());
+        assert!(!p.demonstrates_proof());
+    }
+}
diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/src/specdoc.rs b/joulespec/joulespec-rs/crates/joulespec-cli/src/specdoc.rs
index 3710b1720..e20732309 100644
--- a/joulespec/joulespec-rs/crates/joulespec-cli/src/specdoc.rs
+++ b/joulespec/joulespec-rs/crates/joulespec-cli/src/specdoc.rs
@@ -7,7 +7,24 @@
 //! address moves, so every witness bound to the old wording stops applying,
 //! automatically (SPEC §4.2).
 //!
-//! The format recognised is a numbered list of bolded, labelled items under a
+//! ## The shape is declared, not assumed
+//!
+//! A producer that could only read documents written like this family's own
+//! specifications would be a tool for one organisation. Requirements live in
+//! several conventional shapes — numbered conformance lists, bulleted
+//! requirement tables, a heading per requirement carrying its identifier —
+//! and which one a document uses is a fact about the document, so the
+//! manifest declares it (see [`Shape`]). Nothing else about the extraction
+//! varies: the section is still named, the floor still fails closed, and
+//! continuation lines still join the same way.
+//!
+//! Changing the declared shape changes which text is captured, and therefore
+//! moves every obligation address. That is correct rather than unfortunate —
+//! a different extraction really does describe different obligations — but it
+//! means the shape is part of what an auditor needs in order to recompute the
+//! addresses, alongside the document itself.
+//!
+//! The default shape is a numbered list of bolded, labelled items under a
 //! named section, which is how this family's specifications write their
 //! conformance lists:
 //!
@@ -32,11 +49,24 @@ pub enum SpecDocError {
     /// The named section is not in the document.
     #[error("the document has no section headed {0:?}")]
     NoSection(String),
-    /// The section is there and holds no recognisable items. Fail closed: a
-    /// parser that returns an empty clause list would make every obligation
-    /// vacuously satisfied.
-    #[error("section {0:?} contains no numbered `**Cn — Name.** text` items")]
-    NoItems(String),
+    /// The section is there and holds no items of the declared shape. Fail
+    /// closed: a parser that returns an empty clause list would make every
+    /// obligation vacuously satisfied.
+    #[error("section {section:?} contains no items of shape {shape:?}")]
+    NoItems {
+        /// The section searched.
+        section: String,
+        /// The shape that matched nothing.
+        shape: &'static str,
+    },
+    /// The declared shape is not one this producer implements.
+    #[error("unknown clause shape {got:?}; expected one of {known}")]
+    UnknownShape {
+        /// The shape as declared.
+        got: String,
+        /// The shapes available.
+        known: String,
+    },
     /// Fewer items than the caller said to expect.
     #[error("expected at least {expected} items in section {section:?}, found {found}")]
     TooFew {
@@ -63,6 +93,67 @@ pub struct Item {
     pub text: String,
 }
 
+/// Which conventional shape a document writes its requirements in.
+///
+/// Three, because three are what documents actually use. Each one names how
+/// an item *opens*; how a label, a name and a body are then separated is
+/// shared, so a document is read by declaring its list style rather than by
+/// describing its punctuation.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
+pub enum Shape {
+    /// `1. **C1 — Addressing.** text` — a numbered conformance list. The
+    /// default, and what this family's own specifications use.
+    #[default]
+    NumberedBold,
+    /// `- **FR-1 — Addressing.** text` — the same item in a bulleted list,
+    /// which is how requirements more often appear outside a formal spec.
+    BulletedBold,
+    /// `### REQ-7 — Addressing` followed by prose — one heading per
+    /// requirement, carrying its identifier. Common wherever requirements are
+    /// kept as documentation rather than as a list.
+    Heading,
+}
+
+impl Shape {
+    /// The shapes this producer implements, for an error message.
+    pub const KNOWN: &'static str =
+        "numbered-bold-label, bulleted-bold-label, heading-label";
+
+    /// Read a declared shape.
+    pub fn parse(name: &str) -> Result<Self, SpecDocError> {
+        match name {
+            "numbered-bold-label" => Ok(Self::NumberedBold),
+            "bulleted-bold-label" => Ok(Self::BulletedBold),
+            "heading-label" => Ok(Self::Heading),
+            other => Err(SpecDocError::UnknownShape {
+                got: other.to_string(),
+                known: Self::KNOWN.to_string(),
+            }),
+        }
+    }
+
+    /// The name this shape is declared by.
+    #[must_use]
+    pub const fn label(self) -> &'static str {
+        match self {
+            Self::NumberedBold => "numbered-bold-label",
+            Self::BulletedBold => "bulleted-bold-label",
+            Self::Heading => "heading-label",
+        }
+    }
+}
+
+/// How deep a markdown heading is, or `None` if the line is not one.
+fn heading_depth(line: &str) -> Option<usize> {
+    let t = line.trim_start();
+    if !t.starts_with('#') {
+        return None;
+    }
+    let depth = t.chars().take_while(|c| *c == '#').count();
+    // `#hashtag` is not a heading; a heading has whitespace after its hashes.
+    t[depth..].starts_with(char::is_whitespace).then_some(depth)
+}
+
 fn is_section_heading(line: &str, section: &str) -> bool {
     let t = line.trim_start();
     if !t.starts_with('#') {
@@ -87,20 +178,102 @@ fn split_item(body: &str) -> Option<(String, String, String)> {
     Some((label.trim().to_string(), name.to_string(), tail.trim().to_string()))
 }
 
-/// Parse the numbered items of one section.
+/// Split a heading's text into `label`, `name` on either an em dash or a
+/// colon, which are the two ways an identifier is conventionally separated
+/// from its title.
+fn split_heading(body: &str) -> Option<(String, String)> {
+    let (label, name) = body
+        .split_once(" — ")
+        .or_else(|| body.split_once(": "))
+        .or_else(|| body.split_once(" - "))?;
+    let label = label.trim();
+    let name = name.trim().trim_end_matches('.');
+    (!label.is_empty() && !name.is_empty())
+        .then(|| (label.to_string(), name.to_string()))
+}
+
+/// What one line is, under a given shape.
+enum Line<'a> {
+    /// This line ends the section.
+    SectionEnd,
+    /// This line opens an item.
+    Opens(String, String, String),
+    /// This line continues the open item, or closes it if blank.
+    Body(&'a str),
+}
+
+/// Classify one line. The shape decides only what *opens* an item and what
+/// *ends* the section; everything else is body.
+fn classify<'a>(line: &'a str, shape: Shape, section_depth: usize) -> Line<'a> {
+    let trimmed = line.trim_start();
+    let depth = heading_depth(line);
+
+    match shape {
+        // For list shapes any heading ends the section, which is the rule
+        // this parser has always applied.
+        Shape::NumberedBold | Shape::BulletedBold => {
+            if depth.is_some() {
+                return Line::SectionEnd;
+            }
+            let body = match shape {
+                Shape::NumberedBold => trimmed
+                    .split_once(". ")
+                    .filter(|(n, _)| !n.is_empty() && n.chars().all(|c| c.is_ascii_digit()))
+                    .map(|(_, b)| b),
+                // A bullet marker, not a line that merely begins with a dash:
+                // `- ` and `* ` both open a list item in markdown.
+                _ => trimmed
+                    .strip_prefix("- ")
+                    .or_else(|| trimmed.strip_prefix("* ")),
+            };
+            match body.and_then(split_item) {
+                Some((label, name, text)) => Line::Opens(label, name, text),
+                // A list item that does not carry a label is body: it may be
+                // a sub-list under the open item.
+                None => Line::Body(line),
+            }
+        }
+        // Here the items *are* headings, so the section ends only at a
+        // heading no deeper than the section's own.
+        Shape::Heading => match depth {
+            Some(d) if d <= section_depth => Line::SectionEnd,
+            Some(_) => {
+                let body = trimmed.trim_start_matches('#').trim();
+                match split_heading(body) {
+                    Some((label, name)) => Line::Opens(label, name, String::new()),
+                    // A heading with no identifier is a grouping heading, not
+                    // a requirement. Treating it as one would invent an
+                    // obligation nobody wrote.
+                    None => Line::Body(line),
+                }
+            }
+            None => Line::Body(line),
+        },
+    }
+}
+
+/// Parse the items of one section, in the document's declared shape.
 ///
 /// `expect_at_least` is a floor the caller states: a parser that silently
 /// matched nothing would report success having checked nothing, which is the
 /// failure mode this whole standard exists to make visible.
+///
+/// There is deliberately no shape-free convenience wrapper. A caller that
+/// did not have to name a shape would read some documents correctly and
+/// others silently wrongly, and the obligation addresses are computed from
+/// whatever it captured.
 pub fn items(
     document: &str,
     section: &str,
     expect_at_least: usize,
+    shape: Shape,
 ) -> Result<Vec<Item>, SpecDocError> {
     let mut lines = document.lines();
+    let mut section_depth = 0usize;
     let mut found_section = false;
     for line in lines.by_ref() {
         if is_section_heading(line, section) {
+            section_depth = heading_depth(line).unwrap_or(0);
             found_section = true;
             break;
         }
@@ -112,46 +285,49 @@ pub fn items(
     let mut out: Vec<Item> = Vec::new();
     let mut pending: Option<Item> = None;
     for line in lines {
-        // The next heading of any level ends the section.
-        if line.trim_start().starts_with('#') {
-            break;
-        }
-        let trimmed = line.trim_start();
-        let numbered = trimmed
-            .split_once(". ")
-            .filter(|(n, _)| !n.is_empty() && n.chars().all(|c| c.is_ascii_digit()));
-
-        match numbered {
-            Some((_, body)) => {
+        match classify(line, shape, section_depth) {
+            Line::SectionEnd => break,
+            Line::Opens(label, name, text) => {
                 if let Some(item) = pending.take() {
                     out.push(item);
                 }
-                if let Some((label, name, text)) = split_item(body) {
-                    pending = Some(Item { label, name, text });
-                }
+                pending = Some(Item { label, name, text });
             }
-            None if pending.is_some() => {
-                let continuation = line.trim();
+            Line::Body(raw) => {
+                if pending.is_none() {
+                    continue;
+                }
+                let continuation = raw.trim();
                 if continuation.is_empty() {
-                    if let Some(item) = pending.take() {
+                    // A blank line closes a list item. Under `heading-label`
+                    // a requirement's prose runs over paragraphs, so it does
+                    // not: the next heading closes it instead.
+                    if shape != Shape::Heading && let Some(item) = pending.take() {
                         out.push(item);
                     }
                 } else if let Some(item) = pending.as_mut() {
                     // Re-wrapping must not change the obligation, so
                     // continuation lines join with exactly one space.
-                    item.text.push(' ');
+                    if !item.text.is_empty() {
+                        item.text.push(' ');
+                    }
                     item.text.push_str(continuation);
                 }
             }
-            None => {}
         }
     }
     if let Some(item) = pending {
         out.push(item);
     }
+    // A heading with no prose under it states no requirement; keeping it
+    // would address the empty string and grade an obligation nobody wrote.
+    out.retain(|i| !i.text.is_empty());
 
     if out.is_empty() {
-        return Err(SpecDocError::NoItems(section.to_string()));
+        return Err(SpecDocError::NoItems {
+            section: section.to_string(),
+            shape: shape.label(),
+        });
     }
     if out.len() < expect_at_least {
         return Err(SpecDocError::TooFew {
@@ -189,7 +365,7 @@ pub fn clauses(items: &[Item]) -> Vec<Clause> {
 mod tests {
     use super::*;
 
-    const DOC: &str = "\
+    pub(super) const DOC: &str = "\
 # A Standard
 
 ## 6. Something else
@@ -215,7 +391,7 @@ The reference implementation is conformant by construction.
 
     #[test]
     fn items_are_read_from_the_named_section_only() {
-        let got = items(DOC, "7. Conformance", 3).expect("parses");
+        let got = items(DOC, "7. Conformance", 3, Shape::default()).expect("parses");
         assert_eq!(got.len(), 3, "{got:#?}");
         assert_eq!(got[0].label, "C1");
         assert_eq!(got[0].name, "Addressing");
@@ -224,7 +400,7 @@ The reference implementation is conformant by construction.
 
     #[test]
     fn continuation_lines_join_with_one_space() {
-        let got = items(DOC, "7. Conformance", 3).unwrap();
+        let got = items(DOC, "7. Conformance", 3, Shape::default()).unwrap();
         assert_eq!(
             got[0].text,
             "Obligation addresses are computed over `{kind, text}` with the label excluded; \
@@ -241,9 +417,9 @@ The reference implementation is conformant by construction.
         );
         let reworded = DOC.replace("relabelling preserves an address", "relabelling may preserve an address");
 
-        let base = clauses(&items(DOC, "7. Conformance", 3).unwrap());
-        let wrapped = clauses(&items(&rewrapped, "7. Conformance", 3).unwrap());
-        let changed = clauses(&items(&reworded, "7. Conformance", 3).unwrap());
+        let base = clauses(&items(DOC, "7. Conformance", 3, Shape::default()).unwrap());
+        let wrapped = clauses(&items(&rewrapped, "7. Conformance", 3, Shape::default()).unwrap());
+        let changed = clauses(&items(&reworded, "7. Conformance", 3, Shape::default()).unwrap());
 
         assert_eq!(
             base[0].obligation().unwrap(),
@@ -259,13 +435,13 @@ The reference implementation is conformant by construction.
 
     #[test]
     fn a_missing_section_is_an_error_not_an_empty_list() {
-        assert!(matches!(items(DOC, "99. Nowhere", 1), Err(SpecDocError::NoSection(_))));
+        assert!(matches!(items(DOC, "99. Nowhere", 1, Shape::default()), Err(SpecDocError::NoSection(_))));
     }
 
     #[test]
     fn a_section_with_no_items_is_an_error() {
         let doc = "## 7. Conformance\n\nProse only, no list.\n";
-        assert!(matches!(items(doc, "7. Conformance", 1), Err(SpecDocError::NoItems(_))));
+        assert!(matches!(items(doc, "7. Conformance", 1, Shape::default()), Err(SpecDocError::NoItems { .. })));
     }
 
     #[test]
@@ -273,19 +449,185 @@ The reference implementation is conformant by construction.
         // The guard that matters: a parser that quietly matched two of eleven
         // items would report every unmatched obligation as unevidenced, or --
         // worse, with a narrower specification, as fully covered.
-        let err = items(DOC, "7. Conformance", 11).unwrap_err();
+        let err = items(DOC, "7. Conformance", 11, Shape::default()).unwrap_err();
         assert!(matches!(err, SpecDocError::TooFew { found: 3, expected: 11, .. }), "{err}");
     }
 
     #[test]
     fn an_unlabelled_numbered_line_is_not_an_item() {
         let doc = "## 7. Conformance\n\n1. **Bolded but unlabelled.** No em dash.\n";
-        assert!(matches!(items(doc, "7. Conformance", 1), Err(SpecDocError::NoItems(_))));
+        assert!(matches!(items(doc, "7. Conformance", 1, Shape::default()), Err(SpecDocError::NoItems { .. })));
     }
 
     #[test]
     fn a_duplicate_label_is_refused() {
         let doc = "## 7. C\n\n1. **C1 — A.** One.\n2. **C1 — B.** Two.\n";
-        assert!(matches!(items(doc, "7. C", 2), Err(SpecDocError::DuplicateLabel(l)) if l == "C1"));
+        assert!(matches!(items(doc, "7. C", 2, Shape::default()), Err(SpecDocError::DuplicateLabel(l)) if l == "C1"));
+    }
+}
+
+#[cfg(test)]
+mod shaped {
+    use super::*;
+
+    /// The shape an existing manifest gets when it declares none. If this
+    /// ever changes, every obligation address in every deployment moves.
+    #[test]
+    fn the_default_shape_is_the_numbered_list() {
+        assert_eq!(Shape::default(), Shape::NumberedBold);
+        assert_eq!(Shape::default().label(), "numbered-bold-label");
+        assert_eq!(Shape::parse("numbered-bold-label").unwrap(), Shape::default());
+    }
+
+    /// The load-bearing regression: generalising the parser must not change
+    /// what the default shape extracts, because the obligation address is
+    /// computed from exactly that text. The hex below is the address of a
+    /// fixture clause, so a change of a single character in how the default
+    /// shape captures text fails here rather than silently invalidating the
+    /// evidence of every deployment that upgrades.
+    #[test]
+    fn generalising_the_parser_moved_no_obligation_under_the_default_shape() {
+        use joulespec_core::spec::{Clause, ClauseKind};
+        let got = items(super::tests::DOC, "7. Conformance", 3, Shape::default()).unwrap();
+        let clause = Clause::new(
+            got[0].label.clone(),
+            ClauseKind::Requirement,
+            format!("{} — {}", got[0].name, got[0].text),
+        );
+        assert_eq!(
+            clause.obligation().unwrap().as_str(),
+            // Computed by running this same fixture through the parser as it
+            // stood before the shape generalisation, not by recording what
+            // the new one happens to produce.
+            "b3:71447ade934b77d80fb3816d198c675821b2a99e88b60174190ad35064121060",
+            "the default shape's extraction changed; every deployment's \
+             obligation addresses would move"
+        );
+    }
+
+    const BULLETED: &str = "\
+## Requirements
+
+- **FR-1 — Addressing.** Obligation addresses are computed over `{kind, text}`
+  with the label excluded.
+- a sub-point that carries no label, which is body rather than an item
+* **FR-2 — Validation.** Duplicate labels are refused.
+
+## Next
+";
+
+    #[test]
+    fn a_bulleted_requirement_list_is_read_with_both_markers() {
+        let got =
+            items(BULLETED, "Requirements", 2, Shape::BulletedBold).unwrap();
+        assert_eq!(got.len(), 2, "{got:#?}");
+        assert_eq!(got[0].label, "FR-1");
+        assert_eq!(got[1].label, "FR-2", "an asterisk opens a list item too");
+        assert!(
+            got[0].text.ends_with("body rather than an item"),
+            "an unlabelled bullet is body, not an item: {:?}",
+            got[0].text
+        );
+    }
+
+    const HEADINGS: &str = "\
+# A Requirements Document
+
+## 2. Requirements
+
+Some preamble that belongs to no requirement.
+
+### REQ-1: Addressing
+
+Obligation addresses are computed over the kind and text,
+with the label excluded.
+
+A second paragraph of the same requirement.
+
+### Grouping heading with no identifier
+
+### REQ-2 — Validation
+
+Duplicate labels are refused.
+
+### REQ-3: Nothing is stated here
+
+## 3. Afterwards
+
+### REQ-9: A decoy past the section end
+
+Not a requirement of section 2.
+";
+
+    #[test]
+    fn a_heading_per_requirement_is_read_with_either_separator() {
+        let got = items(HEADINGS, "2. Requirements", 2, Shape::Heading).unwrap();
+        assert_eq!(
+            got.iter().map(|i| i.label.as_str()).collect::<Vec<_>>(),
+            ["REQ-1", "REQ-2"],
+            "{got:#?}"
+        );
+        assert_eq!(got[0].name, "Addressing", "a colon separates too");
+        assert_eq!(got[1].name, "Validation", "and so does an em dash");
+    }
+
+    /// Prose under one of these headings runs over paragraphs, so a blank
+    /// line must not close the item the way it does in a list.
+    #[test]
+    fn a_requirement_heading_holds_its_whole_prose() {
+        let got = items(HEADINGS, "2. Requirements", 2, Shape::Heading).unwrap();
+        assert!(
+            got[0].text.contains("second paragraph"),
+            "a blank line closed the item early: {:?}",
+            got[0].text
+        );
+        assert!(!got[0].text.contains("preamble"), "preamble belongs to nothing");
+    }
+
+    /// A heading that states nothing is not a requirement with empty text —
+    /// addressing the empty string would create an obligation nobody wrote,
+    /// and it would be graded like any other.
+    #[test]
+    fn a_heading_with_no_prose_states_no_requirement() {
+        let got = items(HEADINGS, "2. Requirements", 2, Shape::Heading).unwrap();
+        assert!(
+            !got.iter().any(|i| i.label == "REQ-3"),
+            "an empty heading became an obligation: {got:#?}"
+        );
+        assert!(
+            !got.iter().any(|i| i.label == "REQ-9"),
+            "the section end was not respected: {got:#?}"
+        );
+    }
+
+    /// A heading no deeper than the section's own ends it. Under the list
+    /// shapes any heading does, which is the older and stricter rule.
+    #[test]
+    fn a_shape_that_matches_nothing_fails_closed() {
+        // The heading document read as a numbered list finds no items at all.
+        assert!(matches!(
+            items(HEADINGS, "2. Requirements", 1, Shape::NumberedBold),
+            Err(SpecDocError::NoItems { .. })
+        ));
+        // And the floor still bites when the shape matches too little.
+        assert!(matches!(
+            items(HEADINGS, "2. Requirements", 3, Shape::Heading),
+            Err(SpecDocError::TooFew { found: 2, .. })
+        ));
+    }
+
+    #[test]
+    fn an_unimplemented_shape_is_refused_by_name() {
+        assert!(matches!(
+            Shape::parse("whatever-the-operator-hoped"),
+            Err(SpecDocError::UnknownShape { .. })
+        ));
+    }
+
+    #[test]
+    fn a_hashtag_is_not_a_heading() {
+        assert_eq!(heading_depth("### REQ-1: x"), Some(3));
+        assert_eq!(heading_depth("#notaheading"), None);
+        assert_eq!(heading_depth("plain text"), None);
     }
 }
diff --git a/joulespec/joulespec-rs/crates/joulespec-core/Cargo.toml b/joulespec/joulespec-rs/crates/joulespec-core/Cargo.toml
index 672b6984f..9491d3f3f 100644
--- a/joulespec/joulespec-rs/crates/joulespec-core/Cargo.toml
+++ b/joulespec/joulespec-rs/crates/joulespec-core/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "joulespec-core"
-version = "0.2.0"
+version = "0.3.0"
 description = "JouleSpec — the reference conformance kernel for energy-accounted specifications (joulespec/1): obligation-addressed clauses, a graded evidence ladder from testimony to proof, deterministic drift, and the joules a specification cost to evidence."
 edition.workspace = true
 license.workspace = true
@@ -15,3 +15,7 @@ thiserror = { workspace = true }
 
 [lints.rust]
 missing_docs = "warn"
+# The proof harnesses in src/proofs.rs compile only under the model checker,
+# which sets this cfg itself. Declaring it here keeps `cargo check` from
+# warning about a cfg it has no way to know about.
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)', 'cfg(joulespec_slow_proofs)'] }
diff --git a/joulespec/joulespec-rs/crates/joulespec-core/src/conform.rs b/joulespec/joulespec-rs/crates/joulespec-core/src/conform.rs
index 2dd88b2c2..d82b9894c 100644
--- a/joulespec/joulespec-rs/crates/joulespec-core/src/conform.rs
+++ b/joulespec/joulespec-rs/crates/joulespec-core/src/conform.rs
@@ -298,12 +298,7 @@ impl Conformance {
     /// features nobody requested.
     #[must_use]
     pub fn specified_ppm(&self) -> Option<u64> {
-        let total = self.specified_uj.checked_add(self.unspecified_uj)?;
-        if total == 0 {
-            return None;
-        }
-        // u128 so a specified figure near u64::MAX cannot overflow the scale.
-        Some(((u128::from(self.specified_uj) * 1_000_000) / u128::from(total)) as u64)
+        ppm(self.specified_uj, self.unspecified_uj)
     }
 
     /// Total energy attributed to this specification: the work plus the
@@ -356,6 +351,42 @@ impl Conformance {
     }
 }
 
+/// The §3.2 cap: the minimum over a set of graded figures, absent when any
+/// member has no figure at all.
+///
+/// `None` orders below every `Some`, and that is the whole mechanism: an
+/// obligation with no surviving evidence caps the composite rather than being
+/// skipped over, so nine proved obligations cannot conceal one nobody looked
+/// at. An empty set has nothing to cap and is absent.
+///
+/// Generic because §3.2 applies the identical rule twice — once to grades and
+/// once to attestations — and two copies of a rule are two places for it to
+/// drift. Stated as a named function so a prover can be asked about every
+/// combination of members, including the ones where absence meets the top
+/// rung.
+#[must_use]
+pub fn cap<T: Ord, I: IntoIterator<Item = Option<T>>>(graded: I) -> Option<T> {
+    graded.into_iter().min().unwrap_or(None)
+}
+
+/// The §5 ratio rule: an integer parts-per-million share of a whole, absent
+/// when there is no whole to take a share of.
+///
+/// Stated as a free function over two plain integers so it can be handed to a
+/// prover across its entire input domain rather than sampled at a handful of
+/// points. The `u128` widening is load-bearing and not decoration: a `part`
+/// anywhere near `u64::MAX` overflows the parts-per-million scale in 64 bits,
+/// and the inputs that expose it are far outside the range any hand-written
+/// case would think to pick.
+#[must_use]
+pub fn ppm(part: u64, rest: u64) -> Option<u64> {
+    let total = part.checked_add(rest)?;
+    if total == 0 {
+        return None;
+    }
+    Some(((u128::from(part) * 1_000_000) / u128::from(total)) as u64)
+}
+
 /// Evaluate a specification at one artifact state.
 ///
 /// Every witness is verified here; none is taken on trust and none is
@@ -506,12 +537,7 @@ pub fn evaluate(
     }
     flags.sort();
 
-    let grade = verdicts
-        .iter()
-        .filter(|c| c.kind.is_owed())
-        .map(|c| c.grade)
-        .min()
-        .unwrap_or(None);
+    let grade = cap(verdicts.iter().filter(|c| c.kind.is_owed()).map(|c| c.grade));
 
     let mut specified_uj = 0u64;
     let mut unspecified_uj = 0u64;
@@ -534,12 +560,7 @@ pub fn evaluate(
     let provenance =
         worst_provenance(evidence_provenances.into_iter().chain(work_provenances));
 
-    let attestation = verdicts
-        .iter()
-        .filter(|c| c.kind.is_owed())
-        .map(|c| c.attestation)
-        .min()
-        .unwrap_or(None);
+    let attestation = cap(verdicts.iter().filter(|c| c.kind.is_owed()).map(|c| c.attestation));
 
     Ok(Conformance {
         spec_id,
diff --git a/joulespec/joulespec-rs/crates/joulespec-core/src/lib.rs b/joulespec/joulespec-rs/crates/joulespec-core/src/lib.rs
index ae8df80f7..8e4739b03 100644
--- a/joulespec/joulespec-rs/crates/joulespec-core/src/lib.rs
+++ b/joulespec/joulespec-rs/crates/joulespec-core/src/lib.rs
@@ -77,6 +77,9 @@ pub mod conform;
 pub mod drift;
 pub mod evidence;
 pub mod jcr1;
+
+#[cfg(kani)]
+mod proofs;
 pub mod receipt;
 pub mod spec;
 
diff --git a/joulespec/joulespec-rs/crates/joulespec-core/src/proofs.rs b/joulespec/joulespec-rs/crates/joulespec-core/src/proofs.rs
new file mode 100644
index 000000000..69f015aea
--- /dev/null
+++ b/joulespec/joulespec-rs/crates/joulespec-core/src/proofs.rs
@@ -0,0 +1,190 @@
+//! Machine-checked statements about this implementation, for the `E4` rung.
+//!
+//! These are not tests. A test samples the input domain; a proof here is
+//! discharged over the whole of it, which is the only thing `E4` claims over
+//! `E3`. They compile only under the model checker (`cfg(kani)`), so an
+//! ordinary `cargo test` neither runs nor type-checks them — see
+//! `conformance/v1/README.md` for how the harvest reaches them.
+//!
+//! Every harness carries at least one reachability cover. A model checker
+//! reports success for a harness whose assumptions have eliminated the states
+//! the property was about, so success alone is not evidence that anything was
+//! checked: it is the same shape of silence as a test binary that runs zero
+//! tests and exits zero. The covers are what distinguish the two, and the
+//! producer refuses a harness that declares none.
+
+use crate::conform::{cap, ppm};
+use crate::evidence::Grade;
+
+/// **C7 — Cost.** The ratio rule is arithmetically total: for no pair of
+/// inputs does it overflow or divide by zero.
+///
+/// This is what the `u128` widening in [`ppm`] exists for, and it is the half
+/// of C7 that sampling cannot reach. The inputs that break it are a `part`
+/// above roughly `u64::MAX / 1_000_000`, which no hand-written case picks and
+/// no realistic fixture contains — so a suite can pass indefinitely over an
+/// implementation that computes the scale in 64 bits and overflows.
+///
+/// The statement is discharged by the checker's own arithmetic checks rather
+/// than by an assertion written here. That is the precise claim: not that the
+/// quotient has some value, but that every operation on the way to it is
+/// defined for every input. The covers below are what make the claim mean
+/// something, by showing each branch is reached.
+///
+/// The companion statement — that the quotient is bounded by the scale — is
+/// deliberately *not* made here. It requires the solver to reason about the
+/// output bits of a 128-bit division, and it did not converge; see
+/// `conformance/v1/README.md`. Leaving it unstated is the honest shape, since
+/// a harness that quietly narrowed its domain to converge would report the
+/// same success over a smaller claim.
+#[kani::proof]
+fn the_ratio_rule_is_total_over_every_input() {
+    let part: u64 = kani::any();
+    let rest: u64 = kani::any();
+
+    let share = ppm(part, rest);
+
+    // Each cover names a branch the statement is about. Without them, a
+    // harness whose assumptions had emptied the domain would report the same
+    // success as this one.
+    kani::cover!(share.is_none(), "no whole to take a share of");
+    kani::cover!(share.is_some(), "a whole exists and a share was computed");
+    kani::cover!(
+        part.checked_add(rest).is_none(),
+        "the whole itself overflows, which is the absent case"
+    );
+    kani::cover!(
+        part > u64::MAX / 1_000_000 && share.is_some(),
+        "a part large enough to overflow the scale in 64 bits"
+    );
+}
+
+/// **C7 — Cost.** The quotient itself is bounded by the scale, is the full
+/// scale exactly when nothing is left over, and is none of it when there is no
+/// part.
+///
+/// **This harness does not converge, and is kept as the record of that.** It
+/// is behind a `cfg` nobody sets, so an ordinary run of this package does not
+/// hang on it; reproduce with
+/// `RUSTFLAGS='--cfg joulespec_slow_proofs' cargo kani -p joulespec-core
+/// --harness a_share_never_exceeds_the_scale_it_is_measured_on`.
+///
+/// Measured twice, on one host, over the same input domain:
+///
+/// | Method | Outcome |
+/// |---|---|
+/// | bit-blasting to SAT (the default engine) | no per-property progress in 24 minutes |
+/// | an SMT bitvector theory | 4 of ~51 conditions in about 8 seconds, then over 50 minutes on the 5th |
+///
+/// The second is the interesting one. Naming a solver that reasons about the
+/// operation rather than its output bits moved the wall — it settles most of
+/// the conditions almost at once — but it did not remove it: one condition
+/// about a wide division's quotient remains out of reach. So the cost of a
+/// statement is not simply a property of the engine, and an operator cannot
+/// expect to buy convergence by changing solver. [`the_ratio_rule_is_total_over_every_input`]
+/// states the part of C7 that *is* reachable, which is also the part a
+/// counter-artifact refutes.
+#[cfg(joulespec_slow_proofs)]
+#[kani::proof]
+#[kani::solver(z3)]
+fn a_share_never_exceeds_the_scale_it_is_measured_on() {
+    let part: u64 = kani::any();
+    let rest: u64 = kani::any();
+
+    if let Some(share) = ppm(part, rest) {
+        assert!(share <= 1_000_000, "a share cannot exceed the whole scale");
+        assert!(
+            rest > 0 || share == 1_000_000,
+            "with nothing left over the share is the whole scale"
+        );
+        assert!(
+            part > 0 || share == 0,
+            "with no part the share is none of the scale"
+        );
+    }
+
+    kani::cover!(ppm(part, rest) == Some(1_000_000), "the whole-scale case");
+    kani::cover!(ppm(part, rest) == Some(0), "the none-of-it case");
+    kani::cover!(
+        matches!(ppm(part, rest), Some(s) if s > 0 && s < 1_000_000),
+        "an interior share"
+    );
+}
+
+/// A symbolic grade, over the whole of the ladder.
+fn any_grade() -> Grade {
+    match kani::any::<u8>() % 5 {
+        0 => Grade::Cited,
+        1 => Grade::Reviewed,
+        2 => Grade::Exercised,
+        3 => Grade::Falsifiable,
+        _ => Grade::Proved,
+    }
+}
+
+/// **C5 — Evaluation.** The cap is a minimum, and widening a set can only
+/// lower it.
+///
+/// §3.2 states this as the reason a grade is not gameable by adding clauses,
+/// and it is the one property an adversary has a direct incentive to break.
+/// A test samples it; this settles it over every combination of grades a set
+/// of this size can hold, including the ones where an absent grade meets a
+/// proved one.
+///
+/// The statement is about [`cap`] itself — the function the evaluator calls —
+/// and not about a restatement of the rule inside the harness. A proof of a
+/// property of its own local copy of the logic would establish nothing about
+/// the artifact, and no counter-artifact to the artifact could refute it.
+///
+/// The bound on set size is part of the statement rather than a concession
+/// hidden in the harness: the minimum is determined by one member and the
+/// ordering of the rest, so a set of four exhibits every arrangement the rule
+/// can meet.
+#[kani::proof]
+fn widening_a_set_can_only_lower_its_cap() {
+    let held: [Option<Grade>; 4] = [
+        if kani::any() { Some(any_grade()) } else { None },
+        if kani::any() { Some(any_grade()) } else { None },
+        if kani::any() { Some(any_grade()) } else { None },
+        if kani::any() { Some(any_grade()) } else { None },
+    ];
+    let extra: Option<Grade> = if kani::any() { Some(any_grade()) } else { None };
+
+    let before = cap(held);
+    let widened = [held[0], held[1], held[2], held[3], extra];
+    let after = cap(widened);
+
+    match (before, after) {
+        (Some(b), Some(a)) => {
+            assert!(a <= b, "widening a set cannot raise its cap");
+            assert!(
+                held.contains(&Some(b)),
+                "a cap is one of the figures that fed it, not a value of its own"
+            );
+        }
+        (None, a) => assert!(
+            a.is_none(),
+            "a set with an unevidenced member cannot become evidenced by growing"
+        ),
+        // Widening with an unevidenced member empties the cap. That is the
+        // rule working, and it is the direction §3.2 relies on.
+        (Some(_), None) => assert!(
+            extra.is_none(),
+            "the cap can only empty because the added member was unevidenced"
+        ),
+    }
+
+    kani::cover!(
+        matches!((before, after), (Some(b), Some(a)) if a < b),
+        "the added member strictly lowers the cap"
+    );
+    kani::cover!(
+        matches!((before, after), (Some(b), Some(a)) if a == b),
+        "the added member leaves the cap alone"
+    );
+    kani::cover!(
+        matches!((before, after), (Some(_), None)),
+        "the added member is unevidenced and empties the cap"
+    );
+    kani::cover!(before.is_none(), "the set was already unevidenced");
+}
diff --git a/joulespec/joulespec-rs/crates/joulespec-core/tests/evaluation.rs b/joulespec/joulespec-rs/crates/joulespec-core/tests/evaluation.rs
new file mode 100644
index 000000000..6d26db08a
--- /dev/null
+++ b/joulespec/joulespec-rs/crates/joulespec-core/tests/evaluation.rs
@@ -0,0 +1,736 @@
+//! The published **evaluation** corpus: cases an over-grading implementation
+//! passes incorrectly.
+//!
+//! The wire vectors in `tests/vectors.rs` certify that an implementation
+//! round-trips a receipt's bytes. They say nothing about whether it reaches
+//! the right verdict, because they carry one scenario. This corpus is the
+//! other half: each case is a complete set of evaluation inputs plus the
+//! verdict §3 requires, chosen so that a plausible but wrong evaluator
+//! disagrees.
+//!
+//! Every case names the **trap** it sets and the **direction** of the error
+//! it catches. Most are over-grading: an implementation that reports
+//! conformance never established, which is the failure this standard exists
+//! to stop. At least one is under-grading, because a rule that refuses
+//! everything is also wrong and an implementation can satisfy every
+//! over-grading case by grading nothing at all.
+//!
+//! ## Where the expected verdicts come from
+//!
+//! They are written by hand from §3 of the specification, and they are
+//! **not** regenerated from this implementation's output — a corpus whose
+//! expectations are whatever the code produced would certify agreement with
+//! itself. Setting `JOULESPEC_GEN_EVALUATION=1` republishes the input files
+//! and the expectations as this test states them; it never reads a verdict
+//! back out of the evaluator to decide what to expect.
+//!
+//! ## How another implementation uses it
+//!
+//! Each case directory holds `spec.json`, `state.json`, `witnesses.json`,
+//! `work.json` and `expect.json`. Read the first four, evaluate, and compare
+//! against the fifth.
+
+use std::path::{Path, PathBuf};
+
+use ed25519_dalek::SigningKey;
+use joulespec_core::conform::{self, ArtifactState, Conformance, Work};
+use joulespec_core::evidence::{
+    Anchor, Attestation, Evidence, Formalization, Grade, Grounding, SignedWitness, Vacuity,
+    Witness,
+};
+use joulespec_core::spec::{Clause, SignedSpec, Spec};
+use joulespec_core::{Address, Energy, Provenance};
+use serde::{Deserialize, Serialize};
+
+fn key(seed: u8) -> SigningKey {
+    SigningKey::from_bytes(&[seed; 32])
+}
+
+fn dir() -> PathBuf {
+    Path::new(env!("CARGO_MANIFEST_DIR")).join("../../../conformance/v1/evaluation")
+}
+
+/// What a conforming evaluator must report for one case.
+///
+/// Deliberately small: the fields an over-generous implementation gets wrong.
+/// Energy is omitted because these cases are about grading, and a corpus that
+/// pinned microjoules would stop being reproducible for the reasons the
+/// self-conformance record is not.
+#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
+struct Expect {
+    /// What the case is for, in one line.
+    intent: String,
+    /// What a wrong implementation does here instead.
+    trap: String,
+    /// `over-grading` or `under-grading`: which way the wrong answer errs.
+    direction: String,
+    /// The specification's grade, absent where §3.2 requires absence.
+    grade: Option<Grade>,
+    /// The specification's attestation, on the second axis.
+    attestation: Option<Attestation>,
+    /// Flag kinds raised, by variant name, sorted.
+    flags: Vec<String>,
+    /// Per clause, in specification order.
+    clauses: Vec<ExpectClause>,
+    /// Whether the case conforms at `E3` and `A0`.
+    conformant_at_e3: bool,
+}
+
+#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
+struct ExpectClause {
+    label: String,
+    grade: Option<Grade>,
+    /// How many of its witnesses were set aside as bound to another state.
+    stale: usize,
+}
+
+fn flag_kind(f: &conform::Flag) -> String {
+    match f {
+        conform::Flag::NonGoalWitnessed { .. } => "NonGoalWitnessed",
+        conform::Flag::Unbound { .. } => "Unbound",
+        conform::Flag::ForeignSpec { .. } => "ForeignSpec",
+        conform::Flag::Unverifiable { .. } => "Unverifiable",
+    }
+    .to_string()
+}
+
+fn observed(c: &Conformance, like: &Expect) -> Expect {
+    let mut flags: Vec<String> = c.flags.iter().map(flag_kind).collect();
+    flags.sort();
+    Expect {
+        intent: like.intent.clone(),
+        trap: like.trap.clone(),
+        direction: like.direction.clone(),
+        grade: c.grade,
+        attestation: c.attestation,
+        flags,
+        clauses: c
+            .clauses
+            .iter()
+            .map(|v| ExpectClause {
+                label: v.label.clone(),
+                grade: v.grade,
+                stale: v.stale.len(),
+            })
+            .collect(),
+        conformant_at_e3: c.is_conformant(Grade::Falsifiable, Attestation::SelfAttested),
+    }
+}
+
+// ── case construction ────────────────────────────────────────────────────
+
+fn state() -> ArtifactState {
+    ArtifactState::new(
+        Address::of_bytes(b"eval-tree-v1"),
+        [
+            Address::of_bytes(b"eval-part-a"),
+            Address::of_bytes(b"eval-part-b"),
+        ],
+    )
+}
+
+fn spec_of(clauses: Vec<Clause>) -> SignedSpec {
+    let author = key(1);
+    Spec::new(
+        "A corpus case: the clauses exist to be graded, not to be implemented.",
+        clauses,
+        author.verifying_key().to_bytes(),
+    )
+    .sign(&author)
+    .expect("signs")
+}
+
+fn obligation(spec: &SignedSpec, label: &str) -> joulespec_core::spec::Obligation {
+    spec.spec
+        .clauses
+        .iter()
+        .find(|c| c.label == label)
+        .expect("label is in the specification")
+        .obligation()
+        .expect("addresses")
+}
+
+/// A witness carrying `evidence` for `label`, at `at` (the current state
+/// unless a case is about staleness), signed by `signer`.
+fn witness(
+    spec: &SignedSpec,
+    label: &str,
+    evidence: Evidence,
+    signer: &SigningKey,
+    at: Address,
+) -> SignedWitness {
+    Witness::new(
+        spec.spec.spec_id().unwrap(),
+        obligation(spec, label),
+        at,
+        evidence,
+        Energy::new(1_000, Provenance::Estimator),
+        signer.verifying_key().to_bytes(),
+    )
+    .sign(signer)
+    .expect("signs")
+}
+
+/// One unit of work by `author`, citing `label`.
+///
+/// Every case declares work, because the attestation axis is computed from
+/// **work** authorship: with no implementer known, §2.8 makes attestation
+/// absent, and a corpus of cases that all declared none would exercise one
+/// axis and certify two.
+fn work_by(spec: &SignedSpec, label: &str, author: &SigningKey) -> Vec<Work> {
+    vec![Work::new(
+        Address::of_bytes(b"eval-work"),
+        vec![obligation(spec, label)],
+        Energy::new(500_000, Provenance::Estimator),
+        author.verifying_key().to_bytes(),
+    )]
+}
+
+fn falsifiable(anchor: Anchor) -> Evidence {
+    Evidence::Falsifiable {
+        check: "a_named_check".into(),
+        anchor,
+        counter: Address::of_bytes(b"eval-counter"),
+    }
+}
+
+fn proved(grounding: Grounding, vacuity: Vacuity) -> Evidence {
+    Evidence::Proved {
+        goal: Address::of_bytes(b"eval-goal"),
+        tier: "corpus".into(),
+        formalization: Formalization { statement: "forall x. p(x)".into(), grounding },
+        vacuity,
+    }
+}
+
+struct Case {
+    name: &'static str,
+    spec: SignedSpec,
+    state: ArtifactState,
+    witnesses: Vec<SignedWitness>,
+    work: Vec<Work>,
+    expect: Expect,
+}
+
+#[allow(clippy::too_many_lines)]
+fn cases() -> Vec<Case> {
+    let auditor = key(2);
+    let implementer = key(4);
+    let crosschecker = key(3);
+    let mut out = Vec::new();
+
+    // 1 ── The minimum, not the mean.
+    {
+        let spec = spec_of(vec![
+            Clause::requirement("C1", "The first obligation is well evidenced."),
+            Clause::requirement("C2", "The second obligation is only claimed."),
+        ]);
+        let ws = vec![
+            witness(&spec, "C1", falsifiable(Anchor::Specification), &auditor, state().address),
+            witness(&spec, "C2", Evidence::Cited, &implementer, state().address),
+        ];
+        out.push(Case {
+            name: "01-a-mean-conceals-the-weakest-obligation",
+            expect: Expect {
+                intent: "One obligation at E3, one at E0.".into(),
+                trap: "Averaging the rungs, or reporting the best, gives E3 or E1 \
+                       where §3.2 requires the minimum."
+                    .into(),
+                direction: "over-grading".into(),
+                grade: Some(Grade::Cited),
+                attestation: Some(Attestation::SelfAttested),
+                flags: vec![],
+                clauses: vec![
+                    ExpectClause { label: "C1".into(), grade: Some(Grade::Falsifiable), stale: 0 },
+                    ExpectClause { label: "C2".into(), grade: Some(Grade::Cited), stale: 0 },
+                ],
+                conformant_at_e3: false,
+            },
+            work: work_by(&spec, "C1", &implementer),
+            spec,
+            state: state(),
+            witnesses: ws,
+        });
+    }
+
+    // 2 ── An obligation nobody looked at empties the grade.
+    {
+        let spec = spec_of(vec![
+            Clause::requirement("C1", "The first obligation is well evidenced."),
+            Clause::requirement("C2", "The second obligation has no evidence at all."),
+        ]);
+        let ws = vec![witness(
+            &spec,
+            "C1",
+            falsifiable(Anchor::Specification),
+            &auditor,
+            state().address,
+        )];
+        out.push(Case {
+            name: "02-an-unevidenced-obligation-empties-the-grade",
+            expect: Expect {
+                intent: "One obligation at E3; the other has no witness.".into(),
+                trap: "Skipping the unevidenced clause and grading the rest gives E3. \
+                       Absence orders below every rung, so the grade is absent — not E0, \
+                       which would claim a citation nobody made."
+                    .into(),
+                direction: "over-grading".into(),
+                grade: None,
+                attestation: None,
+                flags: vec![],
+                clauses: vec![
+                    ExpectClause { label: "C1".into(), grade: Some(Grade::Falsifiable), stale: 0 },
+                    ExpectClause { label: "C2".into(), grade: None, stale: 0 },
+                ],
+                conformant_at_e3: false,
+            },
+            work: work_by(&spec, "C1", &implementer),
+            spec,
+            state: state(),
+            witnesses: ws,
+        });
+    }
+
+    // 3 ── A non-goal is not owed, and does not cap.
+    {
+        let spec = spec_of(vec![
+            Clause::requirement("C1", "The obligation is well evidenced."),
+            Clause::non_goal("C2", "This is deliberately not built."),
+        ]);
+        let ws = vec![witness(
+            &spec,
+            "C1",
+            falsifiable(Anchor::Specification),
+            &auditor,
+            state().address,
+        )];
+        out.push(Case {
+            name: "03-an-unwitnessed-non-goal-does-not-cap",
+            expect: Expect {
+                intent: "A requirement at E3 beside an unwitnessed non-goal.".into(),
+                trap: "Treating the non-goal as an owed obligation with no evidence \
+                       empties the grade. A non-goal is owed nothing, so its absence \
+                       of evidence is the correct state and caps nothing."
+                    .into(),
+                direction: "under-grading".into(),
+                grade: Some(Grade::Falsifiable),
+                attestation: Some(Attestation::Independent),
+                flags: vec![],
+                clauses: vec![
+                    ExpectClause { label: "C1".into(), grade: Some(Grade::Falsifiable), stale: 0 },
+                    ExpectClause { label: "C2".into(), grade: None, stale: 0 },
+                ],
+                conformant_at_e3: true,
+            },
+            work: work_by(&spec, "C1", &implementer),
+            spec,
+            state: state(),
+            witnesses: ws,
+        });
+    }
+
+    // 4 ── A witnessed non-goal is a flag, and flags block conformance.
+    {
+        let spec = spec_of(vec![
+            Clause::requirement("C1", "The obligation is well evidenced."),
+            Clause::non_goal("C2", "This is deliberately not built."),
+        ]);
+        let ws = vec![
+            witness(&spec, "C1", falsifiable(Anchor::Specification), &auditor, state().address),
+            witness(&spec, "C2", falsifiable(Anchor::Specification), &auditor, state().address),
+        ];
+        out.push(Case {
+            name: "04-evidence-for-a-non-goal-is-a-flag",
+            expect: Expect {
+                intent: "Something implements the clause that says not to.".into(),
+                trap: "Counting the non-goal's evidence as a rung, or discarding it \
+                       quietly. It is a flag, and §3.4 makes any flag block conformance \
+                       even where every grade is satisfied."
+                    .into(),
+                direction: "over-grading".into(),
+                grade: Some(Grade::Falsifiable),
+                attestation: Some(Attestation::Independent),
+                flags: vec!["NonGoalWitnessed".into()],
+                clauses: vec![
+                    ExpectClause { label: "C1".into(), grade: Some(Grade::Falsifiable), stale: 0 },
+                    ExpectClause { label: "C2".into(), grade: None, stale: 0 },
+                ],
+                conformant_at_e3: false,
+            },
+            work: work_by(&spec, "C1", &implementer),
+            spec,
+            state: state(),
+            witnesses: ws,
+        });
+    }
+
+    // 5 ── An unstated anchor caps a falsifiable check at E2.
+    {
+        let spec = spec_of(vec![Clause::requirement(
+            "C1",
+            "The obligation is checked by something whose expectation is unstated.",
+        )]);
+        let ws = vec![witness(
+            &spec,
+            "C1",
+            falsifiable(Anchor::Unstated),
+            &auditor,
+            state().address,
+        )];
+        out.push(Case {
+            name: "05-an-unstated-anchor-caps-at-exercised",
+            expect: Expect {
+                intent: "A check with a killed counter-artifact but no stated anchor."
+                    .into(),
+                trap: "Reading the counter-artifact alone and awarding E3. An oracle \
+                       derived from the system under test cannot disagree with it, so \
+                       §2.5 caps an unstated anchor at E2 however the check behaved."
+                    .into(),
+                direction: "over-grading".into(),
+                grade: Some(Grade::Exercised),
+                attestation: Some(Attestation::Independent),
+                flags: vec![],
+                clauses: vec![ExpectClause {
+                    label: "C1".into(),
+                    grade: Some(Grade::Exercised),
+                    stale: 0,
+                }],
+                conformant_at_e3: false,
+            },
+            work: work_by(&spec, "C1", &implementer),
+            spec,
+            state: state(),
+            witnesses: ws,
+        });
+    }
+
+    // 6 ── A proof nobody independent read is E2, not E4.
+    {
+        let spec = spec_of(vec![Clause::requirement(
+            "C1",
+            "The obligation is discharged as a proof under the prover's own formalization.",
+        )]);
+        let ws = vec![witness(
+            &spec,
+            "C1",
+            proved(
+                Grounding::Declared,
+                Vacuity::Refuted { counter: Address::of_bytes(b"eval-counter-model") },
+            ),
+            &auditor,
+            state().address,
+        )];
+        out.push(Case {
+            name: "06-a-declared-formalization-caps-at-exercised",
+            expect: Expect {
+                intent: "A non-vacuous proof whose binding to the clause is the \
+                         prover's own word."
+                    .into(),
+                trap: "Awarding E4 because a prover succeeded. The proof is real \
+                       machine-checked evidence about something — E2 — and that the \
+                       something is this clause is unconfirmed (§2.6)."
+                    .into(),
+                direction: "over-grading".into(),
+                grade: Some(Grade::Exercised),
+                attestation: Some(Attestation::Independent),
+                flags: vec![],
+                clauses: vec![ExpectClause {
+                    label: "C1".into(),
+                    grade: Some(Grade::Exercised),
+                    stale: 0,
+                }],
+                conformant_at_e3: false,
+            },
+            work: work_by(&spec, "C1", &implementer),
+            spec,
+            state: state(),
+            witnesses: ws,
+        });
+    }
+
+    // 7 ── A possibly-vacuous proof is E2, even cross-checked.
+    {
+        let spec = spec_of(vec![Clause::requirement(
+            "C1",
+            "The obligation is discharged as a proof nobody checked for vacuity.",
+        )]);
+        let ws = vec![witness(
+            &spec,
+            "C1",
+            proved(
+                Grounding::CrossChecked { by: crosschecker.verifying_key().to_bytes() },
+                Vacuity::Unchecked,
+            ),
+            &auditor,
+            state().address,
+        )];
+        out.push(Case {
+            name: "07-an-unchecked-vacuity-caps-at-exercised",
+            expect: Expect {
+                intent: "A proof with an independently cross-checked formalization, \
+                         never shown capable of failing."
+                    .into(),
+                trap: "Awarding E4 because the formalization was cross-checked. A \
+                       property can hold because nothing reaches the condition it \
+                       guards; every rung above E2 rests on a demonstrated failure."
+                    .into(),
+                direction: "over-grading".into(),
+                grade: Some(Grade::Exercised),
+                attestation: Some(Attestation::Independent),
+                flags: vec![],
+                clauses: vec![ExpectClause {
+                    label: "C1".into(),
+                    grade: Some(Grade::Exercised),
+                    stale: 0,
+                }],
+                conformant_at_e3: false,
+            },
+            work: work_by(&spec, "C1", &implementer),
+            spec,
+            state: state(),
+            witnesses: ws,
+        });
+    }
+
+    // 8 ── A witness bound to a superseded state does not count.
+    {
+        let spec = spec_of(vec![Clause::requirement(
+            "C1",
+            "The obligation was checked against an earlier tree.",
+        )]);
+        let ws = vec![witness(
+            &spec,
+            "C1",
+            falsifiable(Anchor::Specification),
+            &auditor,
+            Address::of_bytes(b"eval-tree-v0"),
+        )];
+        out.push(Case {
+            name: "08-a-superseded-state-makes-a-witness-stale",
+            expect: Expect {
+                intent: "The only witness observed a tree that is no longer the \
+                         artifact, and declared no footprint."
+                    .into(),
+                trap: "Counting it because it verifies and names a stated obligation. \
+                       An empty footprint means the whole artifact, so any change to \
+                       the artifact invalidates it — and the clause is then unevidenced, \
+                       which empties the grade rather than lowering it."
+                    .into(),
+                direction: "over-grading".into(),
+                grade: None,
+                attestation: None,
+                flags: vec![],
+                clauses: vec![ExpectClause {
+                    label: "C1".into(),
+                    grade: None,
+                    stale: 1,
+                }],
+                conformant_at_e3: false,
+            },
+            work: work_by(&spec, "C1", &implementer),
+            spec,
+            state: state(),
+            witnesses: ws,
+        });
+    }
+
+    // 9 ── A witness naming an obligation nobody stated is a flag.
+    {
+        let stated = spec_of(vec![Clause::requirement(
+            "C1",
+            "The obligation as the specification now words it.",
+        )]);
+        // A witness bound to the wording the clause used to have.
+        let older = spec_of(vec![Clause::requirement(
+            "C1",
+            "The obligation as the specification used to word it.",
+        )]);
+        let ws = vec![Witness::new(
+            stated.spec.spec_id().unwrap(),
+            obligation(&older, "C1"),
+            state().address,
+            falsifiable(Anchor::Specification),
+            Energy::new(1_000, Provenance::Estimator),
+            auditor.verifying_key().to_bytes(),
+        )
+        .sign(&auditor)
+        .expect("signs")];
+        out.push(Case {
+            name: "09-a-witness-for-a-reworded-clause-is-a-flag",
+            expect: Expect {
+                intent: "A verifying witness whose obligation address is the clause's \
+                         previous wording."
+                    .into(),
+                trap: "Discarding it silently, which is how drift stops being visible. \
+                       It is reported as unbound, and the clause it used to evidence \
+                       is now unevidenced."
+                    .into(),
+                direction: "over-grading".into(),
+                grade: None,
+                attestation: None,
+                flags: vec!["Unbound".into()],
+                clauses: vec![ExpectClause {
+                    label: "C1".into(),
+                    grade: None,
+                    stale: 0,
+                }],
+                conformant_at_e3: false,
+            },
+            work: work_by(&stated, "C1", &implementer),
+            spec: stated,
+            state: state(),
+            witnesses: ws,
+        });
+    }
+
+    // 10 ── A review by the clause's own author is a citation again.
+    {
+        let spec = spec_of(vec![Clause::requirement(
+            "C1",
+            "The obligation was reviewed by the party that wrote the specification.",
+        )]);
+        let ws = vec![witness(
+            &spec,
+            "C1",
+            Evidence::Reviewed { reviewer: key(1).verifying_key().to_bytes() },
+            &key(1),
+            state().address,
+        )];
+        out.push(Case {
+            name: "10-a-self-review-is-the-citation-again",
+            expect: Expect {
+                intent: "The reviewer and the specification's author are one key."
+                    .into(),
+                trap: "Awarding E1 because the evidence says `reviewed`. E1 requires a \
+                       second party, and independence is computed from the keys rather \
+                       than taken from the label."
+                    .into(),
+                direction: "over-grading".into(),
+                grade: Some(Grade::Cited),
+                attestation: Some(Attestation::SelfAttested),
+                flags: vec![],
+                clauses: vec![ExpectClause {
+                    label: "C1".into(),
+                    grade: Some(Grade::Cited),
+                    stale: 0,
+                }],
+                conformant_at_e3: false,
+            },
+            work: work_by(&spec, "C1", &key(1)),
+            spec,
+            state: state(),
+            witnesses: ws,
+        });
+    }
+
+    out
+}
+
+fn json<T: Serialize>(value: &T) -> String {
+    let mut s = serde_json::to_string_pretty(value).expect("serialises");
+    s.push('\n');
+    s
+}
+
+#[test]
+fn every_case_reaches_the_verdict_the_specification_requires() {
+    let generate = std::env::var("JOULESPEC_GEN_EVALUATION").is_ok();
+    let mut mismatched = Vec::new();
+
+    for case in cases() {
+        let got = conform::evaluate(&case.spec, &case.state, &case.witnesses, &case.work)
+            .unwrap_or_else(|e| panic!("{}: evaluation failed: {e}", case.name));
+        let seen = observed(&got, &case.expect);
+
+        if seen != case.expect {
+            mismatched.push(format!(
+                "{}\n  expected {:#?}\n  observed {:#?}",
+                case.name, case.expect, seen
+            ));
+        }
+
+        let into = dir().join(case.name);
+        if generate {
+            std::fs::create_dir_all(&into).expect("case directory");
+            for (name, body) in [
+                ("spec.json", json(&case.spec)),
+                ("state.json", json(&case.state)),
+                ("witnesses.json", json(&case.witnesses)),
+                ("work.json", json(&case.work)),
+                // The expectation as this test *states* it, never as the
+                // evaluator produced it.
+                ("expect.json", json(&case.expect)),
+            ] {
+                std::fs::write(into.join(name), body).expect("writes");
+            }
+        } else {
+            let published = std::fs::read_to_string(into.join("expect.json")).unwrap_or_else(|e| {
+                panic!("{}: cannot read published expectation: {e}", case.name)
+            });
+            let published: Expect =
+                serde_json::from_str(&published).expect("published expectation parses");
+            assert_eq!(
+                published, case.expect,
+                "{}: the published expectation and this test disagree",
+                case.name
+            );
+        }
+    }
+
+    assert!(
+        mismatched.is_empty(),
+        "the evaluator disagrees with the specification on {} case(s):\n\n{}",
+        mismatched.len(),
+        mismatched.join("\n\n")
+    );
+}
+
+/// A corpus that tested one direction would certify one direction, so this
+/// asserts the shape of the set rather than trusting that it was built as
+/// described.
+///
+/// Both directions have to be present. An implementation that graded nothing
+/// at all would pass every over-grading case — the under-grading cases are
+/// what stop a corpus from rewarding a rule that simply refuses everything.
+#[test]
+fn the_corpus_tests_both_directions_and_says_which() {
+    let all = cases();
+    assert!(all.len() >= 10, "the corpus has shrunk: {}", all.len());
+
+    let mut over = 0;
+    let mut under = 0;
+    for case in &all {
+        assert!(
+            !case.expect.trap.is_empty() && !case.expect.intent.is_empty(),
+            "{}: a case without a stated trap documents nothing",
+            case.name
+        );
+        match case.expect.direction.as_str() {
+            "over-grading" => {
+                over += 1;
+                // The correct verdict must fall short of the bar, or be
+                // blocked by a flag. A case that conformed cleanly would be
+                // passed by a generous implementation for the wrong reason.
+                assert!(
+                    !case.expect.conformant_at_e3 || !case.expect.flags.is_empty(),
+                    "{}: labelled over-grading but conforms at E3 with no flag",
+                    case.name
+                );
+            }
+            "under-grading" => {
+                under += 1;
+                // The correct verdict must *reach* the bar, or the case
+                // cannot catch an implementation that is too strict.
+                assert!(
+                    case.expect.conformant_at_e3,
+                    "{}: labelled under-grading but does not conform at E3, so a \
+                     refuse-everything implementation passes it",
+                    case.name
+                );
+            }
+            other => panic!("{}: unknown direction {other:?}", case.name),
+        }
+    }
+    assert!(over >= 8, "too few over-grading cases: {over}");
+    assert!(under >= 1, "no under-grading case: a refuse-everything evaluator passes");
+}