open-standards/joulespec/SPEC.md

# JouleSpec v0.2 — A Standard for Energy-Accounted Specification Conformance

| | |
|---|---|
| **Standard** | joulespec |
| **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/) |

A vendor-neutral standard for **stating what software owes and measuring
whether anything established it**. JouleSpec specifies an obligation address
that survives renaming and breaks on rewording, a five-rung evidence ladder
from testimony to proof, a deterministic drift partition over revisions, and a
receipt that seals what a specification cost to evidence.

JouleSpec is one of the [Transaction Science open standards](../README.md).
Transaction Science is the steward, not the proprietor.

---

## 1. Scope and doctrine

### 1.1 What JouleSpec decides

JouleSpec decides four questions and no others: **what does this software
owe**, **what is known about each obligation and how well**, **which of that
knowledge survives a change**, and **what did establishing it cost**.

It does not write specifications, does not run checks, does not formalize a
clause on anyone's behalf, and does not judge whether a clause states a good
requirement. Those belong to the author, the test runner, the prover, and the
reviewer respectively. JouleSpec is the part that holds their outputs together
and refuses to report them as interchangeable.

### 1.2 The specification is prose; the obligation is an address

A clause is a sentence a person wrote. That does not change under this
standard, and nothing here asks an author to write a requirement in a formal
notation.

What changes is that a clause carries two identifiers, not one:

- a **label** — `C1`, `auth-2` — which is editorial, exists so reports and
  conversations have a short handle, and may be changed freely;
- an **obligation**, the content address of the clause's *kind and text*, with
  the label deliberately excluded.

Evidence binds to the obligation. The consequence is the mechanism this
standard turns on:

> Renaming a clause moves no obligation and loses no evidence. Changing one
> word of a clause is a different obligation, and every piece of evidence bound
> to the old wording stops applying — with nobody having to notice.

Binding evidence to a label inverts both halves: it survives the edit that
changed the requirement and breaks on the edit that renamed it. Prevailing
practice binds to labels, or to nothing at all, which is why specification
drift is discussed as a discipline problem. It is an addressing problem, and an
address is the whole fix.

### 1.3 Conformance is a grade, not a claim

The prevailing artifact of specification-driven practice is prose an agent
interprets and a human reads, and its verdict is a sentence in a review. A
sentence cannot be compared across changes, cannot be capped by its weakest
part, and cannot distinguish "an agent said it was done" from "no input
violates it".

In `joulespec/1` every piece of evidence lands on a rung of an ordered ladder
(§2.5), and a specification's grade is the grade of its weakest owed obligation
(§3.2). An implementer's claim is a real rung — the bottom one — reported as
the testimony it is rather than as conformance.

### 1.4 A figure's grade is part of the verdict

Every energy figure carries how it was obtained: a counter read for this work,
a calibrated model, or a default guess. An aggregate is graded by its weakest
contributing figure, never by its best, and a receipt that summed one reading
and one guess reports a guess (§5.1). This is the same discipline the rest of
this family applies to every measured quantity it publishes.

---

## 2. Objects

### 2.1 The clause and its obligation

A clause is `{label, kind, text}` where `kind` is one of:

| Kind | Meaning |
|---|---|
| `requirement` | Behaviour the implementation must exhibit. |
| `constraint` | A bound it must stay inside — interface, dependency, style, energy. |
| `non-goal` | Behaviour deliberately out of scope. |

Non-goals are first-class. Writing down what a system must *not* do is half the
value of a design conversation, and a non-goal is checkable in a way the field
usually discards: evidence that something implements it is a finding (§3.3).

The **obligation** is the content address of the canonical document
`{kind, text}`. Text is compared exactly: an author who reflows a paragraph has
changed the obligation as far as this standard is concerned. That is the
conservative direction — evidence is dropped, never silently carried forward.

Because `kind` is addressed, moving a clause from `requirement` to `non-goal`
is a change of obligation. Deciding not to build something is not an editorial
act.

A conforming implementation MUST refuse a specification in which two clauses
state the same obligation. They would share an address, so evidence for one
would silently witness the other. The refusal MUST name both clauses: a report
naming only the second sends the author to the wrong place.

### 2.2 The specification

A specification is `{profile, alg, intent, clauses, parent?, author}`:
an intent in the author's words, ordered clauses with unique labels and
distinct obligations, an optional parent, and the author's key. Its address is
the content address of its canonical document; it is signed over
`spec_id ‖ parent`, so the signature binds a revision to its lineage.

A specification that does not validate has no address. There is no such thing
as the address of a document that does not hold together.

### 2.3 Revision

A revision names its predecessor by address, so the history of what was
approved is tamper-evident, and a reviser signs with their own key. A revision
is not required to be an improvement and the standard takes no position on who
may make one; it records who did.

### 2.4 The witness

A witness is one signed record binding four things:

| Field | Why it is bound |
|---|---|
| `spec` | Which specification this is about. |
| `obligation` | Which obligation — an address, never a label. |
| `artifact` | Which artifact state the evidence was observed against. |
| `evidence` | What was observed, with its full payload. |
| `energy` | What observing it cost, with provenance. |

The signature covers `witness_id ‖ spec ‖ obligation ‖ artifact`, so none of
those can be swapped under a valid signature.

The **artifact binding is what makes staleness computable.** Evidence gathered
against one state of the code says nothing about another, and a witness that
does not name the state it observed cannot be aged out. In practice this is a
tree digest, a build output address, or a commit — JouleSpec does not care
which, only that it is an address.

A witness also names a **footprint**: the addresses *within* that state the
evidence depended on.

This is not an optimisation. Binding evidence to a whole-tree digest alone
makes every commit stale every witness, and that is the documented way
traceability dies: the empirical literature on trace links finds they degrade
mainly through ordinary refactoring, and reports that keeping them current can
cost more than creating them. A standard whose evidence expires on every
unrelated edit has reproduced that failure exactly, however sound its
addressing.

A witness applies at a state when the state is the one it observed, or when
every footprint member is still present in it (§3.1). Paths are deliberately
absent from the mechanism: a content address *is* the identity of its content,
so membership answers "is this input still what the evidence saw" without the
standard having to agree with anyone about file naming.

A footprint is a producer's claim that nothing else mattered. It is signed with
the rest of the witness, and a narrower footprint is a **stronger** claim — so
a wrong one makes the evidence wrong rather than merely stale. An **empty**
footprint means the whole artifact, which is the conservative reading and the
one a producer that cannot enumerate its inputs MUST use.

### 2.5 The evidence ladder

Every rung answers one question: **how hard would it be for this obligation to
be violated without this evidence noticing?**

| Grade | Name | What it establishes |
|---|---|---|
| `E0` | `cited` | The implementer claims it is done. Nothing noticed anything. |
| `E1` | `reviewed` | A second party read the artifact against the clause, once. |
| `E2` | `exercised` | A named check ran against the artifact and passed. |
| `E3` | `falsifiable` | The same check is on record *failing* against a named counter-artifact. |
| `E4` | `proved` | No input violates it, under a formalization someone independent checked. |

Three rungs need their reasons stated.

**`E0` is where prevailing practice lands.** A clause an agent claims to have
implemented, with a human skim at the end, is testimony from the party being
evaluated. Much of it is true. It is still testimony, and reporting it as
conformance is the error this standard exists to stop.

**`E2` flatters.** A green check establishes that something ran, not that the
obligation holds. A test with no assertion passes; so does one whose fixture
never reaches the condition the clause cares about. Nothing at `E2`
distinguishes those from a real check.

**`E3` is the first rung where green means something.** A check recorded as
failing against a named counter-artifact — a mutant, a reverted fix, a
deliberately broken build — has demonstrated that it *can* fail, so its passing
carries information. This is the cheapest strong rung, and the one most
projects can reach with tests they already have.

**The ladder is ordered by re-checkability, not by diligence.** A human review
is bound to the state a person looked at and cannot notice a violation
introduced afterwards; a named check can run again against any later state.
That ordering says nothing about how carefully anyone read the code — it says
that one kind of evidence survives the next commit and the other does not. It
has a second consequence worth stating: the higher rungs are also the cheapest
to **refresh** when a footprint member moves, because a named check can simply
be run again.

#### Every rung above `E2` rests on a demonstrated failure

That rule is uniform, and it binds proofs as much as tests. A formal property
can be satisfied **vacuously** — true because nothing in the model ever
reaches the condition it guards, so it would hold of almost any
implementation. Detecting this is established practice in model checking,
where a property is understood as vacuous when it can be replaced by a
constant without changing its value in the model, and one industrial
verification setting reported around a fifth of specifications initially
passing that way.

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
expected value is derived from the system it is judging cannot disagree with
that system when a fault moves the measurement and the expectation together —
the comparison cancels, and no input reveals the fault. The defect is in the
oracle rather than in the inputs, and it is visible from the oracle's
construction without running anything.

Every check therefore declares an **anchor**:

| Anchor | Meaning |
|---|---|
| `specification` | Expected values are fixed outside the code under test — the specification, a published procedure, a reference table, an independently computed model. |
| `state` | Expected values flow, directly or indirectly, from the code under test. |
| `unstated` | The producer has not said. |

An **unstated** anchor caps a check at `E2`, because whether an oracle reads
its expectation from its own subject is knowable to whoever wrote it at no
cost, and silence is not an answer. A **state**-anchored check that killed a
counter-artifact really did fail once and reaches `E3`, with its anchor
disclosed — the class of faults it cannot catch is disclosed with it. This
standard does not refuse state-anchored evidence; it refuses to report it as
indistinguishable from the other kind.

The anchor is part of the signed witness, so two anchors are two different
claims and two different witnesses.

#### What the equivalent-mutant problem does not cost

Mutation scoring is noisy and contested because a mutant semantically
identical to the original cannot be killed, so it depresses a score without
indicating any weakness; reported rates range from a few per cent to roughly a
third of mutants, and one large-scale industrial account found most generated
mutants unproductive until mutation was restricted to changed lines.

`E3` is immune in the direction that matters: it only ever uses a mutant the
check **did** kill as positive evidence. An equivalent mutant cannot produce an
`E3` witness at all, so the problem that makes scores expensive cannot inflate
a grade here. The cost of the rung is correspondingly low — one killed mutant
per obligation, which a project can harvest from tests it already has.

**Independence is computed, never declared.** A review signed by the key that
made the citation is the citation again, and grades `E0`. A conforming
implementation MUST compute this from key disjointness and MUST NOT read it
from a field the producer set.

### 2.6 Formalization, and what an `E4` claims

A proof discharges a formal statement. The statement is not the clause; the
binding between them is a human act, and it is the weakest link in any claim of
proved conformance. A conforming implementation MUST NOT formalize a clause on
its own initiative: a formalization is supplied, and it carries a grounding.

A proof also carries a **vacuity** state: `refuted` against a named
counter-model, or `unchecked`.

| Grounding | Vacuity | Reached grade |
|---|---|---|
| `cross-checked` by a key other than the witness author's | `refuted` | `E4` |
| `cross-checked` by another key | `unchecked` | `E2` |
| `declared` | any | `E2` |
| `cross-checked` by the witness author's own key | any | `E2` |

There are two independent ways a proof can establish nothing about a clause:
the statement may not be the clause (ungrounded), or it may hold of almost
anything (vacuous). Either leaves real mechanical evidence about *something*,
which is `E2` — the same rung as a green check, for the same reason.

A proof under a formalization nobody independent read is machine-checked
evidence about *something*; that the something is this clause is the prover's
word. It is therefore real mechanical evidence — `E2` — and not proof of the
clause. Demoting rather than refusing is deliberate: the proof is not fake, and
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
operation, a build, a benchmark run — carrying its address, the obligations it
claims to advance, and its energy.

Work and witnesses are accounted separately. Work is what *cost* energy;
a witness is what *observed* something. Conflating them hides the question this
standard exists to answer, which is whether the evidence was worth what it
cost.

### 2.8 Attestation: the second axis

How strong a check is and how independent the party reporting it is are
different questions. Collapsing them loses the one that matters most where the
implementer and the reporter are the same process — the normal case for an
agent that writes code and then reports that it works.

A verdict therefore carries a grade **and** an attestation:

| | Attestation | Meaning |
|---|---|---|
| `A0` | `self-attested` | The party reporting the result is a party that did the work. |
| `A1` | `independent` | Signed by a key that authored none of the work on this specification. |
| `A2` | `reproduced` | Two parties with disjoint keys reported the same check at the same grade and artifact state, at least one of them independent of the work. |

Attestation is **derived, never declared**: from whether a witness's author
also authored work on this specification, and from whether disjoint parties
reported the same check. A conforming implementation MUST compute it and MUST
NOT read it from a field a producer set.

Where **no work was supplied**, no party is known to be an implementer, and
attestation is **absent** rather than assumed independent. Absence of
information about who built something is not evidence that someone else
checked it.

Supply-chain provenance frameworks grade build records on exactly this axis —
whether provenance merely exists, is signed by a hosted builder, or comes from
a hardened one — and are explicit that they say nothing about whether the
software is correct. That is the right division: those levels grade the
*record* while this ladder grades the *evidence*, and a complete claim needs
both. This family's readiness standard likewise publishes several axes with
gates between them rather than one scalar, for the same reason.

---

## 3. Evaluation

### 3.1 What counts

Evaluation takes a specification, one artifact state, the witnesses on record
and the work performed, and produces a verdict per clause plus a verdict for
the specification.

A witness contributes to a grade only when **all** of the following hold. Each
other outcome is reported, and none is discarded:

| Condition | Outcome when it fails |
|---|---|
| Its signature and structure verify | `unverifiable` flag, by input position |
| It names this specification | `foreign-spec` flag |
| It names an obligation this specification states | `unbound` flag |
| It applies at this artifact state (§2.4) | recorded as **stale** on that clause |

A witness naming an obligation the specification does not state is the normal
aftermath of a rewording, and it MUST NOT be dropped quietly — it is the
clearest available signal that evidence and specification have parted company.

A witness **applies** at a state when the state is the one it observed, or
when it narrowed itself to a footprint whose every member is still present. A
footprint that cannot be checked — because the caller cannot enumerate the
current state — is stale, which is the conservative direction.

A clause's grade is the strongest grade among its contributing witnesses, and
its attestation the strongest among them (§2.8), with the whole clause's
attestation absent where no work identifies an implementer. Where
several witnesses tie, the one with the lowest address is named, so two
evaluations over the same inputs produce the same verdict.

### 3.2 The cap is a minimum

A specification's grade is the **minimum** over its requirements and
constraints, and is absent when any of them has no surviving evidence.

Averaging would let nine proved obligations conceal one nobody looked at, which
is precisely the failure a grade exists to surface. This family applies the
same rule wherever a composite claim meets a weak component.

The **attestation** is capped the same way and separately: a specification's
attestation is the minimum over its owed obligations. The two minima are taken
independently, because a specification can be uniformly well checked by the
party that wrote it, or uniformly witnessed by an auditor who only read it.

A grade is not gameable by adding clauses, and in the direction that matters:
adding an obligation can only lower a minimum. §5.3 records the figure where
this does not hold.

### 3.3 Non-goals

Non-goals are excluded from the cap: there is nothing to evidence about
behaviour that should not exist, so an unwitnessed non-goal is correct and
carries no grade.

Evidence that a non-goal *was* implemented is a `non-goal-witnessed` flag. It
does not lower the grade of the owed obligations — they really are evidenced —
and it does block conformance (§3.4). The specification said not to build this
and something says it exists; no amount of evidence elsewhere settles that.

### 3.4 Flags block conformance

A flag is something wrong with the evidence set, as distinct from a weakly
evidenced obligation. An implementation reports conformance at a requested bar
only when every owed obligation reaches it on **both** axes and no flag is
raised.

Both axes gate because they fail separately: a proof nobody independent of the
implementer ever saw, and a citation from an independent auditor, are each
strong on one axis and weakest on the other. An **absent** attestation cannot
satisfy a bar above `A0` — absence of information about who built something is
not evidence that someone else checked it.

### 3.5 Determinism

Evaluation MUST be deterministic: the same specification, artifact, witnesses
and work in any order MUST produce an identical verdict. Collections in the
verdict are sorted, and ties are broken by address.

---

## 4. Drift

### 4.1 The partition

Diffing two revisions by obligation address yields an exact partition:

| Class | Meaning | Evidence |
|---|---|---|
| `kept` | Same obligation, same label | Survives |
| `relabelled` | Same obligation, new label | Survives |
| `reworded` | Same label, different obligation | Old evidence invalidated; new obligation unevidenced |
| `added` | Obligation only in the later revision | Unevidenced |
| `removed` | Obligation only in the earlier one | Orphaned |

From that, two sets follow directly: the obligations whose evidence no longer
applies, and the obligations that start the revision unevidenced. A revision
review wants those sets, not the fact that the specification changed.

### 4.2 Relabelling is free; rewording is not

A revision that changes only labels and ordering is **editorial** and costs no
evidence. Renumbering a whole specification lands there. This matters because a
standard that penalised renaming would teach authors not to rename, and
specifications whose labels cannot be tidied acquire labels nobody can read.

A revision that changes a clause's text costs exactly that clause's evidence,
and nothing else's.

A freed label reused by a new clause is an **addition**, not a rewording: the
old obligation still stands elsewhere in the specification, so no evidence is
invalidated. An implementation MUST distinguish these, because conflating them
would report a loss of evidence that did not happen.

### 4.3 Artifact drift

Specification drift is one of two directions. The other is the artifact moving
under evidence that stayed still, and it is handled at evaluation: a witness
bound to an earlier artifact state is reported stale rather than counted
(§3.1). Neither direction requires anyone to remember to check.

---

## 5. Cost

### 5.1 Work energy and evidence energy

A verdict accounts three figures in microjoules: energy spent on work citing at
least one of this specification's obligations, energy spent on work citing
none, and energy spent producing the surviving evidence. The provenance of the
total is the weakest provenance among every figure that fed it.

### 5.2 The specified share

The share of work energy that implements something the specification asked for
is reported in parts-per-million.

This is the measured form of an observation the field makes qualitatively —
that agents produce features nobody requested. A run in which a quarter of the
energy went into work citing no clause has a number saying so, and that number
is in the receipt.

Unspecified work is also reported as a **named list**, not only as a figure.
Certified-airborne-software practice has required traceability in both
directions for decades, and the backward direction exists for one purpose:
code with no upstream requirement is a finding even when it works correctly,
because unintended function is what the argument cannot otherwise exclude. A
figure answers *how much*; only the list answers *which*, and only the list
can be acted on.

Ratios are integers in parts-per-million because the canonical core admits no
floats (§6.2), and a ppm figure survives the round trip exactly where a rounded
percentage would not.

### 5.3 Microjoules per falsifiable obligation

The headline figure is total attributed energy divided by the number of owed
obligations evidenced at `E3` or better.

The denominator is deliberately the rung whose evidence can fail. A figure per
*attempted* obligation rewards ceremony; a figure per obligation that something
would actually have caught rewards evidence. The family's other per-unit
figures make the same choice, counting accepted output and verified proofs
rather than attempts.

Where nothing reaches the bar the figure is **absent**, not zero. A cost per
unit of nothing is not a small number.

#### Comparable only at a fixed specification

Any figure of the form *things evidenced over things total* can be improved by
adding trivial things. This is the standing objection to counting resolved
doubts in assurance argumentation, where confidence can be inflated by raising
and then dismissing easy ones. Here the denominator is a clause count, so
splitting one requirement into twenty trivially falsifiable ones divides the
figure by twenty while establishing nothing new.

The figure is therefore comparable **only between evaluations carrying the same
specification address**, which is the comparison it exists for: two processes
against one specification. A receipt seals that address (§6.3) precisely so a
reader can tell whether two figures are comparable at all, and an
implementation MUST NOT present the figure as a cross-specification benchmark.

The grade and the attestation carry no such caveat; both are minima, and a
minimum cannot be improved by adding obligations.

This figure is what makes the field's central argument decidable. Whether
specification-driven practice earns its overhead is currently settled by
anecdote in both directions. Two processes applied to the same specification,
reaching the same evidence, with one spending an order of magnitude more energy
to get there, is not a matter of taste.

---

## 6. The receipt

### 6.1 Sealed from the inputs, never from a verdict

A conforming implementation MUST derive a receipt from the specification, the
artifact, the witnesses and the work — and MUST NOT seal a verdict handed to it.

A verdict is an ordinary data structure. An interface that signed one would let
a producer construct the grade it wanted and obtain a receipt saying so.
Because the receipt is derived from the evidence, any claim in it is
reproducible by anyone holding the same inputs, and a producer who wants a
better grade has to go and get better evidence.

### 6.2 Absent, not zero

Receipts seal as **JCR-1** envelopes — canonical det-CBOR (RFC 8949 §4.2.1)
inside a COSE_Sign1 envelope (RFC 9052, EdDSA/Ed25519) — the signed-receipt
format shared across this family, verifiable by tooling that has never heard of
JouleSpec.

That core admits no nulls, and several figures here are legitimately absent: a
specification with an unevidenced requirement has no grade; a run with no work
has no specified share. Such fields MUST be **omitted**, never sealed as zero. A
reader who finds no grade knows none was established; a reader who found `E0`
would believe one was.

### 6.3 The per-clause audit

A receipt carries one entry per clause — label, kind, obligation, grade and
attestation where established, the **means** (the kind of evidence that
carried the grade), its **anchor** where its kind declares one, the witness
that carried it, evidence energy, and the count of stale witnesses — alongside
the specification-level summary and the named list of unspecified work.

The means is load-bearing, not decoration: two clauses at `E2` can be a green
check and a proof whose statement nobody tied to the clause, and a grade alone
cannot tell a reader which it is looking at.

Which obligation is the weak one is the actionable fact. It must be answerable
from the receipt alone, rather than by re-running an evaluation whose inputs
nobody kept.

---

## 7. Conformance

An implementation conforms to `joulespec/1` when:

1. **C1 — Addressing.** Obligation addresses are computed over `{kind, text}`
   with the label excluded; relabelling preserves an address and rewording
   changes it.
2. **C2 — Validation.** Specifications with a duplicate label, a duplicate
   obligation, an empty intent, an empty clause, or no clauses are refused, and
   a duplicate obligation names both clauses.
3. **C3 — Signatures.** Specifications and witnesses verify over the preimages
   in §2.2 and §2.4, and altering any bound field invalidates the signature.
4. **C4 — The ladder.** Grades are assigned per §2.5 and §2.6, with
   independence computed from key disjointness.
5. **C5 — Evaluation.** The weakest-owed-obligation cap, the non-goal rule, the
   four flag conditions, staleness, and determinism under reordering all hold
   per §3.
6. **C6 — Drift.** The §4.1 partition is computed by address, editorial
   revisions invalidate nothing, and a reused label is distinguished from a
   rewording.
7. **C7 — Cost.** Aggregates carry the weakest contributing provenance; ratios
   are integer parts-per-million; absent figures are absent.
8. **C8 — Receipts.** Receipts are derived from inputs, seal as JCR-1, omit
   absent fields, and carry the per-clause audit with means and anchor.
9. **C9 — Footprints.** A witness applies at the state it observed, and at a
   later state whose parts still contain every footprint member; an empty or
   uncheckable footprint is stale (§2.4, §3.1). The footprint is signed, so
   widening it after signing invalidates the witness.
10. **C10 — Demonstrated failure.** No evidence reaches `E3` without a killed
    counter-artifact and a stated anchor, and none reaches `E4` without both an
    independently cross-checked formalization and a refuted statement (§2.5,
    §2.6).
11. **C11 — Attestation.** The second axis is computed from work authorship and
    from agreement between disjoint parties, is absent where no implementer is
    known, and gates conformance alongside the grade (§2.8, §3.4).

A third-party implementation certifies itself by round-tripping the published
vectors in [`conformance/v1/vectors/`](conformance/v1/vectors/): fixed keys,
fixed clauses, fixed witnesses and fixed energy, carrying one witness of every
rung the format can express plus one bound to a superseded artifact state, so
an implementation that mishandles any rung or mishandles staleness fails the
pack rather than passing it quietly.

### 7.1 The reference implementation does not certify itself by assertion

"Conformant by construction" is the claim this standard exists to distrust, so
the reference implementation is held to its own ladder. Each item above is
mapped to a check, and each mapping declares a **counter-artifact** — a
one-occurrence edit that should make that check fail. The reference producer
applies it, runs the check, requires a *failure*, reverts, and only then emits
a witness at `E3` ([`conformance/v1/harvest.toml`](conformance/v1/harvest.toml)).

The mapping from item to check is declared by the operator and not inferred,
for the same reason a formalization is never inferred (§2.6): deciding that a
particular check stands for a particular obligation is a human judgement, and a
tool that guessed it would be grading its own guess.

Running this against the implementation found two things inspection had not: a
check whose assertion could not fail, because it narrowed to a single footprint
member where `all` and `any` coincide; and a guard in `applies_at` that could
not change a single verdict. Both are recorded in
[`conformance/v1/README.md`](conformance/v1/README.md). That is the `E3` rung
doing the only thing it claims to do.

The self-conformance receipt in that directory is a **measurement, not a
vector**: its energy figures come from a wall clock, so re-running the harvest
produces different bytes. Only `vectors/` is byte-stable, and the division is
deliberate — a pack that held measured energy fixed would be publishing a
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
standard measures evidence against stated obligations; it does not validate
obligations against intent, and no address makes a bad requirement good.

**A grade is a property of evidence, not of software.** `E4` across every clause
means no input violates the formalizations that were checked. Software can
satisfy every clause of its specification and be unfit for its purpose, because
the specification was incomplete — and an incomplete specification is exactly
the case where every clause is covered.

**Falsifiability is demonstrated, not guaranteed.** An `E3` witness records that
a check failed against one named counter-artifact. That establishes the check
can fail; it does not establish that the check would catch every way the
obligation could be broken.

**A specified share is not a quality measure.** Work citing no clause may be
necessary — a refactor, a build fix, a dependency bump. The figure says how
much energy went into work nobody asked for in this specification, which is a
question worth having an answer to, and not a verdict.

**Energy figures are as good as their meters.** A figure graded as a default
guess is a guess no matter how precisely it is reported, which is why the grade
travels with the number and why an aggregate never claims better than its
weakest part.

**A footprint is trusted, not verified.** A producer that narrows a witness to
inputs the check did not really depend on gets evidence that outlives the
change which invalidated it. The footprint is signed and disclosed, so the
claim is attributable and reviewable, but this standard cannot tell what a
check actually read. An implementation that can observe its own reads should
emit the footprint it observed; one that cannot MUST leave it empty rather
than guess.

**`A2` is agreement, not correctness.** Two parties running the same check and
getting the same answer have excluded a mistake in the running, not a mistake
in the check. Reproduction of a vacuous check reproduces the vacuity.

**The cost figure is comparable only at a fixed specification** (§5.3). A
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
single author. The *mechanisms* stand on their own — an expectation derived
from the system cannot disagree with it when both move; a property replaceable
by a constant constrains nothing — and the design rests on those arguments
rather than on the magnitudes.

---

## 9. Relation to existing work

JouleSpec is not the first attempt to tie claims to evidence. It is narrow
about what it adds, and the things it does not re-invent are worth naming.

**Structured assurance cases** already standardize the shape of the argument: a
claim decomposed into sub-claims until each is linked to evidence, with the
inference between them stated. The international standard for assurance-case
structure and content is explicit that it sets requirements for structure and
contents and **not** quality requirements for the content — and the grade of a
piece of evidence is exactly that content question. `joulespec/1` adopts the
vocabulary (a clause is a claim; a witness is evidence; an obligation with no
evidence is undeveloped) and supplies the part left open: an ordered,
mechanically computed grade, and a cap that makes the composite no stronger
than its weakest link.

**Certified-airborne-software practice** supplies the bidirectional rule
(§5.2): code with no upstream requirement is a finding even when it works.
It also grades *structural* coverage — statement, decision, modified
condition/decision — on a ladder of its own, by criticality level. That ladder
is orthogonal to this one and composes with it: a check's coverage criterion
describes how thoroughly it exercises the code, where an anchor and a killed
counter-artifact describe whether it can fail at all. A deployment that
requires both is stating two different things, and should.

**Supply-chain provenance frameworks** grade the trustworthiness of the build
*record* and say nothing about whether the software is correct. That is the
`A` axis of §2.8 and this standard does not duplicate it: a conforming
deployment can carry provenance levels for its artifacts and attestation grades
for its evidence, and they answer different questions.

**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
shape, with an evidenced obligation as the functional unit. That standard
covers the energy of *running* software; the energy of *producing* it is
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.

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.

---

*JouleSpec is stewarded by [Transaction Science](https://transaction.science).
The protocol is owned by no one; the right to fork is public.*