open-standards/joulespec/README.md

# JouleSpec — Energy-Accounted Specification Conformance

**Version:** 0.2.0-draft.1 · **Status:** Draft · **Profile:** `joulespec/1`
**Specification text:** CC-BY-4.0 · **Reference code (`joulespec-rs/`):** Apache-2.0

JouleSpec is the open standard for **stating what software owes and measuring
whether anything established it**. A clause is addressed by its obligation, so
renaming is free and rewording costs exactly that clause's evidence. Evidence
climbs a ladder from testimony to proof. A revision yields the exact set of
obligations that just lost their evidence. And the receipt says what the whole
exercise cost in joules.

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

## The problem is measurement, not methodology

Specification-driven practice converged on a shared shape: write the intent
down, derive the plan and the implementation from it, review at each phase. The
artifact it produces is prose an agent interprets and a human reads, and the
difficulties that follow are catalogued consistently wherever the practice is
examined — specifications drifting from the code they describe, generated
artifacts trusted past their evidence, no method for checking that an
implementation conforms, and a review burden heavy enough that practitioners
report preferring to read the code.

Each of those is a measurement problem wearing a methodology costume, and each
persists for the same reason: **the specification is a document.** A clause
cannot be addressed, so nothing can bind to it. Conformance is a sentence in a
review, so it cannot be graded or capped. The cost of the ceremony is an
anecdote, so the argument about whether it is worth the effort has no units and
cannot be settled.

JouleSpec changes none of the methodology. It changes what the specification
*is*.

## Renaming is free; rewording is not

A clause carries a label and an **obligation**. The label — `C1`, `auth-2` — is
editorial. The obligation is the content address of the clause's kind and text,
with the label deliberately excluded (SPEC §1.2), and evidence binds to the
obligation.

```
  C1  "The endpoint rejects unauthenticated requests."    → b3:9f4c…
  auth-2  "The endpoint rejects unauthenticated requests." → b3:9f4c…   same obligation
  C1  "The endpoint should reject unauthenticated requests." → b3:2e71…  different obligation
```

Renumbering a whole specification moves nothing and loses no evidence.
Weakening one requirement by one word invalidates that clause's evidence and
nothing else's — automatically, with nobody having to notice.

Binding evidence to a label gets both halves backwards: it survives the edit
that changed the requirement and breaks on the edit that renamed it. That
inversion is the mechanism by which drift goes unobserved. It is an addressing
problem, not a discipline problem, and an address is the whole fix.

## A ladder ordered by one question

How hard would it be for this obligation to be violated **without this evidence
noticing?**

| | | |
|---|---|---|
| `E0` | `cited` | The implementer says it is done. Nothing noticed anything. |
| `E1` | `reviewed` | A second party read the artifact, 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, shown not to hold vacuously. |

**Every rung above `E2` rests on a demonstrated failure**, and the rule binds
proofs as much as tests. A formal property can be satisfied *vacuously* — true
because nothing ever reaches the condition it guards, so it would hold of
almost any implementation; detecting that is established practice in model
checking, and one industrial 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, exactly as `E3` requires a check to
have failed against a counter-artifact.

**`E0` is where prevailing practice lands**, and it 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. A test with no
assertion passes, and so does one whose fixture never reaches the condition the
clause cares about.

**`E3` is the first rung where green means something** — the check has
demonstrated it can fail, so its passing carries information. It is also the
cheapest strong rung: most projects can reach it with tests they already have,
by recording the mutant the test was written against.

The ladder is ordered by **re-checkability, not diligence**. A review is bound
to the state a person looked at; a named check runs again against any later
state. That says nothing about how carefully anyone read the code — it says one
kind of evidence survives the next commit and the other does not.

**Independence is computed, never declared.** A review signed by the key that
made the citation is the citation again, and grades `E0` (SPEC §2.5).

## Where the expectation comes from

Whether a check *can* fail is not only an empirical question. An oracle whose
expected value is derived from the system it judges 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, not the inputs, and it is visible from the oracle's construction
without running anything.

So every check declares an **anchor**: `specification` (expected values fixed
outside the code under test — the spec, a published procedure, a reference
table), `state` (values flowing from the code under test), or `unstated`. 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 mutant did
fail once and reaches `E3` — with its anchor disclosed, because the class of
faults it cannot catch is disclosed with it (SPEC §2.5).

## Evidence that survives a change it did not depend on

Binding evidence to a whole-tree digest alone would make every commit stale
every witness. That is the documented way traceability dies: the empirical
literature finds trace links 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
however sound its addressing.

A witness therefore names a **footprint** — the addresses within the artifact
it actually depended on — and applies at any later state whose parts still
contain every member (SPEC §2.4). Edit the documentation and the evidence for
the auth requirement stands; edit the auth code and that clause ages, alone.
Paths never enter the mechanism: a content address *is* the identity of its
content.

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

## Two axes, because they fail separately

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.

| | | |
|---|---|---|
| `A0` | `self-attested` | The party reporting the result did the work. |
| `A1` | `independent` | Signed by a key that authored none of the work. |
| `A2` | `reproduced` | Two disjoint parties reported the same check at the same grade and state, at least one independent of the work. |

Both axes gate conformance (SPEC §3.4). Attestation is **derived** from work
authorship and from agreement between disjoint keys — never declared — and
where no work was supplied it is **absent** rather than independent: absence of
information about who built something is not evidence that someone else checked
it.

## What an `E4` actually claims

A proof discharges a formal statement, and the statement is not the clause. The
binding between them is a human act and the weakest link in any claim of proved
conformance — so a proof reaches `E4` only when that binding was cross-checked
by a key other than the prover's. Under a merely declared formalization it
grades `E2`: real mechanical evidence about *something*, where that the
something is this clause remains the prover's word (SPEC §2.6).

The reference library never formalizes a clause on anyone's behalf. Demotion
rather than refusal is deliberate — the proof is not fake, and discarding it
would lose evidence that exists.

## The weakest obligation sets the grade

A specification's grade is the **minimum** over its requirements and
constraints, absent entirely when any of them has no surviving evidence (SPEC
§3.2). Averaging would let nine proved obligations conceal one nobody looked
at, which is the failure a grade exists to surface.

**Non-goals are first-class and handled differently.** There is nothing to
evidence about behaviour that should not exist, so an unwitnessed non-goal is
correct and carries no grade. Evidence that one *was* implemented is a flag: it
does not lower the grade of the owed obligations — they really are evidenced —
and it does block conformance. The specification said not to build this and
something says it exists.

**Nothing is dropped quietly.** A witness that does not verify, names another
specification, or names an obligation the specification does not state is a
reported finding, not a no-op. That last case is the normal aftermath of a
rewording and the clearest available signal that evidence and specification
have parted company.

## Drift is a partition, not a warning

Diffing two revisions by obligation address says exactly which evidence
survives (SPEC §4.1): obligations `kept`, `relabelled` (editorial — no evidence
lost), `reworded` (that clause's evidence invalidated, the new obligation
unevidenced), `added`, and `removed`. From those, the two sets a revision
review actually wants fall out: **what just lost its evidence**, and **what
starts unevidenced**.

A freed label reused by a new clause is an addition, not a rewording — the old
obligation still stands elsewhere, so no evidence is invalidated, and
conflating the two would report a loss that did not happen.

The other direction of drift is the artifact moving under evidence that stayed
still, and it needs no diff at all: a witness is bound to the artifact state it
observed, so evidence from an earlier state is reported stale rather than
counted (SPEC §3.1). Neither direction requires anyone to remember to check.

## The ceremony has a price

Every witness carries the energy it cost to produce, and every unit of work
carries the energy it cost to perform. From that the receipt seals two figures
nothing else in this space can state:

- **The specified share** — how much of the work energy went into work citing
  an obligation this specification actually states, in parts-per-million (SPEC
  §5.2), with the work that cites nothing **named** rather than only counted.
  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*.
- **Microjoules per falsifiable obligation** — total attributed energy over the
  count of owed obligations evidenced at `E3` or better (SPEC §5.3). The
  denominator is deliberately the rung whose evidence can fail: a figure per
  *attempted* obligation rewards ceremony, a figure per obligation something
  would have caught rewards evidence.

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, one spending an order of magnitude
more energy to get there — that is not a matter of taste.

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

And it is **comparable only at a fixed specification address** (SPEC §5.3).
Any figure of the form *things evidenced over things total* improves when you
add trivial things — the standing objection to counting resolved doubts in
assurance argumentation — so splitting one requirement into twenty trivially
falsifiable ones would divide this figure by twenty while establishing nothing.
The receipt seals the specification's address precisely so a reader can tell
whether two figures are comparable at all. The grade and the attestation carry
no such caveat: both are minima, and a minimum cannot be improved by adding
obligations.

## The receipt is derived, never signed on request

A receipt is sealed from the specification, the artifact, the witnesses and the
work — never from a verdict handed in (SPEC §6.1). A verdict is an ordinary
data structure, and an interface that signed one would let a producer construct
the grade it wanted. Because the receipt is derived from the evidence, every
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.

Receipts seal as **`joulespec/1` JCR-1 envelopes** — canonical det-CBOR under
COSE_Sign1 with Ed25519, the wire format the rest of this family seals with, so
a receipt verifies under tooling that has never heard of JouleSpec. The core
admits no nulls and several figures are legitimately absent, so those fields
are **omitted** rather than zeroed: a reader who finds no grade knows none was
established, where a reader who found `E0` would believe one was.

Each receipt carries a **per-clause audit** — label, kind, obligation, grade,
the witness that carried it, evidence energy, stale count — because which
obligation is the weak one is the actionable fact, and it must be answerable
from the receipt alone (SPEC §6.3).

## The producer, and the standard applied to itself

A schema nobody can emit into is a schema. `joulespec-cli` is the reference
producer: it reads the clauses from a published specification document, runs
each declared check, runs it again against a **counter-artifact**, and emits a
signed witness at the rung the observations support.

```
joulespec harvest --manifest conformance/v1/harvest.toml \
                  --out conformance/v1 --require-grade E3
```

It refuses to confuse the three ways a run can fail to pass. A test that did
not run is not a test that passed — a harness filtered to a name nothing
matches prints `running 0 tests`, reports success and exits zero, so the count
is checked. A counter-artifact that did not compile demonstrates nothing,
because the check never ran; treating that as `E3` evidence would manufacture
falsifiability out of a syntax error. And a counter-artifact that compiled, ran
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
```

Run against this family's other specifications — documents written without
this producer in mind — the bulleted shape reads their conformance lists and
the heading shape reads a normative companion kept as one section per
obligation. What does not read is reported rather than returned empty: a
conformance section written as a table of profiles, or as numbered prose with
no labels, says it holds no items of the declared shape. `joulespec clauses`
exists for exactly this, because the alternative is discovering a mis-declared
shape through an item count, which says nothing about which items were missed.

Doing that found two things. In the producer: a bullet carrying a bold label
the splitter could not read was being folded into the item above, which
appended a *different* item's words to that obligation's addressed text —
a soundness bug, since the obligation then says something nobody wrote. It now
fails closed, and a bare label like `**C-neg:**` reads as the item it is. In a
sibling standard: its conformance section enumerates a clause its own
normative companion never defines, so that obligation could never have been
evidenced by anything.

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
footprint — a harness that cannot observe its own reads must not guess (SPEC
§8). Everything else is computed.

**The standard is applied to its own implementation.** Every conformance item
of SPEC §7 is mapped to a check with a counter-artifact, and the clauses are
read from the published `SPEC.md` rather than copied into the manifest, so the
manifest cannot drift from the specification: reword an item and its obligation
address moves, invalidating the evidence bound to the old wording.

Doing that found two things inspection had not. A footprint test narrowed to a
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.

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.

## Applied to a standard that is not this one

A producer that has only ever measured its own specification has demonstrated
a format, not a method. `proof/conformance/v1/joulespec.toml` points this
producer at a sibling standard: its conformance items are read from that
standard's own published document, each is mapped to a named check in its
workspace, and each mapping declares a counter-artifact that must make that
check fail. Every item of that standard's conformance section reaches `E3`,
and CI gates it there under `applied:` — so a refactor that moves the code a
mutation was aimed at makes the harvest refuse, and a check that stops being
able to fail becomes a finding instead of staying green.

Doing it found one thing, and the shape of the finding matters more than the
finding. The first counter-artifact for that standard's routing clause was
aimed at a constant the router turned out not to read, so the check passed
with the constant reordered and the harvester reported that the check could
not see its subject. The report was right; the manifest was wrong. A producer
can say only what it observed — that a check passed while something it was
supposed to notice was broken — and whether that means *the check is weak* or
*the mutation missed* is the operator's call. Re-aimed at the sort that
actually orders the rungs, the same check failed at once, which is how the
clause's evidence ended up real rather than assumed.

## Conformance packs

Three, answering different questions:

- [`conformance/v1/vectors/`](conformance/v1/vectors/) — **the certifiable
  surface.** Fixed keys, clauses, witnesses and energy, byte-stable, carrying
  one witness of every rung plus one bound to a superseded state so an
  implementation that mishandles staleness fails rather than passes quietly.
  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`.
- [`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

Structured assurance cases already standardize the *shape* of the argument —
claims decomposed to sub-claims until each links to evidence — and the
international standard for their structure is explicit that it does not set
quality requirements for the content. The grade of a piece of evidence is
exactly that content question, so `joulespec/1` adopts the vocabulary and
supplies the part left open. Certified-airborne-software practice supplies the
bidirectional rule, and grades *structural* coverage on a ladder of its own
that composes with this one rather than competing: coverage says how thoroughly
a check exercises the code, an anchor and a killed mutant say whether it can
fail at all. Supply-chain provenance frameworks grade the build record and say
nothing about correctness — that is the `A` axis, not duplicated here.
Carbon-intensity accounting for software is an international standard shaped as
a rate per functional unit of work, which is the shape of §5.3, and it covers
the energy of *running* software where this covers the energy of *producing*
it. Full treatment in SPEC §9.

## What it does not do

JouleSpec does not write specifications, run checks, formalize clauses, or
judge whether a clause states a good requirement.

And it cannot tell whether a clause says what its author meant. An obligation
is addressed, signed and tracked, and may still be the wrong requirement.
Software can satisfy every clause of its specification and be unfit for
purpose, because the specification was incomplete — and an incomplete
specification is exactly the case where every clause is covered. A grade is a
property of evidence, not of software (SPEC §8).

Three limits are worth stating here because they bound what the mechanisms
above can establish. A **footprint is trusted, not verified** — a producer that
narrows a witness to inputs its check did not read gets evidence outliving the
change that invalidated it; the claim is signed and attributable, and this
standard cannot tell what a check actually read. **`A2` is agreement, not
correctness**: reproducing a vacuous check reproduces the vacuity. And two of
the results this design builds on are thinly evidenced — the vacuity rate comes
from one industrial setting and the oracle-anchoring effect from a
single-system study — so the design rests on the mechanisms, which stand on
their own, rather than on the magnitudes.

## Reference

[`joulespec-rs/crates/joulespec-core`](joulespec-rs/crates/joulespec-core) —
obligation-addressed clauses and signed revisions (`spec`), the graded evidence
ladder with anchoring, vacuity and computed independence (`evidence`), the
deterministic two-axis evaluator with the weakest-obligation cap and
footprint-aware staleness (`conform`), the revision partition (`drift`), and
the `joulespec/1` JCR-1 receipt derived from its inputs (`receipt`).

[`joulespec-rs/crates/joulespec-cli`](joulespec-rs/crates/joulespec-cli) — the
reference producer: clauses parsed from a published document (`specdoc`), the
artifact state and its part addresses (`tree`), the declared mappings
(`manifest`), the check runner with its three-way distinction between a run
that failed, one that did not compile and one that should not have passed
(`runner`), and the harvest itself (`harvest`).

Prior art inside this family: `joule-code-spec` first shipped the signed,
content-addressed clause and the citation binding a coding operation to it.
Its citations bind by clause **label** and its audit has one notion of coverage
— a clause is covered when something claims it. That is the `E0` rung here, and
label binding is the drift hole this standard closes.